---

Step * 1 1 of Lemma rsum-difference2

.....assertion..... 
1. k : ℤ
2. n : ℤ
3. m : ℤ
4. x : {k..m + 1-} ⟶ ℝ
5. y : {k..m + 1-} ⟶ ℝ
6. k ≤ n
7. n ≤ m
8. ∀i:{k..n + 1-}. (x[i] = y[i])
9. Σ{x[i] | k≤i≤m} = (Σ{x[i] | k≤i≤n} + Σ{x[i] | n + 1≤i≤m})
⊢ Σ{y[i] | k≤i≤n} = Σ{x[i] | k≤i≤n}
BY
{ (RWO "-2" 0 THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  k  :  \mBbbZ{}
2.  n  :  \mBbbZ{}
3.  m  :  \mBbbZ{}
4.  x  :  \{k..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
5.  y  :  \{k..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
6.  k  \mleq{}  n
7.  n  \mleq{}  m
8.  \mforall{}i:\{k..n  +  1\msupminus{}\}.  (x[i]  =  y[i])
9.  \mSigma{}\{x[i]  |  k\mleq{}i\mleq{}m\}  =  (\mSigma{}\{x[i]  |  k\mleq{}i\mleq{}n\}  +  \mSigma{}\{x[i]  |  n  +  1\mleq{}i\mleq{}m\})
\mvdash{}  \mSigma{}\{y[i]  |  k\mleq{}i\mleq{}n\}  =  \mSigma{}\{x[i]  |  k\mleq{}i\mleq{}n\}


By

---

Latex:
(RWO  "-2"  0  THEN  Auto)

---

Home Index