---

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


1. u : ℝ
2. v : ℝ List
3. 1 < ||v|| + 1
4. frs-non-dec([u / v])
5. 1 < ||v||
6. frs-non-dec(v) ⇒ (Σ{v[i + 1] - v[i] | 0≤i≤||v|| - 2} = (last(v) - v[0]))
⊢ Σ{[u / v][i + 1] - [u / v][i] | 0≤i≤(||v|| + 1) - 2} = (last([u / v]) - u)
BY
{ ((RWO "rsum-split-first" 0 THENA Auto) THEN Reduce 0) }

1
1. u : ℝ
2. v : ℝ List
3. 1 < ||v|| + 1
4. frs-non-dec([u / v])
5. 1 < ||v||
6. frs-non-dec(v) ⇒ (Σ{v[i + 1] - v[i] | 0≤i≤||v|| - 2} = (last(v) - v[0]))
⊢ ((v[0] - u) + Σ{[u / v][i + 1] - [u / v][i] | 1≤i≤(||v|| + 1) - 2}) = (last([u / v]) - u)

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "rsum-split-first"  0  THENA  Auto)  THEN  Reduce  0)

---

Home Index