---

Step * 1 1 1 1 1 1 of Lemma accelerate-bdd-diff


1. k : ℕ+@i
2. f : {f:ℕ+ ⟶ ℤ| k-regular-seq(f)} 
3. n : ℕ+@i
4. |(f ((2 * k) * n)) - (2 * k) * (f n)| ≤ ((2 * k) * ((2 * k) + 1))
⊢ (|(f ((2 * k) * n)) - (2 * k) * (f n)| + |2 * k|) ≤ ((2 * k) * ((2 * k) + 2))
BY
{ (RWO "-1" 0 THEN Auto) }

1
1. k : ℕ+@i
2. f : {f:ℕ+ ⟶ ℤ| k-regular-seq(f)} 
3. n : ℕ+@i
4. |(f ((2 * k) * n)) - (2 * k) * (f n)| ≤ ((2 * k) * ((2 * k) + 1))
⊢ (((2 * k) * ((2 * k) + 1)) + |2 * k|) ≤ ((2 * k) * ((2 * k) + 2))

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}@i
2.  f  :  \{f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  k-regular-seq(f)\} 
3.  n  :  \mBbbN{}\msupplus{}@i
4.  |(f  ((2  *  k)  *  n))  -  (2  *  k)  *  (f  n)|  \mleq{}  ((2  *  k)  *  ((2  *  k)  +  1))
\mvdash{}  (|(f  ((2  *  k)  *  n))  -  (2  *  k)  *  (f  n)|  +  |2  *  k|)  \mleq{}  ((2  *  k)  *  ((2  *  k)  +  2))


By

---

Latex:
(RWO  "-1"  0  THEN  Auto)

---

Home Index