---

Step * 2 2 of Lemma frs-non-dec-sum


1. u : ℝ
2. u1 : ℝ
3. v : ℝ List
4. 1 < (||v|| + 1) + 1
5. frs-non-dec([u; [u1 / v]])
6. ¬1 < ||v|| + 1
⊢ Σ{[u; [u1 / v]][i + 1] - [u; [u1 / v]][i] | 0≤i≤((||v|| + 1) + 1) - 2} = (last([u; [u1 / v]]) - u)
BY
{ (DVar `v' THEN All Reduce THEN Auto') }

1
1. u : ℝ
2. u1 : ℝ
3. 1 < 2
4. frs-non-dec([u; u1])
5. ¬1 < 1
⊢ Σ{[u; u1][i + 1] - [u; u1][i] | 0≤i≤0} = (last([u; u1]) - u)

---

Latex:

---

Latex:

1.  u  :  \mBbbR{}
2.  u1  :  \mBbbR{}
3.  v  :  \mBbbR{}  List
4.  1  <  (||v||  +  1)  +  1
5.  frs-non-dec([u;  [u1  /  v]])
6.  \mneg{}1  <  ||v||  +  1
\mvdash{}  \mSigma{}\{[u;  [u1  /  v]][i  +  1]  -  [u;  [u1  /  v]][i]  |  0\mleq{}i\mleq{}((||v||  +  1)  +  1)  -  2\}  =  (last([u;  [u1  /  v]])  -  u)


By

---

Latex:
(DVar  `v'  THEN  All  Reduce  THEN  Auto')

---

Home Index