---

Step * of Lemma square-rleq-1-iff

∀x:ℝ. (x^2 ≤ r1 ⇐⇒ |x| ≤ r1)
BY
{ ((D 0 THENA Auto)
   THEN (InstLemma  `rnexp-rleq-iff` [⌜|x|⌝;⌜r1⌝;⌜2⌝]⋅ THENA Auto)
   THEN (RWO  "rabs-rnexp<" (-1) THENA Auto)
   THEN (RWO "-1" 0 THENA Auto)) }

1
1. x : ℝ
2. |x| ≤ r1 ⇐⇒ |x^2| ≤ r1^2
⊢ x^2 ≤ r1 ⇐⇒ |x^2| ≤ r1^2

---

Latex:

---

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


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (InstLemma    `rnexp-rleq-iff`  [\mkleeneopen{}|x|\mkleeneclose{};\mkleeneopen{}r1\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO    "rabs-rnexp<"  (-1)  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto))

---

Home Index