---

Step * of Lemma reg-seq-mul-assoc

∀x,y,z:ℝ.  bdd-diff(reg-seq-mul(reg-seq-mul(x;y);z);reg-seq-mul(x;reg-seq-mul(y;z)))
BY
{ (Auto
   THEN RepUR ``reg-seq-mul bdd-diff`` 0
   THEN With ⌜(2 * imax(canonical-bound(x);canonical-bound(z))) + 2⌝ (D 0)⋅
   THEN Auto
   THEN (Using [`n', ⌜|2 * n|⌝] (BLemma `mul_cancel_in_le`)⋅ THENA Auto)
   THEN (RWO "absval_mul<" 0 THENA Auto)
   THEN (RWO "left_mul_subtract_distrib" 0 THENA Auto)
   THEN (RWO "div_rem_sum2" 0 THENA Auto)) }

1
1. x : ℝ
2. y : ℝ
3. z : ℝ
4. n : ℕ+
⊢ |((((x n) * (y n)) ÷ 2 * n) * (z n)) - (((x n) * (y n)) ÷ 2 * n) * (z n) rem 2 * n - ((x n)
  * (((y n) * (z n)) ÷ 2 * n)) - (x n) * (((y n) * (z n)) ÷ 2 * n) rem 2 * n| ≤ (|2 * n|
  * ((2 * imax(canonical-bound(x);canonical-bound(z))) + 2))

---

Latex:

---

Latex:
\mforall{}x,y,z:\mBbbR{}.    bdd-diff(reg-seq-mul(reg-seq-mul(x;y);z);reg-seq-mul(x;reg-seq-mul(y;z)))


By

---

Latex:
(Auto
  THEN  RepUR  ``reg-seq-mul  bdd-diff``  0
  THEN  With  \mkleeneopen{}(2  *  imax(canonical-bound(x);canonical-bound(z)))  +  2\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  (Using  [`n',  \mkleeneopen{}|2  *  n|\mkleeneclose{}]  (BLemma  `mul\_cancel\_in\_le`)\mcdot{}  THENA  Auto)
  THEN  (RWO  "absval\_mul<"  0  THENA  Auto)
  THEN  (RWO  "left\_mul\_subtract\_distrib"  0  THENA  Auto)
  THEN  (RWO  "div\_rem\_sum2"  0  THENA  Auto))

---

Home Index