---

Step * 1 of Lemma rational-approx-property-alt2


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))
BY
{ ((RWO  "r-triangle-inequality" 0 THENA Auto)
   THEN (RWO "3" 0 THENA Auto)
   THEN (RWO "rabs-rmul" 0 THENA Auto)
   THEN (Assert |r(2 * n)| = r(2 * n) BY
               (RWO  "rabs-of-nonneg" 0 THEN Auto))
   THEN RWO  "-1" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  n  :  \mBbbN{}\msupplus{}
3.  |r(x  n)  -  r(2  *  n)  *  x|  \mleq{}  r(2)
4.  r(x  n)  =  ((r(x  n)  -  r(2  *  n)  *  x)  +  (r(2  *  n)  *  x))
\mvdash{}  |(r(x  n)  -  r(2  *  n)  *  x)  +  (r(2  *  n)  *  x)|  \mleq{}  ((r(2  *  n)  *  |x|)  +  r(2))


By

---

Latex:
((RWO    "r-triangle-inequality"  0  THENA  Auto)
  THEN  (RWO  "3"  0  THENA  Auto)
  THEN  (RWO  "rabs-rmul"  0  THENA  Auto)
  THEN  (Assert  |r(2  *  n)|  =  r(2  *  n)  BY
                          (RWO    "rabs-of-nonneg"  0  THEN  Auto))
  THEN  RWO    "-1"  0
  THEN  Auto)

---

Home Index