---

Step * 1 of Lemma reg-seq-mul-regular-eventually


1. x : ℕ+ ⟶ ℤ
2. regular-seq(x)
3. y : ℕ+ ⟶ ℤ
4. regular-seq(y)
5. B : ℕ+
6. b : ℕ+
7. ∀n,m:{b...}.  ((2 * ((m * |x n|) + (n * |y m|))) ≤ ((n * m) * ((4 * B) - 2)))
8. n : {b...}
9. m : {b...}
⊢ |(2 * n * m) * ((m * (reg-seq-mul(x;y) n)) - n * (reg-seq-mul(x;y) m))| ≤ (|2 * n * m| * (2 * B) * (n + m))
BY
{ ((Subst ⌜(2 * n * m) * ((m * (reg-seq-mul(x;y) n)) - n * (reg-seq-mul(x;y) m)) ~ ((m * m)
           * (2 * n)
           * (reg-seq-mul(x;y) n)) - (n * n) * (2 * m) * (reg-seq-mul(x;y) m)⌝ 0⋅
    THENA Auto
    )
   THEN RepUR ``reg-seq-mul`` 0
   THEN (RWO "div_rem_sum2" 0 THENA Auto)
   THEN (GenConcl ⌜((x n) * (y n) rem 2 * n) = r1 ∈ {r:ℤ| |r| < |2 * n|} ⌝⋅ THENA Auto)⋅
   THEN (GenConcl ⌜((x m) * (y m) rem 2 * m) = r2 ∈ {r:ℤ| |r| < |2 * m|} ⌝⋅ THENA Auto)⋅)⋅ }

1
1. x : ℕ+ ⟶ ℤ
2. regular-seq(x)
3. y : ℕ+ ⟶ ℤ
4. regular-seq(y)
5. B : ℕ+
6. b : ℕ+
7. ∀n,m:{b...}.  ((2 * ((m * |x n|) + (n * |y m|))) ≤ ((n * m) * ((4 * B) - 2)))
8. n : {b...}
9. m : {b...}
10. r1 : {r:ℤ| |r| < |2 * n|} 
11. ((x n) * (y n) rem 2 * n) = r1 ∈ {r:ℤ| |r| < |2 * n|} 
12. r2 : {r:ℤ| |r| < |2 * m|} 
13. ((x m) * (y m) rem 2 * m) = r2 ∈ {r:ℤ| |r| < |2 * m|} 
⊢ |((m * m) * (((x n) * (y n)) - r1)) - (n * n) * (((x m) * (y m)) - r2)| ≤ (|2 * n * m| * (2 * B) * (n + m))

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
2.  regular-seq(x)
3.  y  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
4.  regular-seq(y)
5.  B  :  \mBbbN{}\msupplus{}
6.  b  :  \mBbbN{}\msupplus{}
7.  \mforall{}n,m:\{b...\}.    ((2  *  ((m  *  |x  n|)  +  (n  *  |y  m|)))  \mleq{}  ((n  *  m)  *  ((4  *  B)  -  2)))
8.  n  :  \{b...\}
9.  m  :  \{b...\}
\mvdash{}  |(2  *  n  *  m)  *  ((m  *  (reg-seq-mul(x;y)  n))  -  n  *  (reg-seq-mul(x;y)  m))|  \mleq{}  (|2  *  n  *  m|
    *  (2  *  B)
    *  (n  +  m))


By

---

Latex:
((Subst  \mkleeneopen{}(2  *  n  *  m)  *  ((m  *  (reg-seq-mul(x;y)  n))  -  n  *  (reg-seq-mul(x;y)  m))  \msim{}  ((m  *  m)
                  *  (2  *  n)
                  *  (reg-seq-mul(x;y)  n))  -  (n  *  n)  *  (2  *  m)  *  (reg-seq-mul(x;y)  m)\mkleeneclose{}  0\mcdot{}
    THENA  Auto
    )
  THEN  RepUR  ``reg-seq-mul``  0
  THEN  (RWO  "div\_rem\_sum2"  0  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}((x  n)  *  (y  n)  rem  2  *  n)  =  r1\mkleeneclose{}\mcdot{}  THENA  Auto)\mcdot{}
  THEN  (GenConcl  \mkleeneopen{}((x  m)  *  (y  m)  rem  2  *  m)  =  r2\mkleeneclose{}\mcdot{}  THENA  Auto)\mcdot{})\mcdot{}

---

Home Index