---

Step * 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 ∈ upto(k)) = Σ(f[x] | x < k) ∈ ℤ
BY
{ ((RWO  "upto_decomp1" 0 THENA Auto)
   THEN (RWO "lsum-append" 0 THENA (Auto THEN GenListD (-1) THEN Auto THEN D -1 THEN GenListD (-1) THEN Auto))
   THEN (RWO "-2" 0 THENA (Auto THEN GenListD (-1) THEN Auto))) }

1
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) ∈ ℤ

---

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  \mmember{}  upto(k))  =  \mSigma{}(f[x]  |  x  <  k)


By

---

Latex:
((RWO    "upto\_decomp1"  0  THENA  Auto)
  THEN  (RWO  "lsum-append"  0
              THENA  (Auto  THEN  GenListD  (-1)  THEN  Auto  THEN  D  -1  THEN  GenListD  (-1)  THEN  Auto)
              )
  THEN  (RWO  "-2"  0  THENA  (Auto  THEN  GenListD  (-1)  THEN  Auto)))

---

Home Index