---

Step * of Lemma reg-seq-mul_functionality_wrt_bdd-diff

∀x1:ℝ. ∀[x2,y1:ℕ+ ⟶ ℤ].  ∀y2:ℝ. (bdd-diff(y1;y2) ⇒ bdd-diff(x1;x2) ⇒ bdd-diff(reg-seq-mul(x1;y1);reg-seq-mul(x2;y2)))
BY
{ (Auto
   THEN All (Unfold `bdd-diff`)
   THEN ExRepD
   THEN RepUR ``reg-seq-mul`` 0
   THEN With ⌜2 + (B1 * canonical-bound(x1)) + (B * canonical-bound(y2))⌝ (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)
   THEN (GenConcl ⌜((x1 n) * (y1 n) rem 2 * n) = r1 ∈ {r:ℤ| |r| < |2 * n|} ⌝⋅ THENA Auto)
   THEN (GenConcl ⌜((x2 n) * (y2 n) rem 2 * n) = r2 ∈ {r:ℤ| |r| < |2 * n|} ⌝⋅ THENA Auto)) }

1
1. x1 : ℝ
2. x2 : ℕ+ ⟶ ℤ
3. y1 : ℕ+ ⟶ ℤ
4. y2 : ℝ
5. B1 : ℕ
6. ∀n:ℕ+. (|(y1 n) - y2 n| ≤ B1)
7. B : ℕ
8. ∀n:ℕ+. (|(x1 n) - x2 n| ≤ B)
9. n : ℕ+
10. r1 : {r:ℤ| |r| < |2 * n|} 
11. ((x1 n) * (y1 n) rem 2 * n) = r1 ∈ {r:ℤ| |r| < |2 * n|} 
12. r2 : {r:ℤ| |r| < |2 * n|} 
13. ((x2 n) * (y2 n) rem 2 * n) = r2 ∈ {r:ℤ| |r| < |2 * n|} 
⊢ |((x1 n) * (y1 n)) - r1 - ((x2 n) * (y2 n)) - r2| ≤ (|2 * n|
  * (2 + (B1 * canonical-bound(x1)) + (B * canonical-bound(y2))))

---

Latex:

---

Latex:
\mforall{}x1:\mBbbR{}
    \mforall{}[x2,y1:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}].
        \mforall{}y2:\mBbbR{}.  (bdd-diff(y1;y2)  {}\mRightarrow{}  bdd-diff(x1;x2)  {}\mRightarrow{}  bdd-diff(reg-seq-mul(x1;y1);reg-seq-mul(x2;y2)))


By

---

Latex:
(Auto
  THEN  All  (Unfold  `bdd-diff`)
  THEN  ExRepD
  THEN  RepUR  ``reg-seq-mul``  0
  THEN  With  \mkleeneopen{}2  +  (B1  *  canonical-bound(x1))  +  (B  *  canonical-bound(y2))\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  (Using  [`n',  \mkleeneopen{}|2  *  n|\mkleeneclose{}]  (BLemma  `mul\_cancel\_in\_le`)\mcdot{}  THENA  Auto)\mcdot{}
  THEN  (RWO  "absval\_mul<"  0  THENA  Auto)
  THEN  (RWO  "left\_mul\_subtract\_distrib"  0  THENA  Auto)
  THEN  (RWO  "div\_rem\_sum2"  0  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}((x1  n)  *  (y1  n)  rem  2  *  n)  =  r1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}((x2  n)  *  (y2  n)  rem  2  *  n)  =  r2\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index