Proofgold Proposition

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

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