---

Step * 1 1 of Lemma regular-consistency


1. x : ℕ+ ⟶ ℤ
2. regular-seq(x)
3. y : ℕ+ ⟶ ℤ
4. regular-seq(y)
5. n : ℕ+
6. m : ℕ+
⊢ (m * |(x n) - y n|) ≤ ((n * |(x m) - y m|) + (4 * n) + (4 * m))
BY
{ (Assert |(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
         ((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. regular-seq(x)
3. y : ℕ+ ⟶ ℤ
4. regular-seq(y)
5. n : ℕ+
6. m : ℕ+
7. |(m * (x n)) - m * (y n)| ≤ (|(m * (x n)) - n * (x m)| + |(n * (x m)) - n * (y m)| + |(m * (y n)) - n * (y m)|)
⊢ (m * |(x n) - y n|) ≤ ((n * |(x m) - y m|) + (4 * n) + (4 * m))

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
2.  regular-seq(x)
3.  y  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
4.  regular-seq(y)
5.  n  :  \mBbbN{}\msupplus{}
6.  m  :  \mBbbN{}\msupplus{}
\mvdash{}  (m  *  |(x  n)  -  y  n|)  \mleq{}  ((n  *  |(x  m)  -  y  m|)  +  (4  *  n)  +  (4  *  m))


By

---

Latex:
(Assert  |(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
              ((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