---

Step * 1 1 of Lemma rsum-telescopes

.....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])))
BY
{ (InductionOnNat THEN Auto THEN RWO "rsum_unroll" 0 THEN Auto THEN AutoSplit) }

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])
6. d : ℤ
7. ¬n + d < n
8. 0 < d
9. ((d - 1) ≤ (m - n)) ⇒ (Σ{x[k] - y[k] | n≤k≤n + (d - 1)} = (x[n + (d - 1)] - y[n]))
10. d ≤ (m - n)
⊢ (Σ{x[k] - y[k] | n≤k≤(n + d) - 1} + (x[n + d] - y[n + d])) = (x[n + d] - y[n])

---

Latex:

---

Latex:
.....assertion..... 
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{}  \mforall{}d:\mBbbN{}.  ((d  \mleq{}  (m  -  n))  {}\mRightarrow{}  (\mSigma{}\{x[k]  -  y[k]  |  n\mleq{}k\mleq{}n  +  d\}  =  (x[n  +  d]  -  y[n])))


By

---

Latex:
(InductionOnNat  THEN  Auto  THEN  RWO  "rsum\_unroll"  0  THEN  Auto  THEN  AutoSplit)

---

Home Index