---

Step * 1 1 of Lemma uniform-partition-increasing


1. a : ℝ
2. b : ℝ
3. a < b
4. k : ℕ+
5. icompact([a, b])
6. i : ℕk - 1
7. j : ℕk - 1
8. i < j
⊢ (((r(k) - r(i + 1)) * a) + (r(i + 1) * b)/r(k)) < (((r(k) - r(j + 1)) * a) + (r(j + 1) * b)/r(k))
BY
{ (nRMul ⌜r(k)⌝ 0⋅ THEN (Assert r(i + 1) < r(j + 1) BY Auto) THEN nRMul ⌜b - a⌝ (-1)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  a  <  b
4.  k  :  \mBbbN{}\msupplus{}
5.  icompact([a,  b])
6.  i  :  \mBbbN{}k  -  1
7.  j  :  \mBbbN{}k  -  1
8.  i  <  j
\mvdash{}  (((r(k)  -  r(i  +  1))  *  a)  +  (r(i  +  1)  *  b)/r(k))  <  (((r(k)  -  r(j  +  1))  *  a)  +  (r(j  +  1)  *  b)/r(k))


By

---

Latex:
(nRMul  \mkleeneopen{}r(k)\mkleeneclose{}  0\mcdot{}  THEN  (Assert  r(i  +  1)  <  r(j  +  1)  BY  Auto)  THEN  nRMul  \mkleeneopen{}b  -  a\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto)

---

Home Index