Proofgold Proposition

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

type
prop

theory
HotG

name
pos_small_real_recip_ex

proof
PUK8p..

Megalodon
pos_small_real_recip_ex

proofgold address
TMKZT..^{pos_small_real_recip_ex}

creator
12486 PrGxv../91d11..

owner
12486 PrGxv../91d11..

term root
631ec..