---

Step * 2 1 2 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
8. ((i ÷ k) * k) ≤ i
⊢ ((i ÷ k) * 2) ≤ ((i ÷ k) * k)
BY
{ (Assert 2 ≤ k BY
         Auto) }

1
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
8. ((i ÷ k) * k) ≤ i
9. 2 ≤ k
⊢ ((i ÷ k) * 2) ≤ ((i ÷ k) * k)

---

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
8.  ((i  \mdiv{}  k)  *  k)  \mleq{}  i
\mvdash{}  ((i  \mdiv{}  k)  *  2)  \mleq{}  ((i  \mdiv{}  k)  *  k)


By

---

Latex:
(Assert  2  \mleq{}  k  BY
              Auto)

---

Home Index