---

Step * of Lemma square-rless-implies

∀x,y:ℝ.  ((r0 ≤ y) ⇒ (x^2 < y^2) ⇒ (x < y))
BY
{ (Auto
   THEN nRAdd ⌜-(x^2)⌝ (-1)⋅
   THEN (Assert (-(x^2) + y^2) = ((y + x) * (y - x)) BY
               ((RWO "rnexp2" 0 THENM nRNorm 0) THEN Auto))
   THEN (RWO  "-1" (-2) THENA Auto)
   THEN (RWO "rmul-is-positive" (-2) THENA Auto)
   THEN D -2
   THEN Auto) }

1
1. x : ℝ
2. y : ℝ
3. r0 ≤ y
4. (y + x) < r0
5. (y - x) < r0
6. (-(x^2) + y^2) = ((y + x) * (y - x))
⊢ x < y

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    ((r0  \mleq{}  y)  {}\mRightarrow{}  (x\^{}2  <  y\^{}2)  {}\mRightarrow{}  (x  <  y))


By

---

Latex:
(Auto
  THEN  nRAdd  \mkleeneopen{}-(x\^{}2)\mkleeneclose{}  (-1)\mcdot{}
  THEN  (Assert  (-(x\^{}2)  +  y\^{}2)  =  ((y  +  x)  *  (y  -  x))  BY
                          ((RWO  "rnexp2"  0  THENM  nRNorm  0)  THEN  Auto))
  THEN  (RWO    "-1"  (-2)  THENA  Auto)
  THEN  (RWO  "rmul-is-positive"  (-2)  THENA  Auto)
  THEN  D  -2
  THEN  Auto)

---

Home Index