Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: RealsStruct x0.
Apply RealsStruct_Z_props with x0, RealsStruct_Z x0 ⊆ field0 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H1: ∀ x1 . x1 ∈ RealsStruct_Npos x0 ⟶ Field_minus (Field_of_RealsStruct x0) x1 ∈ RealsStruct_Z x0.
Assume H2: field4 x0 ∈ RealsStruct_Z x0.
Assume H3: RealsStruct_Npos x0 ⊆ RealsStruct_Z x0.
Assume H4: RealsStruct_Z x0 ⊆ field0 x0.
Assume H5: ∀ x1 . x1 ∈ RealsStruct_Z x0 ⟶ ∀ x2 : ο . (Field_minus (Field_of_RealsStruct x0) x1 ∈ RealsStruct_Npos x0 ⟶ x2) ⟶ (x1 = field4 x0 ⟶ x2) ⟶ (x1 ∈ RealsStruct_Npos x0 ⟶ x2) ⟶ x2.
Assume H6: RealsStruct_one x0 ∈ RealsStruct_Z x0.
Assume H7: Field_minus (Field_of_RealsStruct x0) (RealsStruct_one x0) ∈ RealsStruct_Z x0.
Assume H8: ∀ x1 . x1 ∈ RealsStruct_Z x0 ⟶ Field_minus (Field_of_RealsStruct x0) x1 ∈ RealsStruct_Z x0.
Assume H9: ∀ x1 . x1 ∈ RealsStruct_Z x0 ⟶ ∀ x2 . x2 ∈ RealsStruct_Z x0 ⟶ field1b x0 x1 x2 ∈ RealsStruct_Z x0.
Assume H10: ∀ x1 . x1 ∈ RealsStruct_Z x0 ⟶ ∀ x2 . x2 ∈ RealsStruct_Z x0 ⟶ field2b x0 x1 x2 ∈ RealsStruct_Z x0.
The subproof is completed by applying H4.
■