---

Step * of Lemma mul-div-bounds

∀[a,b:ℤ]. ∀[m:ℤ-o].  (|(a * (b ÷ m)) - b * (a ÷ m)| ≤ (|a| + |b|))
BY
{ (Auto
   THEN ((InstLemma `div_rem_sum` [⌜b⌝;⌜m⌝]⋅ THENA Auto) THEN Mul ⌜a⌝ (-1)⋅)
   THEN (InstLemma `div_rem_sum` [⌜a⌝;⌜m⌝]⋅ THENA Auto)
   THEN Mul ⌜b⌝ (-1)⋅
   THEN Mul ⌜|m|⌝ 0⋅
   THEN (RWO "absval_mul<" 0 THENA Auto)
   THEN (Subst' (m * ((a * (b ÷ m)) - b * (a ÷ m))) = ((b * (a rem m)) - a * (b rem m)) ∈ ℤ 0 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))) ∈ ℤ
⊢ |(b * (a rem m)) - a * (b rem m)| ≤ (|m| * (|a| + |b|))

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbZ{}].  \mforall{}[m:\mBbbZ{}\msupminus{}\msupzero{}].    (|(a  *  (b  \mdiv{}  m))  -  b  *  (a  \mdiv{}  m)|  \mleq{}  (|a|  +  |b|))


By

---

Latex:
(Auto
  THEN  ((InstLemma  `div\_rem\_sum`  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  Mul  \mkleeneopen{}a\mkleeneclose{}  (-1)\mcdot{})
  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Mul  \mkleeneopen{}b\mkleeneclose{}  (-1)\mcdot{}
  THEN  Mul  \mkleeneopen{}|m|\mkleeneclose{}  0\mcdot{}
  THEN  (RWO  "absval\_mul<"  0  THENA  Auto)
  THEN  (Subst'  (m  *  ((a  *  (b  \mdiv{}  m))  -  b  *  (a  \mdiv{}  m)))  =  ((b  *  (a  rem  m))  -  a  *  (b  rem  m))  0  THENA  Auto))

---

Home Index