---

Step * 1 1 1 of Lemma real-approx


1. x : ℝ
2. n : ℕ+
3. r(2 * n) = |r(2 * n)|
⊢ ∀n@0:ℕ+
    ∃N:ℕ+
     ∀m:{N...}. (((-2) * m) ≤ (n@0 * ((2 * m * 2) + (-|(-(2 * m * (x n))) + (((2 * m * 2 * n) * (x m)) ÷ 2 * m)|))))
BY
{ (Auto THEN RenameVar `k' (-1)) }

1
1. x : ℝ
2. n : ℕ+
3. r(2 * n) = |r(2 * n)|
4. k : ℕ+
⊢ ∃N:ℕ+. ∀m:{N...}. (((-2) * m) ≤ (k * ((2 * m * 2) + (-|(-(2 * m * (x n))) + (((2 * m * 2 * n) * (x m)) ÷ 2 * m)|))))

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  n  :  \mBbbN{}\msupplus{}
3.  r(2  *  n)  =  |r(2  *  n)|
\mvdash{}  \mforall{}n@0:\mBbbN{}\msupplus{}
        \mexists{}N:\mBbbN{}\msupplus{}
          \mforall{}m:\{N...\}
              (((-2)  *  m)  \mleq{}  (n@0
                *  ((2  *  m  *  2)  +  (-|(-(2  *  m  *  (x  n)))  +  (((2  *  m  *  2  *  n)  *  (x  m))  \mdiv{}  2  *  m)|))))


By

---

Latex:
(Auto  THEN  RenameVar  `k'  (-1))

---

Home Index