Proofgold Proposition

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

type
prop

theory
HotG

name
pos_real_recip_ex

proof
PUK8p..

Megalodon
pos_real_recip_ex

proofgold address
TMHFw..^{pos_real_recip_ex}

creator
12486 PrGxv../8803e..

owner
12486 PrGxv../8803e..

term root
141e4..