Proofgold Proposition

∀ x0 . SNo x0 ⟶ x0 ∈ real ⟶ SNoLt 0 x0 ⟶ and (recip_SNo_pos x0 ∈ real) (∀ x1 . nat_p x1 ⟶ and (ap (SNo_recipaux x0 recip_SNo_pos x1) 0 ⊆ real) (ap (SNo_recipaux x0 recip_SNo_pos x1) 1 ⊆ real))

type
prop

theory
HotG

name
real_recip_SNo_lem1

proof
PUfrJ..

Megalodon
real_recip_SNo_lem1

proofgold address
TMSMg..^{real_recip_SNo_lem1}

creator
27869 PrQUS../b06c3..

owner
27869 PrQUS../b06c3..

term root
12948..