---

Step * of Lemma square-rleq-implies

∀x,y:ℝ.  ((r0 ≤ y) ⇒ (x^2 ≤ y^2) ⇒ (x ≤ y))
BY
{ (Auto THEN (InstLemma `rnexp-rleq-iff` [⌜|x|⌝;⌜y⌝;⌜2⌝]⋅ THENA Auto) THEN RepeatFor 2 (D -1)) }

1
.....antecedent..... 
1. x : ℝ
2. y : ℝ
3. r0 ≤ y
4. x^2 ≤ y^2
5. (|x| ≤ y) ⇒ (|x|^2 ≤ y^2)
⊢ |x|^2 ≤ y^2

2
1. x : ℝ
2. y : ℝ
3. r0 ≤ y
4. x^2 ≤ y^2
5. (|x| ≤ y) ⇒ (|x|^2 ≤ y^2)
6. |x| ≤ y
⊢ x ≤ y

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (InstLemma  `rnexp-rleq-iff`  [\mkleeneopen{}|x|\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  RepeatFor  2  (D  -1))

---

Home Index