---

Step * of Lemma accelerate-real-strong-regular

∀k:ℕ+. ∀x:ℝ.  strong-regular-int-seq(2 * k;(2 * k) + 1;accelerate(k;x))
BY
{ ((Auto THEN D 0 THEN Auto)
   THEN D 2
   THEN (Unhide THENA Auto)
   THEN Unfold `regular-int-seq` 3
   THEN RepUR ``accelerate`` 0
   THEN RepeatFor 2 (((CallByValueReduce 0 THENA Auto) THEN Reduce 0))
   THEN (Assert 2 * k ~ |2 * k| BY
               Auto)) }

1
1. k : ℕ+
2. x : ℕ+ ⟶ ℤ
3. ∀n,m:ℕ+.  (|(m * (x n)) - n * (x m)| ≤ ((2 * 1) * (n + m)))
4. n : ℕ+
5. m : ℕ+
6. 2 * k ~ |2 * k|
⊢ ((2 * k) * |(m * ((x ((2 * k) * n)) ÷ 2 * k)) - n * ((x ((2 * k) * m)) ÷ 2 * k)|) ≤ (((2 * k) + 1) * (n + m))

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}\msupplus{}.  \mforall{}x:\mBbbR{}.    strong-regular-int-seq(2  *  k;(2  *  k)  +  1;accelerate(k;x))


By

---

Latex:
((Auto  THEN  D  0  THEN  Auto)
  THEN  D  2
  THEN  (Unhide  THENA  Auto)
  THEN  Unfold  `regular-int-seq`  3
  THEN  RepUR  ``accelerate``  0
  THEN  RepeatFor  2  (((CallByValueReduce  0  THENA  Auto)  THEN  Reduce  0))
  THEN  (Assert  2  *  k  \msim{}  |2  *  k|  BY
                          Auto))

---

Home Index