---

Step * 1 of Lemma absval_div_decreases


1. n : {2...}
2. i : ℤ-o
3. |i| = (((|i| ÷ n) * n) + (|i| rem n)) ∈ ℤ
4. (0 ≤ (|i| rem n)) ∧ |i| rem n < n
⊢ |i| ÷ n < |i|
BY
{ ((SupposeNot THEN Auto)⋅
   THEN (Assert ⌜False⌝⋅ THEN Auto)
   THEN (Assert |i| ≤ (|i| ÷ n) BY
               Auto)
   THEN (Mul ⌜n⌝ (-1)⋅ THENA Auto)) }

1
1. n : {2...}
2. i : ℤ-o
3. |i| = (((|i| ÷ n) * n) + (|i| rem n)) ∈ ℤ
4. 0 ≤ (|i| rem n)
5. |i| rem n < n
6. ¬|i| ÷ n < |i|
7. |i| ≤ (|i| ÷ n)
8. (n * |i|) ≤ (n * (|i| ÷ n))
⊢ False

---

Latex:

---

Latex:

1.  n  :  \{2...\}
2.  i  :  \mBbbZ{}\msupminus{}\msupzero{}
3.  |i|  =  (((|i|  \mdiv{}  n)  *  n)  +  (|i|  rem  n))
4.  (0  \mleq{}  (|i|  rem  n))  \mwedge{}  |i|  rem  n  <  n
\mvdash{}  |i|  \mdiv{}  n  <  |i|


By

---

Latex:
((SupposeNot  THEN  Auto)\mcdot{}
  THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (Assert  |i|  \mleq{}  (|i|  \mdiv{}  n)  BY
                          Auto)
  THEN  (Mul  \mkleeneopen{}n\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto))

---

Home Index