---

Step * 2 1 1 of Lemma div_mono1

.....assertion..... 
1. i : ℕ
2. k : ℕ
3. 0 < i
4. 1 < k
5. ¬i < k
6. i = (((i ÷ k) * k) + (i rem k)) ∈ ℤ
7. (0 ≤ (i rem k)) ∧ i rem k < k
⊢ ((i ÷ k) * k) ≤ i
BY
{ Auto' }

---

Latex:

---

Latex:
.....assertion..... 
1.  i  :  \mBbbN{}
2.  k  :  \mBbbN{}
3.  0  <  i
4.  1  <  k
5.  \mneg{}i  <  k
6.  i  =  (((i  \mdiv{}  k)  *  k)  +  (i  rem  k))
7.  (0  \mleq{}  (i  rem  k))  \mwedge{}  i  rem  k  <  k
\mvdash{}  ((i  \mdiv{}  k)  *  k)  \mleq{}  i


By

---

Latex:
Auto'

---

Home Index