---

Step * 1 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))
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|))
BY
{ (RWW "int-triangle-inequality2 -1 -4" 0 THEN Auto) }

---

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))
11.  |b  rem  m|  <  |m|
12.  |b  rem  m|  \mleq{}  (|m|  -  1)
13.  |a  *  (b  rem  m)|  \mleq{}  (|a|  *  (|m|  -  1))
\mvdash{}  |(b  *  (a  rem  m))  -  a  *  (b  rem  m)|  \mleq{}  (|m|  *  (|a|  +  |b|))


By

---

Latex:
(RWW  "int-triangle-inequality2  -1  -4"  0  THEN  Auto)

---

Home Index