---

Step * 1 1 1 1 of Lemma real-approx


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)|))))
BY
{ Assert ⌜∃N:ℕ+. ∀m:{N...}. (((-2) * m) ≤ (k * ((2 * m * 2) + (-(|2| * |(n * (x m)) - m * (x n)|)))))⌝⋅ }

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

2
1. x : ℝ
2. n : ℕ+
3. r(2 * n) = |r(2 * n)|
4. k : ℕ+
5. ∃N:ℕ+. ∀m:{N...}. (((-2) * m) ≤ (k * ((2 * m * 2) + (-(|2| * |(n * (x m)) - m * (x n)|)))))
⊢ ∃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)|
4.  k  :  \mBbbN{}\msupplus{}
\mvdash{}  \mexists{}N:\mBbbN{}\msupplus{}
      \mforall{}m:\{N...\}
          (((-2)  *  m)  \mleq{}  (k
            *  ((2  *  m  *  2)  +  (-|(-(2  *  m  *  (x  n)))  +  (((2  *  m  *  2  *  n)  *  (x  m))  \mdiv{}  2  *  m)|))))


By

---

Latex:
Assert  \mkleeneopen{}\mexists{}N:\mBbbN{}\msupplus{}.  \mforall{}m:\{N...\}.  (((-2)  *  m)  \mleq{}  (k  *  ((2  *  m  *  2)  +  (-(|2|  *  |(n  *  (x  m))  -  m  *  (x  n)|)))))\mkleeneclose{}
\mcdot{}

---

Home Index