Step
*
2
of Lemma
rsum_int
1. n : ℤ
2. 0 < n
3. ∀y:ℕn - 1 ⟶ ℤ. (Σ{r(y[k]) | 0≤k≤n - 1 - 1} = r(Σ(y[k] | k < n - 1)))
4. y : ℕn ⟶ ℤ
⊢ Σ{r(y[k]) | 0≤k≤n - 1} = r(Σ(y[k] | k < n))
BY
{ (RWO "rsum-split-last" 0 THENA Auto) }
1
1. n : ℤ
2. 0 < n
3. ∀y:ℕn - 1 ⟶ ℤ. (Σ{r(y[k]) | 0≤k≤n - 1 - 1} = r(Σ(y[k] | k < n - 1)))
4. y : ℕn ⟶ ℤ
⊢ (Σ{r(y[k]) | 0≤k≤n - 1 - 1} + r(y[n - 1])) = r(Σ(y[k] | k < n))
Latex:
Latex:
1. n : \mBbbZ{}
2. 0 < n
3. \mforall{}y:\mBbbN{}n - 1 {}\mrightarrow{} \mBbbZ{}. (\mSigma{}\{r(y[k]) | 0\mleq{}k\mleq{}n - 1 - 1\} = r(\mSigma{}(y[k] | k < n - 1)))
4. y : \mBbbN{}n {}\mrightarrow{} \mBbbZ{}
\mvdash{} \mSigma{}\{r(y[k]) | 0\mleq{}k\mleq{}n - 1\} = r(\mSigma{}(y[k] | k < n))
By
Latex:
(RWO "rsum-split-last" 0 THENA Auto)
Home
Index