---

Step * 2 1 1 1 1 1 1 of Lemma regularize-2-regular


1. f : ℤ ⟶ ℤ@i
2. n : ℕ+@i
3. m : ℕ+@i
4. ¬(∀i,j:{1..m + 1-}.  (|(i * (f j)) - j * (f i)| ≤ (2 * (i + j))))
5. ∀i,j:{1..n + 1-}.  (|(i * (f j)) - j * (f i)| ≤ (2 * (i + j)))
6. v : ℕ@i
7. ∀[i:ℕ]. ¬¬(∀i1,j:{1..i + 1-}.  (|(i1 * (f j)) - j * (f i1)| ≤ (2 * (i1 + j)))) supposing i < v@i
8. ¬(v = 1 ∈ ℤ)
9. ¬(v = 0 ∈ ℤ)
10. k : ℕ+@i
11. (v - 1) = k ∈ ℕ+@i
12. ¬(n ≤ k)
13. v ≤ n
⊢ ∀i,j:{1..v + 1-}.  (|(i * (f j)) - j * (f i)| ≤ (2 * (i + j)))
BY
{ (ParallelOp 5 THEN ParallelLast) }

---

Latex:

---

Latex:

1.  f  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}@i
2.  n  :  \mBbbN{}\msupplus{}@i
3.  m  :  \mBbbN{}\msupplus{}@i
4.  \mneg{}(\mforall{}i,j:\{1..m  +  1\msupminus{}\}.    (|(i  *  (f  j))  -  j  *  (f  i)|  \mleq{}  (2  *  (i  +  j))))
5.  \mforall{}i,j:\{1..n  +  1\msupminus{}\}.    (|(i  *  (f  j))  -  j  *  (f  i)|  \mleq{}  (2  *  (i  +  j)))
6.  v  :  \mBbbN{}@i
7.  \mforall{}[i:\mBbbN{}].  \mneg{}\mneg{}(\mforall{}i1,j:\{1..i  +  1\msupminus{}\}.    (|(i1  *  (f  j))  -  j  *  (f  i1)|  \mleq{}  (2  *  (i1  +  j))))  supposing  i  <  v@i
8.  \mneg{}(v  =  1)
9.  \mneg{}(v  =  0)
10.  k  :  \mBbbN{}\msupplus{}@i
11.  (v  -  1)  =  k@i
12.  \mneg{}(n  \mleq{}  k)
13.  v  \mleq{}  n
\mvdash{}  \mforall{}i,j:\{1..v  +  1\msupminus{}\}.    (|(i  *  (f  j))  -  j  *  (f  i)|  \mleq{}  (2  *  (i  +  j)))


By

---

Latex:
(ParallelOp  5  THEN  ParallelLast)

---

Home Index