---

Step * 1 of Lemma rsum-difference2


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})
⊢ (Σ{x[i] | n + 1≤i≤m} + Σ{x[i] | k≤i≤n} + -(Σ{y[i] | k≤i≤n})) = Σ{x[i] | n + 1≤i≤m}
BY
{ Assert ⌜Σ{y[i] | k≤i≤n} = Σ{x[i] | k≤i≤n}⌝⋅ }

1
.....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}

2
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})
10. Σ{y[i] | k≤i≤n} = Σ{x[i] | k≤i≤n}
⊢ (Σ{x[i] | n + 1≤i≤m} + Σ{x[i] | k≤i≤n} + -(Σ{y[i] | k≤i≤n})) = Σ{x[i] | n + 1≤i≤m}

---

Latex:

---

Latex:

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{}\{x[i]  |  n  +  1\mleq{}i\mleq{}m\}  +  \mSigma{}\{x[i]  |  k\mleq{}i\mleq{}n\}  +  -(\mSigma{}\{y[i]  |  k\mleq{}i\mleq{}n\}))  =  \mSigma{}\{x[i]  |  n  +  1\mleq{}i\mleq{}m\}


By

---

Latex:
Assert  \mkleeneopen{}\mSigma{}\{y[i]  |  k\mleq{}i\mleq{}n\}  =  \mSigma{}\{x[i]  |  k\mleq{}i\mleq{}n\}\mkleeneclose{}\mcdot{}

---

Home Index