Step
*
1
1
1
1
1
1
1
2
of Lemma
accelerate_wf
1. k : ℕ+
2. f : ℕ+ ⟶ ℤ
3. accelerate(k;f) ∈ ℕ+ ⟶ ℤ
4. ∀n,m:ℕ+. (|(m * (f n)) - n * (f m)| ≤ ((2 * k) * (n + m)))
5. n : ℕ+@i
6. m : ℕ+@i
7. ∀m,x:ℤ. ((2 * k) * m * (x ÷ 2 * k) ~ (m * x) - m * (x rem 2 * k))
8. r1 : {r:ℤ| |r| < |2 * k|}
9. (f ((2 * k) * n) rem 2 * k) = r1 ∈ {r:ℤ| |r| < |2 * k|}
10. r2 : {r:ℤ| |r| < |2 * k|}
11. (f ((2 * k) * m) rem 2 * k) = r2 ∈ {r:ℤ| |r| < |2 * k|}
12. |(m * (f ((2 * k) * n))) - m * r1 - (n * (f ((2 * k) * m))) - n * r2| ≤ (|(m * (f ((2 * k) * n))) - n
* (f ((2 * k) * m))|
+ |-(m * r1)|
+ |n * r2|)
13. (|-(m * r1)| + |n * r2|) ≤ (|2 * k| * (n + m))
14. |(m * (f ((2 * k) * n))) - n * (f ((2 * k) * m))| ≤ (|2 * k| * (n + m))
⊢ (|(m * (f ((2 * k) * n))) - n * (f ((2 * k) * m))| + (|2 * k| * (n + m))) ≤ (|2 * k| * 2 * (n + m))
BY
{ (RWO "-1" 0 THEN Auto) }
Latex:
Latex:
1. k : \mBbbN{}\msupplus{}
2. f : \mBbbN{}\msupplus{} {}\mrightarrow{} \mBbbZ{}
3. accelerate(k;f) \mmember{} \mBbbN{}\msupplus{} {}\mrightarrow{} \mBbbZ{}
4. \mforall{}n,m:\mBbbN{}\msupplus{}. (|(m * (f n)) - n * (f m)| \mleq{} ((2 * k) * (n + m)))
5. n : \mBbbN{}\msupplus{}@i
6. m : \mBbbN{}\msupplus{}@i
7. \mforall{}m,x:\mBbbZ{}. ((2 * k) * m * (x \mdiv{} 2 * k) \msim{} (m * x) - m * (x rem 2 * k))
8. r1 : \{r:\mBbbZ{}| |r| < |2 * k|\}
9. (f ((2 * k) * n) rem 2 * k) = r1
10. r2 : \{r:\mBbbZ{}| |r| < |2 * k|\}
11. (f ((2 * k) * m) rem 2 * k) = r2
12. |(m * (f ((2 * k) * n))) - m * r1 - (n * (f ((2 * k) * m))) - n * r2|
\mleq{} (|(m * (f ((2 * k) * n))) - n * (f ((2 * k) * m))| + |-(m * r1)| + |n * r2|)
13. (|-(m * r1)| + |n * r2|) \mleq{} (|2 * k| * (n + m))
14. |(m * (f ((2 * k) * n))) - n * (f ((2 * k) * m))| \mleq{} (|2 * k| * (n + m))
\mvdash{} (|(m * (f ((2 * k) * n))) - n * (f ((2 * k) * m))| + (|2 * k| * (n + m))) \mleq{} (|2 * k|
* 2
* (n + m))
By
Latex:
(RWO "-1" 0 THEN Auto)
Home
Index