---

Step * 1 1 1 of Lemma div_bounds_1


1. a : ℤ
2. a ≥ 0 
3. n : ℤ
4. 0 < n
5. a = ((n * (a ÷ n)) + (a rem n)) ∈ ℤ
6. 0 ≤ (a rem n)
7. a rem n < n
8. ¬(0 ≤ (a ÷ n))
9. (n * (a ÷ n)) ≤ ((-1) * n)
⊢ 0 ≤ (a ÷ n)
BY
{ (Add ⌜a rem n⌝ (-1)⋅ THEN RevHypSubst' 5 (-1)) }

1
1. a : ℤ
2. a ≥ 0 
3. n : ℤ
4. 0 < n
5. a = ((n * (a ÷ n)) + (a rem n)) ∈ ℤ
6. 0 ≤ (a rem n)
7. a rem n < n
8. ¬(0 ≤ (a ÷ n))
9. (n * (a ÷ n)) ≤ ((-1) * n)
10. a ≤ (((-1) * n) + (a rem n))
⊢ 0 ≤ (a ÷ n)

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  a  \mgeq{}  0 
3.  n  :  \mBbbZ{}
4.  0  <  n
5.  a  =  ((n  *  (a  \mdiv{}  n))  +  (a  rem  n))
6.  0  \mleq{}  (a  rem  n)
7.  a  rem  n  <  n
8.  \mneg{}(0  \mleq{}  (a  \mdiv{}  n))
9.  (n  *  (a  \mdiv{}  n))  \mleq{}  ((-1)  *  n)
\mvdash{}  0  \mleq{}  (a  \mdiv{}  n)


By

---

Latex:
(Add  \mkleeneopen{}a  rem  n\mkleeneclose{}  (-1)\mcdot{}  THEN  RevHypSubst'  5  (-1))

---

Home Index