---

Step * 1 2 of Lemma bdd-diff-regular


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)|))
11. ∀m:ℕ+. ((m * |(x n) - y n|) ≤ ((((2 * k) + (2 * l)) * (n + m)) + (n * B)))
⊢ |(x n) - y n| ≤ ((2 * k) + (2 * l))
BY
{ (((SupposeNot THEN Auto) THEN Assert ⌜False⌝⋅ THEN Auto)
   THEN (Assert ∀m:ℕ+. (m ≤ ((((2 * k) + (2 * l)) * n) + (n * B))) BY
               (((Assert ⌜(1 + (2 * k) + (2 * l)) ≤ |(x n) - y n|⌝⋅ THENA Auto') THEN (RWO "-1<" (-3) THENA Auto))
                THEN ParallelOp (-3)
                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)|))
11. ∀m:ℕ+. ((m * |(x n) - y n|) ≤ ((((2 * k) + (2 * l)) * (n + m)) + (n * B)))
12. ¬(|(x n) - y n| ≤ ((2 * k) + (2 * l)))
13. ∀m:ℕ+. (m ≤ ((((2 * k) + (2 * l)) * n) + (n * B)))
⊢ False

---

Latex:

---

Latex:

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


By

---

Latex:
(((SupposeNot  THEN  Auto)  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (Assert  \mforall{}m:\mBbbN{}\msupplus{}.  (m  \mleq{}  ((((2  *  k)  +  (2  *  l))  *  n)  +  (n  *  B)))  BY
                          (((Assert  \mkleeneopen{}(1  +  (2  *  k)  +  (2  *  l))  \mleq{}  |(x  n)  -  y  n|\mkleeneclose{}\mcdot{}  THENA  Auto')
                              THEN  (RWO  "-1<"  (-3)  THENA  Auto)
                              )
                            THEN  ParallelOp  (-3)
                            THEN  Auto'))
  )\mcdot{}

---

Home Index