---

Step * 2 1 2 of Lemma div_mono1


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 < i
BY
{ Assert ⌜((i ÷ k) * 2) ≤ ((i ÷ k) * k)⌝⋅ }

1
.....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)

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

---

Latex:

---

Latex:

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  <  i


By

---

Latex:
Assert  \mkleeneopen{}((i  \mdiv{}  k)  *  2)  \mleq{}  ((i  \mdiv{}  k)  *  k)\mkleeneclose{}\mcdot{}

---

Home Index