Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: RealsStruct x0.
Apply Field_of_RealsStruct_0 with x0, λ x1 x2 . ∀ x3 x4 . nIn x3 x1Field_div (Field_of_RealsStruct x0) x3 x4 = 0.
Apply Field_div_undef1 with Field_of_RealsStruct x0.
Apply Field_Field_of_RealsStruct with x0.
The subproof is completed by applying H0.