Proofgold Proposition

∀ x0 . x0 ∈ real ⟶ SNoLt 0 x0 ⟶ (x0 = 2 ⟶ ∀ x1 : ο . x1) ⟶ (∀ x1 . x1 ∈ omega ⟶ x0 = eps_ x1 ⟶ ∀ x2 : ο . x2) ⟶ ∀ x1 : ο . (∀ x2 . and (x2 ∈ SNoL_pos x0) (SNoLt x0 (mul_SNo 2 x2)) ⟶ x1) ⟶ x1

type
prop

theory
HotG

name
pos_real_left_approx_double

proof
PUSRj..

Megalodon
pos_real_left_approx_double

proofgold address
TMUA8..^{pos_real_left_approx_double}

creator
27837 PrQUS../0aaf6..

owner
27837 PrQUS../0aaf6..

term root
721fe..