Step * 1 1 of Lemma mul-div-bounds


1. : ℤ
2. : ℤ
3. : ℤ-o
4. (((b ÷ m) m) (b rem m)) ∈ ℤ
5. (a b) (a (((b ÷ m) m) (b rem m))) ∈ ℤ
6. (((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)) (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. : ℤ
2. : ℤ
3. : ℤ-o
4. (((b ÷ m) m) (b rem m)) ∈ ℤ
5. (a b) (a (((b ÷ m) m) (b rem m))) ∈ ℤ
6. (((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)) (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