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 ⟶ RealsStruct_leq x0 x1 x2 ⟶ RealsStruct_leq x0 x2 x1 ⟶ x1 = x2 leaving 2 subgoals.

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

Assume H2: explicit_OrderedField (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) (RealsStruct_leq x0).

Assume H3: ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ lt (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) (RealsStruct_leq x0) (field4 x0) x1 ⟶ RealsStruct_leq x0 (field4 x0) 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 x0 x2 (field2b x0 x3 x1)).

Assume H4: ∀ 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))).

Apply explicit_OrderedField_leq_antisym with field0 ..., ..., ..., ..., ..., ....

...

...

■