---

Step * of Lemma sum-in-vs-split-shift

∀[k,n,m:ℤ]. ∀[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[f:{n..m + 1-} ⟶ Point(vs)].
  Σ{f[i] | n≤i≤m} = Σ{f[i] | n≤i≤k} + Σ{f[k + i + 1] | 0≤i≤m - k + 1} ∈ Point(vs) supposing (n ≤ k) ∧ (k ≤ m)
BY
{ (Intros
   THEN (InstLemma `sum-in-vs-split` [⌜n⌝;⌜m⌝;⌜k⌝;⌜K⌝;⌜vs⌝;⌜f⌝]⋅ THENA Auto)
   THEN (InstLemma `sum-in-vs-shift` [⌜k + 1⌝;⌜k + 1⌝;⌜m⌝;⌜f⌝;⌜vs⌝]⋅ THENA Auto)
   THEN HypSubst' (-1) (-2)
   THEN NthHypSq (-2)
   THEN RepeatFor 3 (EqCD)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[k,n,m:\mBbbZ{}].  \mforall{}[K:Rng].  \mforall{}[vs:VectorSpace(K)].  \mforall{}[f:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  Point(vs)].
    \mSigma{}\{f[i]  |  n\mleq{}i\mleq{}m\}  =  \mSigma{}\{f[i]  |  n\mleq{}i\mleq{}k\}  +  \mSigma{}\{f[k  +  i  +  1]  |  0\mleq{}i\mleq{}m  -  k  +  1\}  supposing  (n  \mleq{}  k)  \mwedge{}  (k  \mleq{}  m)


By

---

Latex:
(Intros
  THEN  (InstLemma  `sum-in-vs-split`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}vs\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `sum-in-vs-shift`  [\mkleeneopen{}k  +  1\mkleeneclose{};\mkleeneopen{}k  +  1\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}vs\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  HypSubst'  (-1)  (-2)
  THEN  NthHypSq  (-2)
  THEN  RepeatFor  3  (EqCD)
  THEN  Auto)

---

Home Index