---

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


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)|))))
BY
{ (RepeatFor 2 (ParallelLast)
   THEN (Subst ⌜(2 * m * 2 * n) * (x m) ~ ((2 * n) * (x m)) * 2 * m⌝ 0⋅ THENA Auto)
   THEN (RWO "div-cancel" 0 THENA Auto)
   THEN Subst ⌜|(-(2 * m * (x n))) + ((2 * n) * (x m))| ~ |2| * |(n * (x m)) - m * (x n)|⌝ 0⋅
   THEN (Auto THEN (RWO "absval_mul<" 0⋅ THENA Auto))⋅) }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  n  :  \mBbbN{}\msupplus{}
3.  r(2  *  n)  =  |r(2  *  n)|
4.  k  :  \mBbbN{}\msupplus{}
5.  \mexists{}N:\mBbbN{}\msupplus{}.  \mforall{}m:\{N...\}.  (((-2)  *  m)  \mleq{}  (k  *  ((2  *  m  *  2)  +  (-(|2|  *  |(n  *  (x  m))  -  m  *  (x  n)|)))))
\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:
(RepeatFor  2  (ParallelLast)
  THEN  (Subst  \mkleeneopen{}(2  *  m  *  2  *  n)  *  (x  m)  \msim{}  ((2  *  n)  *  (x  m))  *  2  *  m\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (RWO  "div-cancel"  0  THENA  Auto)
  THEN  Subst  \mkleeneopen{}|(-(2  *  m  *  (x  n)))  +  ((2  *  n)  *  (x  m))|  \msim{}  |2|  *  |(n  *  (x  m))  -  m  *  (x  n)|\mkleeneclose{}  0\mcdot{}
  THEN  (Auto  THEN  (RWO  "absval\_mul<"  0\mcdot{}  THENA  Auto))\mcdot{})

---

Home Index