---

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


1. x : ℝ
2. n : ℕ+
3. r(2 * n) = |r(2 * n)|
⊢ (|r(2 * n)| * |x + (r(-(x n))/r(2 * n))|) ≤ r(2)
BY
{ ((RWO "rabs-rmul<" 0 THENA Auto) THEN (RW (AddrC [1;1] FieldReqC) 0 THENA Auto)) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "rabs-rmul<"  0  THENA  Auto)  THEN  (RW  (AddrC  [1;1]  FieldReqC)  0  THENA  Auto))

---

Home Index