---

Step * of Lemma rsum-split

∀[n,m:ℤ]. ∀[x:{n..m + 1-} ⟶ ℝ]. ∀[k:ℤ].
  (Σ{x[i] | n≤i≤m} = (Σ{x[i] | n≤i≤k} + Σ{x[i] | k + 1≤i≤m})) supposing ((k ≤ m) and (n ≤ k))
BY
{ (Auto
   THEN Unfold `rsum` 0
   THEN RepeatFor 3 ((CallByValueReduce 0 THENA Auto))
   THEN ((RWO "radd-list-append<" 0 THENA Auto)
         THEN (RWO "map_append_sq<" 0 THENA Auto)
         THEN RWO "from-upto-split<" 0
         THEN Auto)⋅) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  Unfold  `rsum`  0
  THEN  RepeatFor  3  ((CallByValueReduce  0  THENA  Auto))
  THEN  ((RWO  "radd-list-append<"  0  THENA  Auto)
              THEN  (RWO  "map\_append\_sq<"  0  THENA  Auto)
              THEN  RWO  "from-upto-split<"  0
              THEN  Auto)\mcdot{})

---

Home Index