---

Step * 1 1 of Lemma square-rless-1-iff


1. x : ℝ
2. r0 < (r1 + -(x * x))
⊢ |x| < r1
BY
{ ((Assert (r1 + -(x * x)) = ((r1 + x) * (r1 - x)) BY (nRNorm 0 THEN Auto)) THEN (RWO "-1" (-2) THENA Auto)) }

1
1. x : ℝ
2. r0 < ((r1 + x) * (r1 - x))
3. (r1 + -(x * x)) = ((r1 + x) * (r1 - x))
⊢ |x| < r1

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  r0  <  (r1  +  -(x  *  x))
\mvdash{}  |x|  <  r1


By

---

Latex:
((Assert  (r1  +  -(x  *  x))  =  ((r1  +  x)  *  (r1  -  x))  BY
                (nRNorm  0  THEN  Auto))
  THEN  (RWO  "-1"  (-2)  THENA  Auto)
  )

---

Home Index