---

Step * 1 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))
9. (n * |i|) ≤ |i|
10. 2 ≤ n
11. (|i| * 2) ≤ (|i| * n)
12. |i| = 0 ∈ ℤ
⊢ False
BY
{ (MoveToConcl (-1) THEN (RWO "absval_unfold" (0) THENA Auto) THEN AutoSplit) }

---

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))
9.  (n  *  |i|)  \mleq{}  |i|
10.  2  \mleq{}  n
11.  (|i|  *  2)  \mleq{}  (|i|  *  n)
12.  |i|  =  0
\mvdash{}  False


By

---

Latex:
(MoveToConcl  (-1)  THEN  (RWO  "absval\_unfold"  (0)  THENA  Auto)  THEN  AutoSplit)

---

Home Index