---

Step * 1 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...}
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))
BY
{ ((Assert |((m * m) * (((x n) * (y n)) - r1)) - (n * n) * (((x m) * (y m)) - r2)| ≤ (|((m * m) * (x n) * (y n)) - (n
                                                                                                                   * n)
                                                                                      * (x m)
                                                                                      * (y m)|
           + |(m * m) * (-r1)|
           + |(n * n) * r2|) BY
          (RepeatFor 2 ((RWO "int-triangle-inequality<" 0 THENA Auto)) THEN RW IntNormC 0 THEN Auto))⋅
   THEN RWO "-1" 0
   THEN Auto
   THEN RepeatFor 2 (Thin (-1))
   THEN Thin (-2)) }

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. r2 : {r:ℤ| |r| < |2 * m|} 
⊢ (|((m * m) * (x n) * (y n)) - (n * n) * (x m) * (y m)| + |(m * m) * (-r1)| + |(n * n) * 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...\}
10.  r1  :  \{r:\mBbbZ{}|  |r|  <  |2  *  n|\} 
11.  ((x  n)  *  (y  n)  rem  2  *  n)  =  r1
12.  r2  :  \{r:\mBbbZ{}|  |r|  <  |2  *  m|\} 
13.  ((x  m)  *  (y  m)  rem  2  *  m)  =  r2
\mvdash{}  |((m  *  m)  *  (((x  n)  *  (y  n))  -  r1))  -  (n  *  n)  *  (((x  m)  *  (y  m))  -  r2)|  \mleq{}  (|2  *  n  *  m|
    *  (2  *  B)
    *  (n  +  m))


By

---

Latex:
((Assert  |((m  *  m)  *  (((x  n)  *  (y  n))  -  r1))  -  (n  *  n)  *  (((x  m)  *  (y  m))  -  r2)|  \mleq{}  (|((m  *  m)
                                                                                                                                                                        *  (x  n)
                                                                                                                                                                        *  (y  n))  -  (n
                                                                                                                                                                                              *  n)
                                                                                                                                                                        *  (x  m)
                                                                                                                                                                        *  (y  m)|
                  +  |(m  *  m)  *  (-r1)|
                  +  |(n  *  n)  *  r2|)  BY
                (RepeatFor  2  ((RWO  "int-triangle-inequality<"  0  THENA  Auto))  THEN  RW  IntNormC  0  THEN  Auto))\mcdot{}
  THEN  RWO  "-1"  0
  THEN  Auto
  THEN  RepeatFor  2  (Thin  (-1))
  THEN  Thin  (-2))

---

Home Index