Proofgold Proof

pf

Let x0 of type ι be given.

Assume H0: RealsStruct x0.

Let x1 of type ο be given.

Assume H1: (∀ x2 . x2 ∈ RealsStruct_Npos x0 ⟶ Field_minus (Field_of_RealsStruct x0) x2 ∈ RealsStruct_Z x0) ⟶ field4 x0 ∈ RealsStruct_Z x0 ⟶ RealsStruct_Npos x0 ⊆ RealsStruct_Z x0 ⟶ RealsStruct_Z x0 ⊆ field0 x0 ⟶ (∀ x2 . x2 ∈ RealsStruct_Z x0 ⟶ ∀ x3 : ο . (Field_minus (Field_of_RealsStruct x0) x2 ∈ RealsStruct_Npos x0 ⟶ x3) ⟶ (x2 = field4 x0 ⟶ x3) ⟶ (x2 ∈ RealsStruct_Npos x0 ⟶ x3) ⟶ x3) ⟶ RealsStruct_one x0 ∈ RealsStruct_Z x0 ⟶ Field_minus (Field_of_RealsStruct x0) (RealsStruct_one x0) ∈ RealsStruct_Z x0 ⟶ (∀ x2 . x2 ∈ RealsStruct_Z x0 ⟶ Field_minus (Field_of_RealsStruct x0) x2 ∈ RealsStruct_Z x0) ⟶ (∀ x2 . x2 ∈ RealsStruct_Z x0 ⟶ ∀ x3 . x3 ∈ RealsStruct_Z x0 ⟶ field1b x0 x2 x3 ∈ RealsStruct_Z x0) ⟶ (∀ x2 . x2 ∈ RealsStruct_Z x0 ⟶ ∀ x3 . x3 ∈ RealsStruct_Z x0 ⟶ field2b x0 x2 x3 ∈ RealsStruct_Z x0) ⟶ x1.

Apply explicit_OrderedField_Z_props with field0 x0, field4 x0, RealsStruct_one x0, field1b x0, field2b x0, RealsStruct_leq x0, x1 leaving 2 subgoals.

Apply explicit_OrderedField_of_RealsStruct with x0.

The subproof is completed by applying H0.

Apply unknownprop_87925c67a03b35d7e2b95672013636ce0205b3bb767f5d1c0c78f69cadaeb3e9 with x0, λ x2 x3 . (∀ x4 . x4 ∈ RealsStruct_Npos x0 ⟶ explicit_Field_minus (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) x4 ∈ x2) ⟶ field4 x0 ∈ x2 ⟶ RealsStruct_Npos x0 ⊆ x2 ⟶ x2 ⊆ field0 x0 ⟶ (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 : ο . (explicit_Field_minus (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) x4 ∈ RealsStruct_Npos x0 ⟶ x5) ⟶ (x4 = field4 x0 ⟶ x5) ⟶ (x4 ∈ RealsStruct_Npos x0 ⟶ x5) ⟶ x5) ⟶ RealsStruct_one x0 ∈ x2 ⟶ explicit_Field_minus (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) (RealsStruct_one x0) ∈ x2 ⟶ (∀ x4 . x4 ∈ x2 ⟶ explicit_Field_minus (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) x4 ∈ x2) ⟶ (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ field1b x0 x4 x5 ∈ x2) ⟶ (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ field2b x0 x4 x5 ∈ x2) ⟶ x1 leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H2: ∀ x2 . ... ⟶ explicit_Field_minus (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) ... ... ∈ ....

...

■