---

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


1. x : ℕ+ ⟶ ℤ
2. y : ℕ+ ⟶ ℤ
3. k : ℕ+
4. l : ℕ+
5. ∀n,m:ℕ+.  (|(m * (y n)) - n * (y m)| ≤ ((2 * l) * (n + m)))
6. ∀n,m:ℕ+.  (|(m * (x n)) - n * (x m)| ≤ ((2 * k) * (n + m)))
7. B : ℕ
8. ∀n:ℕ+. (|(x n) - y n| ≤ B)
9. n : ℕ+@i
10. m : ℕ+@i
11. |(m * (x n)) - m * (y n)| ≤ (((2 * k) * (n + m)) + |(n * (x m)) - n * (y m)| + ((2 * l) * (n + m)))
⊢ (m * |(x n) - y n|) ≤ ((((2 * k) + (2 * l)) * (n + m)) + (n * B))
BY
{ (RWW "left_mul_subtract_distrib< absval_mul" (-1) THENA Auto) }

1
1. x : ℕ+ ⟶ ℤ
2. y : ℕ+ ⟶ ℤ
3. k : ℕ+
4. l : ℕ+
5. ∀n,m:ℕ+.  (|(m * (y n)) - n * (y m)| ≤ ((2 * l) * (n + m)))
6. ∀n,m:ℕ+.  (|(m * (x n)) - n * (x m)| ≤ ((2 * k) * (n + m)))
7. B : ℕ
8. ∀n:ℕ+. (|(x n) - y n| ≤ B)
9. n : ℕ+@i
10. m : ℕ+@i
11. (|m| * |(x n) - y n|) ≤ (((2 * k) * (n + m)) + (|n| * |(x m) - y m|) + ((2 * l) * (n + m)))
⊢ (m * |(x n) - y n|) ≤ ((((2 * k) + (2 * l)) * (n + m)) + (n * B))

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
2.  y  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  k  :  \mBbbN{}\msupplus{}
4.  l  :  \mBbbN{}\msupplus{}
5.  \mforall{}n,m:\mBbbN{}\msupplus{}.    (|(m  *  (y  n))  -  n  *  (y  m)|  \mleq{}  ((2  *  l)  *  (n  +  m)))
6.  \mforall{}n,m:\mBbbN{}\msupplus{}.    (|(m  *  (x  n))  -  n  *  (x  m)|  \mleq{}  ((2  *  k)  *  (n  +  m)))
7.  B  :  \mBbbN{}
8.  \mforall{}n:\mBbbN{}\msupplus{}.  (|(x  n)  -  y  n|  \mleq{}  B)
9.  n  :  \mBbbN{}\msupplus{}@i
10.  m  :  \mBbbN{}\msupplus{}@i
11.  |(m  *  (x  n))  -  m  *  (y  n)|  \mleq{}  (((2  *  k)  *  (n  +  m))
        +  |(n  *  (x  m))  -  n  *  (y  m)|
        +  ((2  *  l)  *  (n  +  m)))
\mvdash{}  (m  *  |(x  n)  -  y  n|)  \mleq{}  ((((2  *  k)  +  (2  *  l))  *  (n  +  m))  +  (n  *  B))


By

---

Latex:
(RWW  "left\_mul\_subtract\_distrib<  absval\_mul"  (-1)  THENA  Auto)

---

Home Index