---

Step * 1 1 of Lemma rational-approx-property


1. x : ℝ
2. n : ℕ+
⊢ (r(2 * n) * |x + (r(-(x n))/r(2 * n))|) ≤ r(2)
BY
{ ((Assert ⌜r(2 * n) = |r(2 * n)|⌝⋅ THENA (RWO "rabs-int" 0 THEN Auto))
   THEN (RW (AddrC [1;1] (HypC (-1))) 0 THENA Auto)
   ) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  \mkleeneopen{}r(2  *  n)  =  |r(2  *  n)|\mkleeneclose{}\mcdot{}  THENA  (RWO  "rabs-int"  0  THEN  Auto))
  THEN  (RW  (AddrC  [1;1]  (HypC  (-1)))  0  THENA  Auto)
  )

---

Home Index