---

Step * of Lemma rational-approx-property-alt2

∀x:ℝ. ∀n:ℕ+.  (|r(x n)| ≤ ((r(2 * n) * |x|) + r(2)))
BY
{ (InstLemma `rational-approx-property-alt` []
   THEN RepeatFor 2 (ParallelLast')
   THEN (RWO "rabs-difference-symmetry" (-1) THENA Auto)
   THEN (Assert r(x n) = ((r(x n) - r(2 * n) * x) + (r(2 * n) * x)) BY
               Auto)
   THEN (RWO  "-1" 0 THENA Auto)) }

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

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  \mforall{}n:\mBbbN{}\msupplus{}.    (|r(x  n)|  \mleq{}  ((r(2  *  n)  *  |x|)  +  r(2)))


By

---

Latex:
(InstLemma  `rational-approx-property-alt`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  (RWO  "rabs-difference-symmetry"  (-1)  THENA  Auto)
  THEN  (Assert  r(x  n)  =  ((r(x  n)  -  r(2  *  n)  *  x)  +  (r(2  *  n)  *  x))  BY
                          Auto)
  THEN  (RWO    "-1"  0  THENA  Auto))

---

Home Index