---

Step * 1 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) - 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))
BY
{ ((Subst ⌜|m| ~ m⌝ (-1)⋅ THENA (RWO "absval_pos" 0 THEN Auto))
   THEN RWO "-1" 0
   THEN Auto
   THEN (Subst ⌜|n| ~ n⌝ 0⋅ THENA (RWO "absval_pos" 0 THEN 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)))
⊢ (((2 * k) * (n + m)) + (n * |(x m) - y m|) + ((2 * l) * (n + m))) ≤ ((((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)  -  y  n|)  \mleq{}  (((2  *  k)  *  (n  +  m))  +  (|n|  *  |(x  m)  -  y  m|)  +  ((2  *  l)  *  (n  +  m)))
\mvdash{}  (m  *  |(x  n)  -  y  n|)  \mleq{}  ((((2  *  k)  +  (2  *  l))  *  (n  +  m))  +  (n  *  B))


By

---

Latex:
((Subst  \mkleeneopen{}|m|  \msim{}  m\mkleeneclose{}  (-1)\mcdot{}  THENA  (RWO  "absval\_pos"  0  THEN  Auto))
  THEN  RWO  "-1"  0
  THEN  Auto
  THEN  (Subst  \mkleeneopen{}|n|  \msim{}  n\mkleeneclose{}  0\mcdot{}  THENA  (RWO  "absval\_pos"  0  THEN  Auto)))

---

Home Index