---

Step * 1 of Lemma div_absval_bound


1. M : ℕ+
2. z : ℤ
3. n : ℕ
4. |z| ≤ (n * M)
5. ¬(n = 0 ∈ ℤ)
6. 1 ≤ n
7. (M * 1) ≤ (M * n)
⊢ |z ÷ M| ≤ n
BY
{ ((Mul ⌜M⌝ 0⋅ THENA Auto)
   THEN (Subst' M * |z ÷ M| ~ |M * (z ÷ M)| 0 THENA (Auto THEN (RWO  "absval_mul" 0 THENM EqCDA) THEN Auto))
   THEN (InstLemma `div_rem_sum` [⌜z⌝;⌜M⌝]⋅ THENA Auto)
   THEN (Subst' M * (z ÷ M) ~ z - z rem M 0 THENA Auto)
   THEN ((Decide ⌜0 ≤ z⌝⋅ THENA Auto)
         THENL [(InstLemma  `rem_bounds_1` [⌜z⌝;⌜M⌝]⋅ THEN Auto); (InstLemma  `rem_bounds_2` [⌜z⌝;⌜M⌝]⋅ THEN Auto)]
   )
   THEN MoveToConcl 4
   THEN (RWO  "absval_unfold" 0 THENA Auto)
   THEN RepeatFor 2 (AutoSplit)
   THEN Auto) }

---

Latex:

---

Latex:

1.  M  :  \mBbbN{}\msupplus{}
2.  z  :  \mBbbZ{}
3.  n  :  \mBbbN{}
4.  |z|  \mleq{}  (n  *  M)
5.  \mneg{}(n  =  0)
6.  1  \mleq{}  n
7.  (M  *  1)  \mleq{}  (M  *  n)
\mvdash{}  |z  \mdiv{}  M|  \mleq{}  n


By

---

Latex:
((Mul  \mkleeneopen{}M\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (Subst'  M  *  |z  \mdiv{}  M|  \msim{}  |M  *  (z  \mdiv{}  M)|  0
              THENA  (Auto  THEN  (RWO    "absval\_mul"  0  THENM  EqCDA)  THEN  Auto)
              )
  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}M\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Subst'  M  *  (z  \mdiv{}  M)  \msim{}  z  -  z  rem  M  0  THENA  Auto)
  THEN  ((Decide  \mkleeneopen{}0  \mleq{}  z\mkleeneclose{}\mcdot{}  THENA  Auto)
              THENL  [(InstLemma    `rem\_bounds\_1`  [\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}M\mkleeneclose{}]\mcdot{}  THEN  Auto)
                          ;  (InstLemma    `rem\_bounds\_2`  [\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}M\mkleeneclose{}]\mcdot{}  THEN  Auto)]
  )
  THEN  MoveToConcl  4
  THEN  (RWO    "absval\_unfold"  0  THENA  Auto)
  THEN  RepeatFor  2  (AutoSplit)
  THEN  Auto)

---

Home Index