---

Step * 1 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[n + (d - 1)] - y[n]) + (x[n + d] - y[n + d])) = (x[n + d] - y[n])
BY
{ ((InstHyp [⌜n + (d - 1)⌝] 5⋅ THENA Auto) THEN (RWO "-1<" 0 THENA 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)
11. y[(n + (d - 1)) + 1] = x[n + (d - 1)]
⊢ ((y[(n + (d - 1)) + 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{}  ((x[n  +  (d  -  1)]  -  y[n])  +  (x[n  +  d]  -  y[n  +  d]))  =  (x[n  +  d]  -  y[n])


By

---

Latex:
((InstHyp  [\mkleeneopen{}n  +  (d  -  1)\mkleeneclose{}]  5\mcdot{}  THENA  Auto)  THEN  (RWO  "-1<"  0  THENA  Auto))

---

Home Index