---

Step * of Lemma bdd-diff-regular

∀[x,y:ℕ+ ⟶ ℤ]. ∀[k,l:ℕ+].
  (∀n:ℕ+. (|(x n) - y n| ≤ ((2 * k) + (2 * l)))) supposing (bdd-diff(x;y) and k-regular-seq(x) and l-regular-seq(y))
BY
{ (Auto
   THEN D -2
   THEN (Assert ∀m:ℕ+
                  (|(m * (x n)) - m * (y n)| ≤ (|(m * (x n)) - n * (x m)|
                   + |(n * (x m)) - n * (y m)|
                   + |(m * (y n)) - n * (y m)|)) BY
               (Auto
                THEN (RW (AddrC [2;2;1] (LemmaC `absval_sym`)) 0 THENA Auto)
                THEN ((RWO "int-triangle-inequality<" 0 THENA Auto)
                      THEN (RW (AddrC [2;2] (LemmaC `absval_sym`)) 0 THENA Auto)
                      THEN (RWO "int-triangle-inequality<" 0 THENA Auto)
                      THEN RW IntNormC 0
                      THEN Auto)⋅))) }

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

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[k,l:\mBbbN{}\msupplus{}].
    (\mforall{}n:\mBbbN{}\msupplus{}.  (|(x  n)  -  y  n|  \mleq{}  ((2  *  k)  +  (2  *  l))))  supposing 
          (bdd-diff(x;y)  and 
          k-regular-seq(x)  and 
          l-regular-seq(y))


By

---

Latex:
(Auto
  THEN  D  -2
  THEN  (Assert  \mforall{}m:\mBbbN{}\msupplus{}
                                (|(m  *  (x  n))  -  m  *  (y  n)|  \mleq{}  (|(m  *  (x  n))  -  n  *  (x  m)|
                                  +  |(n  *  (x  m))  -  n  *  (y  m)|
                                  +  |(m  *  (y  n))  -  n  *  (y  m)|))  BY
                          (Auto
                            THEN  (RW  (AddrC  [2;2;1]  (LemmaC  `absval\_sym`))  0  THENA  Auto)
                            THEN  ((RWO  "int-triangle-inequality<"  0  THENA  Auto)
                                        THEN  (RW  (AddrC  [2;2]  (LemmaC  `absval\_sym`))  0  THENA  Auto)
                                        THEN  (RWO  "int-triangle-inequality<"  0  THENA  Auto)
                                        THEN  RW  IntNormC  0
                                        THEN  Auto)\mcdot{})))

---

Home Index