---

Step * of Lemma rsum-telescopes

No Annotations
∀[n:ℤ]. ∀[m:{n...}]. ∀[x,y:{n..m + 1-} ⟶ ℝ].
  Σ{x[k] - y[k] | n≤k≤m} = (x[m] - y[n]) supposing ∀i:{n..m-}. (y[i + 1] = x[i])
BY
{ Auto }

1
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])

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbZ{}].  \mforall{}[m:\{n...\}].  \mforall{}[x,y:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}].
    \mSigma{}\{x[k]  -  y[k]  |  n\mleq{}k\mleq{}m\}  =  (x[m]  -  y[n])  supposing  \mforall{}i:\{n..m\msupminus{}\}.  (y[i  +  1]  =  x[i])


By

---

Latex:
Auto

---

Home Index