---

Step * 1 1 of Lemma lsum-upto


1. k : ℤ
2. 0 < k
3. ∀[f:ℕk - 1 ⟶ ℤ]. (Σ(f[x] | x ∈ upto(k - 1)) = Σ(f[x] | x < k - 1) ∈ ℤ)
4. f : ℕk ⟶ ℤ
⊢ (Σ(f[x] | x < k - 1) + Σ(f[x] | x ∈ [k - 1])) = Σ(f[x] | x < k) ∈ ℤ
BY
{ (RW (AddrC [3] (LemmaC `sum-unroll`)) 0 THEN Auto) }

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
2.  0  <  k
3.  \mforall{}[f:\mBbbN{}k  -  1  {}\mrightarrow{}  \mBbbZ{}].  (\mSigma{}(f[x]  |  x  \mmember{}  upto(k  -  1))  =  \mSigma{}(f[x]  |  x  <  k  -  1))
4.  f  :  \mBbbN{}k  {}\mrightarrow{}  \mBbbZ{}
\mvdash{}  (\mSigma{}(f[x]  |  x  <  k  -  1)  +  \mSigma{}(f[x]  |  x  \mmember{}  [k  -  1]))  =  \mSigma{}(f[x]  |  x  <  k)


By

---

Latex:
(RW  (AddrC  [3]  (LemmaC  `sum-unroll`))  0  THEN  Auto)

---

Home Index