Step
*
8
of Lemma
div_floor_bounds
1. a : ℤ
2. n : ℤ-o
3. v : ℤ@i
4. (a ÷ n) = v ∈ ℤ
5. v1 : ℤ@i
6. ¬v1 < 1
7. (a rem n) = v1 ∈ ℤ
8. |v1| < |n|
9. a = ((v * n) + v1) ∈ ℤ
10. n < 0
11. n < 0
12. ((v - 1) + 1) * n < (v * n) + v1
⊢ ((v * n) + v1) ≤ ((v - 1) * n)
BY
{ TACTIC:Assert ⌜v1 < -n⌝⋅ }
1
.....assertion.....
1. a : ℤ
2. n : ℤ-o
3. v : ℤ@i
4. (a ÷ n) = v ∈ ℤ
5. v1 : ℤ@i
6. ¬v1 < 1
7. (a rem n) = v1 ∈ ℤ
8. |v1| < |n|
9. a = ((v * n) + v1) ∈ ℤ
10. n < 0
11. n < 0
12. ((v - 1) + 1) * n < (v * n) + v1
⊢ v1 < -n
2
1. a : ℤ
2. n : ℤ-o
3. v : ℤ@i
4. (a ÷ n) = v ∈ ℤ
5. v1 : ℤ@i
6. ¬v1 < 1
7. (a rem n) = v1 ∈ ℤ
8. |v1| < |n|
9. a = ((v * n) + v1) ∈ ℤ
10. n < 0
11. n < 0
12. ((v - 1) + 1) * n < (v * n) + v1
13. v1 < -n
⊢ ((v * n) + v1) ≤ ((v - 1) * n)
Latex:
Latex:
1. a : \mBbbZ{}
2. n : \mBbbZ{}\msupminus{}\msupzero{}
3. v : \mBbbZ{}@i
4. (a \mdiv{} n) = v
5. v1 : \mBbbZ{}@i
6. \mneg{}v1 < 1
7. (a rem n) = v1
8. |v1| < |n|
9. a = ((v * n) + v1)
10. n < 0
11. n < 0
12. ((v - 1) + 1) * n < (v * n) + v1
\mvdash{} ((v * n) + v1) \mleq{} ((v - 1) * n)
By
Latex:
TACTIC:Assert \mkleeneopen{}v1 < -n\mkleeneclose{}\mcdot{}
Home
Index