---

Step * 1 1 2 1 1 1 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. Σ{v[i + 1] - v[i] | 0≤i≤||v|| - 2} = (last(v) - v[0])
7. ∀[n,m:ℤ]. ∀[x:Top].  (Σ{x[i] | n≤i≤m} ~ Σ{x[i + 1] | n - 1≤i≤m - 1})
⊢ Σ{[u / v][(i + 1) + 1] - [u / v][i + 1] | 0≤i≤||v|| - 2} = Σ{v[i + 1] - v[i] | 0≤i≤||v|| - 2}
BY
{ (BLemma `rsum_functionality` THEN Auto) }

1
1. u : ℝ
2. v : ℝ List
3. 1 < ||v|| + 1
4. frs-non-dec([u / v])
5. 1 < ||v||
6. Σ{v[i + 1] - v[i] | 0≤i≤||v|| - 2} = (last(v) - v[0])
7. ∀[n,m:ℤ]. ∀[x:Top].  (Σ{x[i] | n≤i≤m} ~ Σ{x[i + 1] | n - 1≤i≤m - 1})
⊢ [u / v][(i + 1) + 1] - [u / v][i + 1] = v[i + 1] - v[i] for i ∈ [0,||v|| - 2]

---

Latex:

---

Latex:

1.  u  :  \mBbbR{}
2.  v  :  \mBbbR{}  List
3.  1  <  ||v||  +  1
4.  frs-non-dec([u  /  v])
5.  1  <  ||v||
6.  \mSigma{}\{v[i  +  1]  -  v[i]  |  0\mleq{}i\mleq{}||v||  -  2\}  =  (last(v)  -  v[0])
7.  \mforall{}[n,m:\mBbbZ{}].  \mforall{}[x:Top].    (\mSigma{}\{x[i]  |  n\mleq{}i\mleq{}m\}  \msim{}  \mSigma{}\{x[i  +  1]  |  n  -  1\mleq{}i\mleq{}m  -  1\})
\mvdash{}  \mSigma{}\{[u  /  v][(i  +  1)  +  1]  -  [u  /  v][i  +  1]  |  0\mleq{}i\mleq{}||v||  -  2\}  =  \mSigma{}\{v[i  +  1]  -  v[i]  |  0\mleq{}i\mleq{}||v||  -  2\}


By

---

Latex:
(BLemma  `rsum\_functionality`  THEN  Auto)

---

Home Index