Proofgold Proof

pf

Let x0 of type ι be given.

Assume H0: RealsStruct x0.

Apply Field_of_RealsStruct_0 with x0, λ x1 x2 . ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ setminus x1 (Sing (field4 x0)) ⟶ and (Field_div (Field_of_RealsStruct x0) x3 x4 ∈ x1) (x3 = field2b x0 x4 (Field_div (Field_of_RealsStruct x0) x3 x4)).

Apply Field_of_RealsStruct_2f with x0, λ x1 x2 : ι → ι → ι . ∀ x3 . x3 ∈ ap (Field_of_RealsStruct x0) 0 ⟶ ∀ x4 . x4 ∈ setminus (ap (Field_of_RealsStruct x0) 0) (Sing (field4 x0)) ⟶ and (Field_div (Field_of_RealsStruct x0) x3 x4 ∈ ap (Field_of_RealsStruct x0) 0) (x3 = x1 x4 (Field_div (Field_of_RealsStruct x0) x3 x4)) leaving 2 subgoals.

The subproof is completed by applying H0.

Apply Field_of_RealsStruct_3 with x0, λ x1 x2 . ∀ x3 . x3 ∈ ap (Field_of_RealsStruct x0) 0 ⟶ ∀ x4 . x4 ∈ setminus (ap (Field_of_RealsStruct x0) 0) (Sing x1) ⟶ and (Field_div (Field_of_RealsStruct x0) x3 x4 ∈ ap (Field_of_RealsStruct x0) 0) (x3 = (λ x5 . ap (ap (ap (Field_of_RealsStruct x0) 2) x5)) x4 (Field_div (Field_of_RealsStruct x0) x3 x4)).

Apply Field_div_prop with Field_of_RealsStruct x0.

Apply Field_Field_of_RealsStruct with x0.

The subproof is completed by applying H0.

■