Proofgold Proposition

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

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..