Proofgold Proposition

∀ x0 x1 . x0 ∈ real ⟶ SNoLt 0 x0 ⟶ SNo x0 ⟶ x1 ∈ omega ⟶ eps_ x1 ∈ real ⟶ SNoLt 0 (mul_SNo (eps_ x1) x0) ⟶ ∀ x2 : ο . (∀ x3 . and (x3 ∈ real) (mul_SNo x0 x3 = 1) ⟶ x2) ⟶ x2

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_pos_real_recip_ex__2__4

proofgold address
TMHdu..^{Conj_pos_real_recip_ex__2__4}

creator
35053 PrNpY../4a5d8..

owner
35061 PrNpY../0bac4..

term root
fdf77..