---

Step * 1 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)
5. |i| rem n < n
6. ¬|i| ÷ n < |i|
7. |i| ≤ (|i| ÷ n)
8. (n * |i|) ≤ (n * (|i| ÷ n))
⊢ False
BY
{ ((Assert (n * |i|) ≤ |i| BY
          Auto)⋅
   THEN (Assert 2 ≤ n BY
               Auto)
   THEN Mul ⌜|i|⌝ (-1)⋅
   THEN Auto'
   THEN Assert ⌜|i| = 0 ∈ ℤ⌝⋅
   THEN 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))
9. (n * |i|) ≤ |i|
10. 2 ≤ n
11. (|i| * 2) ≤ (|i| * n)
12. |i| = 0 ∈ ℤ
⊢ 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)
5.  |i|  rem  n  <  n
6.  \mneg{}|i|  \mdiv{}  n  <  |i|
7.  |i|  \mleq{}  (|i|  \mdiv{}  n)
8.  (n  *  |i|)  \mleq{}  (n  *  (|i|  \mdiv{}  n))
\mvdash{}  False


By

---

Latex:
((Assert  (n  *  |i|)  \mleq{}  |i|  BY
                Auto)\mcdot{}
  THEN  (Assert  2  \mleq{}  n  BY
                          Auto)
  THEN  Mul  \mkleeneopen{}|i|\mkleeneclose{}  (-1)\mcdot{}
  THEN  Auto'
  THEN  Assert  \mkleeneopen{}|i|  =  0\mkleeneclose{}\mcdot{}
  THEN  Auto')

---

Home Index