---

Step * of Lemma rsum-telescopes2

∀[n:ℤ]. ∀[m:{n...}]. ∀[x,y:{n..m + 1-} ⟶ ℝ].
  Σ{x[k] - y[k] | n≤k≤m} = (x[n] - y[m]) supposing ∀i:{n..m-}. (x[i + 1] = y[i])
BY
{ (Auto
   THEN (InstLemma `rsum-telescopes` [⌜n⌝;⌜m⌝;⌜λ2k.-(y[k])⌝;⌜λ2k.-(x[k])⌝]⋅ THENA (Auto THEN RWO "-2" 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]))
⊢ Σ{x[k] - y[k] | n≤k≤m} = (x[n] - y[m])

---

Latex:

---

Latex:
\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[n]  -  y[m])  supposing  \mforall{}i:\{n..m\msupminus{}\}.  (x[i  +  1]  =  y[i])


By

---

Latex:
(Auto
  THEN  (InstLemma  `rsum-telescopes`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}k.-(y[k])\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}k.-(x[k])\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  RWO  "-2"  0  THEN  Auto)
              )
  )

---

Home Index