---

Step * of Lemma square-rge-1-iff

∀x:ℝ. (r1 ≤ x^2 ⇐⇒ r1 ≤ |x|)
BY
{ (InstLemma `square-rleq-1-iff` []
   THEN ParallelLast
   THEN Auto
   THEN (BLemma `not-rless` THENA Auto)
   THEN (D 0 THENA Auto)) }

1
1. ∀x:ℝ. (x^2 ≤ r1 ⇐⇒ |x| ≤ r1)
2. x : ℝ
3. (x^2 ≤ r1) ⇒ (|x| ≤ r1)
4. (x^2 ≤ r1) ⇐ |x| ≤ r1
5. r1 ≤ x^2
6. |x| < r1
⊢ False

2
1. ∀x:ℝ. (x^2 ≤ r1 ⇐⇒ |x| ≤ r1)
2. x : ℝ
3. (x^2 ≤ r1) ⇒ (|x| ≤ r1)
4. (x^2 ≤ r1) ⇐ |x| ≤ r1
5. r1 ≤ |x|
6. x^2 < r1
⊢ False

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  (r1  \mleq{}  x\^{}2  \mLeftarrow{}{}\mRightarrow{}  r1  \mleq{}  |x|)


By

---

Latex:
(InstLemma  `square-rleq-1-iff`  []
  THEN  ParallelLast
  THEN  Auto
  THEN  (BLemma  `not-rless`  THENA  Auto)
  THEN  (D  0  THENA  Auto))

---

Home Index