---

Step * 1 1 of Lemma mul-div-bounds


1. a : ℤ
2. b : ℤ
3. m : ℤ-o
4. b = (((b ÷ m) * m) + (b rem m)) ∈ ℤ
5. (a * b) = (a * (((b ÷ m) * m) + (b rem m))) ∈ ℤ
6. a = (((a ÷ m) * m) + (a rem m)) ∈ ℤ
7. (b * a) = (b * (((a ÷ m) * m) + (a rem m))) ∈ ℤ
8. |a rem m| < |m|
9. |a rem m| ≤ (|m| - 1)
10. |b * (a rem m)| ≤ (|b| * (|m| - 1))
⊢ |(b * (a rem m)) - a * (b rem m)| ≤ (|m| * (|a| + |b|))
BY
{ ((InstLemma `rem_bounds_absval` [⌜m⌝;⌜b⌝]⋅ THENA Auto)
   THEN (Assert |b rem m| ≤ (|m| - 1) BY
               Auto)
   THEN Mul ⌜|a|⌝ (-1)⋅
   THEN (RWO "absval_mul<" (-1) THENA Auto)) }

1
1. a : ℤ
2. b : ℤ
3. m : ℤ-o
4. b = (((b ÷ m) * m) + (b rem m)) ∈ ℤ
5. (a * b) = (a * (((b ÷ m) * m) + (b rem m))) ∈ ℤ
6. a = (((a ÷ m) * m) + (a rem m)) ∈ ℤ
7. (b * a) = (b * (((a ÷ m) * m) + (a rem m))) ∈ ℤ
8. |a rem m| < |m|
9. |a rem m| ≤ (|m| - 1)
10. |b * (a rem m)| ≤ (|b| * (|m| - 1))
11. |b rem m| < |m|
12. |b rem m| ≤ (|m| - 1)
13. |a * (b rem m)| ≤ (|a| * (|m| - 1))
⊢ |(b * (a rem m)) - a * (b rem m)| ≤ (|m| * (|a| + |b|))

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  b  :  \mBbbZ{}
3.  m  :  \mBbbZ{}\msupminus{}\msupzero{}
4.  b  =  (((b  \mdiv{}  m)  *  m)  +  (b  rem  m))
5.  (a  *  b)  =  (a  *  (((b  \mdiv{}  m)  *  m)  +  (b  rem  m)))
6.  a  =  (((a  \mdiv{}  m)  *  m)  +  (a  rem  m))
7.  (b  *  a)  =  (b  *  (((a  \mdiv{}  m)  *  m)  +  (a  rem  m)))
8.  |a  rem  m|  <  |m|
9.  |a  rem  m|  \mleq{}  (|m|  -  1)
10.  |b  *  (a  rem  m)|  \mleq{}  (|b|  *  (|m|  -  1))
\mvdash{}  |(b  *  (a  rem  m))  -  a  *  (b  rem  m)|  \mleq{}  (|m|  *  (|a|  +  |b|))


By

---

Latex:
((InstLemma  `rem\_bounds\_absval`  [\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  |b  rem  m|  \mleq{}  (|m|  -  1)  BY
                          Auto)
  THEN  Mul  \mkleeneopen{}|a|\mkleeneclose{}  (-1)\mcdot{}
  THEN  (RWO  "absval\_mul<"  (-1)  THENA  Auto))

---

Home Index