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