---

Step * 1 1 of Lemma div_bounds_1


1. a : ℤ
2. a ≥ 0 
3. n : ℤ
4. 0 < n
5. a = (((a ÷ n) * n) + (a rem n)) ∈ ℤ
6. (0 ≤ (a rem n)) ∧ a rem n < n
7. ¬(0 ≤ (a ÷ n))
8. (n * (a ÷ n)) ≤ (n * (-1))
⊢ 0 ≤ (a ÷ n)
BY
{ (((RW IntNormC 5 THENM RW IntNormC (-1)) THENA Auto) THEN SplitAndHyps) }

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)

---

Latex:

---

Latex:

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


By

---

Latex:
(((RW  IntNormC  5  THENM  RW  IntNormC  (-1))  THENA  Auto)  THEN  SplitAndHyps)

---

Home Index