---

Step * 1 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. 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))
BY
{ ((Assert |((m * m) * (x n) * (y n)) - (n * n) * (x m) * (y m)| ≤ (|(m * (x n)) * ((m * (y n)) - n * (y m))|
           + |(n * (y m)) * ((m * (x n)) - n * (x m))|) BY
          ((RWO "int-triangle-inequality<" 0 THENA Auto) THEN RW IntNormC 0 THEN Auto))⋅
   THEN (RWO "-1" 0 THENA Auto)
   THEN Thin (-1)
   THEN (RWO "absval_mul" 0 THENA Auto)⋅
   THEN Unfold `regular-int-seq` 4
   THEN (RW (SweepDnC (HypC 4)) 0 THEN Thin 4 THEN Auto)
   THEN ((Unfold `regular-int-seq` 2 THEN RW (SweepDnC (HypC 2)) 0 THEN Thin 2) THEN Auto)
   THEN (RWO "absval_mul" 0 THENA Auto)) }

1
1. x : ℕ+ ⟶ ℤ
2. y : ℕ+ ⟶ ℤ
3. B : ℕ+
4. b : ℕ+
5. ∀n,m:{b...}.  ((2 * ((m * |x n|) + (n * |y m|))) ≤ ((n * m) * ((4 * B) - 2)))
6. n : {b...}
7. m : {b...}
8. r1 : {r:ℤ| |r| < |2 * n|} 
9. r2 : {r:ℤ| |r| < |2 * m|} 
⊢ ((((|m| * |x n|) * (2 * 1) * (n + m)) + ((|n| * |y m|) * (2 * 1) * (n + 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.  r2  :  \{r:\mBbbZ{}|  |r|  <  |2  *  m|\} 
\mvdash{}  (|((m  *  m)  *  (x  n)  *  (y  n))  -  (n  *  n)  *  (x  m)  *  (y  m)|  +  |(m  *  m)  *  (-r1)|  +  |(n  *  n)  *  r2|) 
    \mleq{}  (|2  *  n  *  m|  *  (2  *  B)  *  (n  +  m))


By

---

Latex:
((Assert  |((m  *  m)  *  (x  n)  *  (y  n))  -  (n  *  n)  *  (x  m)  *  (y  m)|  \mleq{}  (|(m  *  (x  n))
                  *  ((m  *  (y  n))  -  n  *  (y  m))|
                  +  |(n  *  (y  m))  *  ((m  *  (x  n))  -  n  *  (x  m))|)  BY
                ((RWO  "int-triangle-inequality<"  0  THENA  Auto)  THEN  RW  IntNormC  0  THEN  Auto))\mcdot{}
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  Thin  (-1)
  THEN  (RWO  "absval\_mul"  0  THENA  Auto)\mcdot{}
  THEN  Unfold  `regular-int-seq`  4
  THEN  (RW  (SweepDnC  (HypC  4))  0  THEN  Thin  4  THEN  Auto)
  THEN  ((Unfold  `regular-int-seq`  2  THEN  RW  (SweepDnC  (HypC  2))  0  THEN  Thin  2)  THEN  Auto)
  THEN  (RWO  "absval\_mul"  0  THENA  Auto))

---

Home Index