---

Step * of Lemma real-approx

No Annotations
∀[x:ℝ]. ∀[n:ℕ+].  (|(r(2 * n) * x) - r(x n)| ≤ r(2))
BY
{ (Auto
   THEN (Assert r(2 * n) = |r(2 * n)| BY
               (RWO "rabs-of-nonneg" 0 THEN Auto))
   THEN (Assert ((r(2 * n) * x) - r(x n)) = (-(r(x n)) + (r(2 * n) * x)) BY
               (nRNorm 0 THENA Auto))
   THEN (RWO "-1" 0 THENA Auto)
   THEN Thin (-1)) }

1
1. x : ℝ
2. n : ℕ+
3. r(2 * n) = |r(2 * n)|
⊢ |-(r(x n)) + (r(2 * n) * x)| ≤ r(2)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[x:\mBbbR{}].  \mforall{}[n:\mBbbN{}\msupplus{}].    (|(r(2  *  n)  *  x)  -  r(x  n)|  \mleq{}  r(2))


By

---

Latex:
(Auto
  THEN  (Assert  r(2  *  n)  =  |r(2  *  n)|  BY
                          (RWO  "rabs-of-nonneg"  0  THEN  Auto))
  THEN  (Assert  ((r(2  *  n)  *  x)  -  r(x  n))  =  (-(r(x  n))  +  (r(2  *  n)  *  x))  BY
                          (nRNorm  0  THENA  Auto))
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  Thin  (-1))

---

Home Index