Proofgold Proposition

∀ x0 . RealsStruct x0 ⟶ ∀ x1 : ο . ((∀ 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) ⟶ x1

type
prop

theory
HotG

name
RealsStruct_Z_props

proof
PUSVY..

Megalodon
RealsStruct_Z_props

proofgold address
TMQPz..^{RealsStruct_Z_props}

creator
5804 Pr6Pc../82632..

owner
5804 Pr6Pc../82632..

term root
017fe..