Proofgold Proposition

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

type
prop

theory
HotG

name
nonzero_real_recip_ex

proof
PUK8p..

Megalodon
nonzero_real_recip_ex

proofgold address
TMUcA..^{nonzero_real_recip_ex}

creator
12486 PrGxv../56f8b..

owner
12486 PrGxv../56f8b..

term root
4fbd3..