---

Step * of Lemma square-positive-iff

∀x:ℝ. (r0 < (x * x) ⇐⇒ x ≠ r0)
BY
{ (InstLemma `rnexp2-positive-iff` [] THEN ParallelLast' THEN (RWO "-1<" 0 THENA Auto)) }

1
1. x : ℝ
2. r0 < x^2 ⇐⇒ x ≠ r0
⊢ r0 < (x * x) ⇐⇒ r0 < x^2

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  (r0  <  (x  *  x)  \mLeftarrow{}{}\mRightarrow{}  x  \mneq{}  r0)


By

---

Latex:
(InstLemma  `rnexp2-positive-iff`  []  THEN  ParallelLast'  THEN  (RWO  "-1<"  0  THENA  Auto))

---

Home Index