---

Step * of Lemma rsum-split-shift

∀[k,n,m:ℤ]. ∀[x:{n..m + 1-} ⟶ ℝ].
  (Σ{x[i] | n≤i≤m} = (Σ{x[i] | n≤i≤k} + Σ{x[k + i + 1] | 0≤i≤m - k + 1})) supposing ((k ≤ m) and (n ≤ k))
BY
{ (Intros
   THEN (InstLemma `rsum-split` [⌜n⌝;⌜m⌝;⌜x⌝;⌜k⌝]⋅ THENA Auto)
   THEN (InstLemma `rsum-shift` [⌜k + 1⌝;⌜k + 1⌝;⌜m⌝;⌜x⌝]⋅ THENA Auto)
   THEN HypSubst' (-1) (-2)
   THEN NthHypSq (-2)
   THEN RepeatFor 3 (EqCD)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[k,n,m:\mBbbZ{}].  \mforall{}[x:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}].
    (\mSigma{}\{x[i]  |  n\mleq{}i\mleq{}m\}  =  (\mSigma{}\{x[i]  |  n\mleq{}i\mleq{}k\}  +  \mSigma{}\{x[k  +  i  +  1]  |  0\mleq{}i\mleq{}m  -  k  +  1\}))  supposing 
          ((k  \mleq{}  m)  and 
          (n  \mleq{}  k))


By

---

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

---

Home Index