---

Step * 1 2 2 of Lemma rmul-distrib1


1. x : ℝ
2. y : ℝ
3. z : ℝ
4. bdd-diff(reg-seq-list-add([x * y; x * z]);reg-seq-list-add([reg-seq-mul(x;y); reg-seq-mul(x;z)]))
⊢ bdd-diff(reg-seq-mul(reg-seq-list-add([y; z]);x);reg-seq-list-add([reg-seq-mul(x;y); reg-seq-mul(x;z)]))
BY
{ (((RWO "reg-seq-list-add-as-l_sum" 0 THENA Auto) THEN Reduce 0)
   THEN RepUR ``bdd-diff reg-seq-mul reg-seq-list-add`` 0
   THEN With ⌜3⌝ (D 0)⋅
   THEN Auto
   THEN (Using [`n',⌜|2 * n|⌝] (BLemma `mul_cancel_in_le`)⋅ THENA Auto)
   THEN (RWO "absval_mul<" 0 THENA Auto)
   THEN (RWW "left_mul_subtract_distrib left_mul_add_distrib" 0 THENA Auto)
   THEN (RWO "div_rem_sum2" 0 THENA Auto)
   THEN (GenConcl ⌜(((y n) + (z n) + 0) * (x n) rem 2 * n) = r1 ∈ {r:ℤ| |r| < |2 * n|} ⌝⋅ THENA Auto)
   THEN (GenConcl ⌜((x n) * (y n) rem 2 * n) = r2 ∈ {r:ℤ| |r| < |2 * n|} ⌝⋅ THENA Auto)
   THEN (GenConcl ⌜((x n) * (z n) rem 2 * n) = r3 ∈ {r:ℤ| |r| < |2 * n|} ⌝⋅ THENA Auto)
   THEN (RW IntNormC 0 THENA Auto)) }

1
1. x : ℝ
2. y : ℝ
3. z : ℝ
4. bdd-diff(reg-seq-list-add([x * y; x * z]);reg-seq-list-add([reg-seq-mul(x;y); reg-seq-mul(x;z)]))
5. n : ℕ+
6. r1 : {r:ℤ| |r| < |2 * n|} 
7. (((y n) + (z n) + 0) * (x n) rem 2 * n) = r1 ∈ {r:ℤ| |r| < |2 * n|} 
8. r2 : {r:ℤ| |r| < |2 * n|} 
9. ((x n) * (y n) rem 2 * n) = r2 ∈ {r:ℤ| |r| < |2 * n|} 
10. r3 : {r:ℤ| |r| < |2 * n|} 
11. ((x n) * (z n) rem 2 * n) = r3 ∈ {r:ℤ| |r| < |2 * n|} 
⊢ |((-1) * r1) + r2 + r3| ≤ (3 * |2 * n|)

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  z  :  \mBbbR{}
4.  bdd-diff(reg-seq-list-add([x  *  y;  x  *  z]);reg-seq-list-add([reg-seq-mul(x;y);  reg-seq-mul(x;z)]))
\mvdash{}  bdd-diff(reg-seq-mul(reg-seq-list-add([y;  z]);x);reg-seq-list-add([reg-seq-mul(x;y);
                                                                                                                                          reg-seq-mul(x;z)]))


By

---

Latex:
(((RWO  "reg-seq-list-add-as-l\_sum"  0  THENA  Auto)  THEN  Reduce  0)
  THEN  RepUR  ``bdd-diff  reg-seq-mul  reg-seq-list-add``  0
  THEN  With  \mkleeneopen{}3\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  (RWW  "left\_mul\_subtract\_distrib  left\_mul\_add\_distrib"  0  THENA  Auto)
  THEN  (RWO  "div\_rem\_sum2"  0  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(((y  n)  +  (z  n)  +  0)  *  (x  n)  rem  2  *  n)  =  r1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}((x  n)  *  (y  n)  rem  2  *  n)  =  r2\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}((x  n)  *  (z  n)  rem  2  *  n)  =  r3\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (RW  IntNormC  0  THENA  Auto))

---

Home Index