---

Step * 1 1 1 1 1 of Lemma real-approx

.....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)|)))))
BY
{ (((Assert 1 ≤ n BY Auto) THEN (Mul ⌜k⌝ (-1)⋅ THENA Auto))
   THEN (With ⌜2 * n * k⌝ (D 0)⋅ THEN Auto)
   THEN RW IntNormC 0
   THEN Auto) }

1
1. x : ℝ
2. n : ℕ+
3. r(2 * n) = |r(2 * n)|
4. k : ℕ+
5. 1 ≤ n
6. (k * 1) ≤ (k * n)
7. m : {2 * n * k...}
⊢ ((-2) * m) ≤ (((-1) * k * |((-1) * m * (x n)) + (n * (x m))| * |2|) + (4 * k * m))

---

Latex:

---

Latex:
.....assertion..... 
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|  *  |(n  *  (x  m))  -  m  *  (x  n)|)))))


By

---

Latex:
(((Assert  1  \mleq{}  n  BY  Auto)  THEN  (Mul  \mkleeneopen{}k\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto))
  THEN  (With  \mkleeneopen{}2  *  n  *  k\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)
  THEN  RW  IntNormC  0
  THEN  Auto)

---

Home Index