Proofgold Proposition

∀ x0 x1 x2 x3 x4 x5 x6 . SNo x0 ⟶ SNo x1 ⟶ SNo (mul_SNo x0 x1) ⟶ SNo (minus_SNo (mul_SNo x0 x1)) ⟶ SNo x2 ⟶ SNoLt (mul_SNo x0 x1) x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNoLe (add_SNo (mul_SNo x3 x1) (mul_SNo x0 x4)) (add_SNo x2 (mul_SNo x3 x4)) ⟶ SNo (mul_SNo x0 x4) ⟶ SNo (mul_SNo x3 x4) ⟶ SNo (minus_SNo (mul_SNo x3 x4)) ⟶ SNo (add_SNo x0 (minus_SNo x3)) ⟶ SNo (add_SNo x4 (minus_SNo x1)) ⟶ x5 ∈ omega ⟶ SNoLe (eps_ x5) (add_SNo x0 (minus_SNo x3)) ⟶ x6 ∈ omega ⟶ SNoLe (eps_ x6) (add_SNo x4 (minus_SNo x1)) ⟶ SNo (eps_ x5) ⟶ SNo (eps_ x6) ⟶ SNo (eps_ (add_SNo x5 x6)) ⟶ SNo (mul_SNo (eps_ x5) (eps_ x6)) ⟶ SNoLt (abs_SNo (add_SNo x2 (minus_SNo (mul_SNo x0 x1)))) (eps_ (add_SNo x5 x6)) ⟶ not (SNoLe (eps_ (add_SNo x5 x6)) (abs_SNo (add_SNo x2 (minus_SNo (mul_SNo x0 x1)))))

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_real_mul_SNo_pos__14__9

proofgold address
TMY1t..^{Conj_real_mul_SNo_pos__14__9}

creator
35053 PrNpY../50408..

owner
35061 PrNpY../558fe..

term root
2dc4b..