Proofgold Proof

pf

Let x0 of type ι be given.

Assume H0: RealsStruct x0.

Apply explicit_Reals_E with field0 x0, field4 x0, RealsStruct_one x0, field1b x0, field2b x0, RealsStruct_leq x0, ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ ∀ x3 . x3 ∈ field0 x0 ⟶ field2b x0 x1 (field1b x0 x2 x3) = field1b x0 (field2b x0 x1 x2) (field2b x0 x1 x3) leaving 2 subgoals.

Assume H1: explicit_Reals (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) (RealsStruct_leq x0).

Apply explicit_OrderedField_E with field0 x0, field4 x0, RealsStruct_one x0, field1b x0, field2b x0, RealsStruct_leq x0, (∀ x1 . ... ⟶ ∀ x2 . ... ⟶ ... ⟶ ... ⟶ ∃ x3 . and (x3 ∈ Sep (field0 x0) (natOfOrderedField_p (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) (RealsStruct_leq x0))) (RealsStruct_leq ... ... ...)) ⟶ (∀ x1 . x1 ∈ setexp (field0 x0) (Sep (field0 x0) (natOfOrderedField_p (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) (RealsStruct_leq x0))) ⟶ ∀ x2 . x2 ∈ setexp (field0 x0) (Sep (field0 x0) (natOfOrderedField_p (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) (RealsStruct_leq x0))) ⟶ (∀ x3 . x3 ∈ Sep (field0 x0) (natOfOrderedField_p (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) (RealsStruct_leq x0)) ⟶ and (and (RealsStruct_leq x0 (ap x1 x3) (ap x2 x3)) (RealsStruct_leq x0 (ap x1 x3) (ap x1 (field1b x0 x3 (RealsStruct_one x0))))) (RealsStruct_leq x0 (ap x2 (field1b x0 x3 (RealsStruct_one x0))) (ap x2 x3))) ⟶ ∃ x3 . and (x3 ∈ field0 x0) (∀ x4 . x4 ∈ Sep (field0 x0) (natOfOrderedField_p (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) (RealsStruct_leq x0)) ⟶ and (RealsStruct_leq x0 (ap x1 x4) x3) (RealsStruct_leq x0 x3 (ap x2 x4)))) ⟶ ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ ∀ x3 . x3 ∈ field0 x0 ⟶ field2b x0 x1 (field1b x0 x2 x3) = field1b x0 (field2b x0 x1 x2) (field2b x0 x1 x3).

...

...

■