---

Step * 1 of Lemma rsum-telescopes2


1. n : ℤ
2. m : {n...}
3. x : {n..m + 1-} ⟶ ℝ
4. y : {n..m + 1-} ⟶ ℝ
5. ∀i:{n..m-}. (x[i + 1] = y[i])
6. Σ{-(y[k]) - -(x[k]) | n≤k≤m} = (-(y[m]) - -(x[n]))
⊢ Σ{x[k] - y[k] | n≤k≤m} = (x[n] - y[m])
BY
{ (Assert Σ{-(y[k]) - -(x[k]) | n≤k≤m} = Σ{x[k] - y[k] | n≤k≤m} BY
         ((BLemma `rsum_functionality` THENM D 0 THENM nRNorm 0) THEN Auto)) }

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

---

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{}\}.  (x[i  +  1]  =  y[i])
6.  \mSigma{}\{-(y[k])  -  -(x[k])  |  n\mleq{}k\mleq{}m\}  =  (-(y[m])  -  -(x[n]))
\mvdash{}  \mSigma{}\{x[k]  -  y[k]  |  n\mleq{}k\mleq{}m\}  =  (x[n]  -  y[m])


By

---

Latex:
(Assert  \mSigma{}\{-(y[k])  -  -(x[k])  |  n\mleq{}k\mleq{}m\}  =  \mSigma{}\{x[k]  -  y[k]  |  n\mleq{}k\mleq{}m\}  BY
              ((BLemma  `rsum\_functionality`  THENM  D  0  THENM  nRNorm  0)  THEN  Auto))

---

Home Index