Proofgold Proposition

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

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