---

Step * 1 of Lemma rsum-telescopes


1. n : ℤ
2. m : {n...}
3. x : {n..m + 1-} ⟶ ℝ
4. y : {n..m + 1-} ⟶ ℝ
5. ∀i:{n..m-}. (y[i + 1] = x[i])
⊢ Σ{x[k] - y[k] | n≤k≤m} = (x[m] - y[n])
BY
{ Assert ⌜∀d:ℕ. ((d ≤ (m - n)) ⇒ (Σ{x[k] - y[k] | n≤k≤n + d} = (x[n + d] - y[n])))⌝⋅ }

1
.....assertion..... 
1. n : ℤ
2. m : {n...}
3. x : {n..m + 1-} ⟶ ℝ
4. y : {n..m + 1-} ⟶ ℝ
5. ∀i:{n..m-}. (y[i + 1] = x[i])
⊢ ∀d:ℕ. ((d ≤ (m - n)) ⇒ (Σ{x[k] - y[k] | n≤k≤n + d} = (x[n + d] - y[n])))

2
1. n : ℤ
2. m : {n...}
3. x : {n..m + 1-} ⟶ ℝ
4. y : {n..m + 1-} ⟶ ℝ
5. ∀i:{n..m-}. (y[i + 1] = x[i])
6. ∀d:ℕ. ((d ≤ (m - n)) ⇒ (Σ{x[k] - y[k] | n≤k≤n + d} = (x[n + d] - y[n])))
⊢ Σ{x[k] - y[k] | n≤k≤m} = (x[m] - y[n])

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  m  :  \{n...\}
3.  x  :  \{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
4.  y  :  \{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
5.  \mforall{}i:\{n..m\msupminus{}\}.  (y[i  +  1]  =  x[i])
\mvdash{}  \mSigma{}\{x[k]  -  y[k]  |  n\mleq{}k\mleq{}m\}  =  (x[m]  -  y[n])


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}.  ((d  \mleq{}  (m  -  n))  {}\mRightarrow{}  (\mSigma{}\{x[k]  -  y[k]  |  n\mleq{}k\mleq{}n  +  d\}  =  (x[n  +  d]  -  y[n])))\mkleeneclose{}\mcdot{}

---

Home Index