Proofgold Proof

pf

Let x0 of type ι be given.

Assume H0: RealsStruct x0.

Apply RealsStruct_Z_props with x0, RealsStruct_Npos x0 ⊆ RealsStruct_Z 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 H3.

■