---

Step * 1 of Lemma bdd-diff-add


1. f1 : ℕ+ ⟶ ℤ
2. f2 : ℕ+ ⟶ ℤ
3. g1 : ℕ+ ⟶ ℤ
4. g2 : ℕ+ ⟶ ℤ
5. B1 : ℕ
6. ∀n:ℕ+. (|(f1 n) - f2 n| ≤ B1)
7. B : ℕ
8. ∀n:ℕ+. (|(g1 n) - g2 n| ≤ B)
9. n : ℕ+
⊢ |(f1[n] + g1[n]) - f2[n] + g2[n]| ≤ (B + B1)
BY
{ ((Assert |(f1[n] + g1[n]) - f2[n] + g2[n]| ≤ (|f1[n] - f2[n]| + |g1[n] - g2[n]|) BY
          (RWO "int-triangle-inequality<" 0 THEN Auto))
   THEN RWO "-1" 0
   THEN Auto
   THEN RWO "6 8" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  f1  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
2.  f2  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  g1  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
4.  g2  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
5.  B1  :  \mBbbN{}
6.  \mforall{}n:\mBbbN{}\msupplus{}.  (|(f1  n)  -  f2  n|  \mleq{}  B1)
7.  B  :  \mBbbN{}
8.  \mforall{}n:\mBbbN{}\msupplus{}.  (|(g1  n)  -  g2  n|  \mleq{}  B)
9.  n  :  \mBbbN{}\msupplus{}
\mvdash{}  |(f1[n]  +  g1[n])  -  f2[n]  +  g2[n]|  \mleq{}  (B  +  B1)


By

---

Latex:
((Assert  |(f1[n]  +  g1[n])  -  f2[n]  +  g2[n]|  \mleq{}  (|f1[n]  -  f2[n]|  +  |g1[n]  -  g2[n]|)  BY
                (RWO  "int-triangle-inequality<"  0  THEN  Auto))
  THEN  RWO  "-1"  0
  THEN  Auto
  THEN  RWO  "6  8"  0
  THEN  Auto)

---

Home Index