---

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

No Annotations
∀[x,y:ℝ].
  ∀B,b:ℕ+.
    ∀n,m:{b...}.  (|(m * (reg-seq-mul(x;y) n)) - n * (reg-seq-mul(x;y) m)| ≤ ((2 * B) * (n + m))) 
    supposing ∀n,m:{b...}.  ((2 * ((m * |x n|) + (n * |y m|))) ≤ ((n * m) * ((4 * B) - 2)))
BY
{ (Auto
   THEN D 2
   THEN D 1
   THEN Unhide
   THEN Auto
   THEN (Using [`n', ⌜|2 * n * m|⌝] (BLemma `mul_cancel_in_le`)⋅ THENA Auto)⋅
   THEN (RWO "absval_mul<" 0 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...}
⊢ |(2 * n * m) * ((m * (reg-seq-mul(x;y) n)) - n * (reg-seq-mul(x;y) m))| ≤ (|2 * n * m| * (2 * B) * (n + m))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[x,y:\mBbbR{}].
    \mforall{}B,b:\mBbbN{}\msupplus{}.
        \mforall{}n,m:\{b...\}.    (|(m  *  (reg-seq-mul(x;y)  n))  -  n  *  (reg-seq-mul(x;y)  m)|  \mleq{}  ((2  *  B)  *  (n  +  m))) 
        supposing  \mforall{}n,m:\{b...\}.    ((2  *  ((m  *  |x  n|)  +  (n  *  |y  m|)))  \mleq{}  ((n  *  m)  *  ((4  *  B)  -  2)))


By

---

Latex:
(Auto
  THEN  D  2
  THEN  D  1
  THEN  Unhide
  THEN  Auto
  THEN  (Using  [`n',  \mkleeneopen{}|2  *  n  *  m|\mkleeneclose{}]  (BLemma  `mul\_cancel\_in\_le`)\mcdot{}  THENA  Auto)\mcdot{}
  THEN  (RWO  "absval\_mul<"  0  THENA  Auto))\mcdot{}

---

Home Index