---

Step * 1 1 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])
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])
BY
{ ((Subst' (n + d) - 1 ~ n + (d - 1) 0 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-}. (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[n + (d - 1)] - y[n]) + (x[n + d] - y[n + d])) = (x[n + d] - 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])
6.  d  :  \mBbbZ{}
7.  \mneg{}n  +  d  <  n
8.  0  <  d
9.  ((d  -  1)  \mleq{}  (m  -  n))  {}\mRightarrow{}  (\mSigma{}\{x[k]  -  y[k]  |  n\mleq{}k\mleq{}n  +  (d  -  1)\}  =  (x[n  +  (d  -  1)]  -  y[n]))
10.  d  \mleq{}  (m  -  n)
\mvdash{}  (\mSigma{}\{x[k]  -  y[k]  |  n\mleq{}k\mleq{}(n  +  d)  -  1\}  +  (x[n  +  d]  -  y[n  +  d]))  =  (x[n  +  d]  -  y[n])


By

---

Latex:
((Subst'  (n  +  d)  -  1  \msim{}  n  +  (d  -  1)  0  THENA  Auto)  THEN  RWO  "-2"  0  THEN  Auto)

---

Home Index