---

Step * of Lemma square-nonneg

∀[x:ℝ]. (r0 ≤ (x * x))
BY
{ (Auto
   THEN Unfold `rleq` 0
   THEN nRNorm 0
   THEN (RWO "rnonneg-iff" 0 THENA Auto)
   THEN (RWO "rmul-bdd-diff-reg-seq-mul" 0 THENA Auto)
   THEN RepUR ``rnonneg2 reg-seq-mul`` 0
   THEN Auto) }

1
1. x : ℝ
2. n : ℕ+
⊢ ∃N:ℕ+. ∀m:{N...}. (((-2) * m) ≤ (n * (((x m) * (x m)) ÷ 2 * m)))

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (r0  \mleq{}  (x  *  x))


By

---

Latex:
(Auto
  THEN  Unfold  `rleq`  0
  THEN  nRNorm  0
  THEN  (RWO  "rnonneg-iff"  0  THENA  Auto)
  THEN  (RWO  "rmul-bdd-diff-reg-seq-mul"  0  THENA  Auto)
  THEN  RepUR  ``rnonneg2  reg-seq-mul``  0
  THEN  Auto)

---

Home Index