---

Step * of Lemma rsum-difference

∀[k,n,m:ℤ]. ∀[x:{k..m + 1-} ⟶ ℝ].
  ((Σ{x[i] | k≤i≤m} - Σ{x[i] | k≤i≤n}) = Σ{x[i] | n + 1≤i≤m}) supposing ((n ≤ m) and (k ≤ n))
BY
{ (Auto
   THEN ((InstLemma `rsum-split` [⌜k⌝; ⌜m⌝; ⌜x⌝; ⌜n⌝])⋅ THENA Auto)
   THEN ((SubstReal (-1) 0) THENA Auto)
   THEN nRNorm 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  ((InstLemma  `rsum-split`  [\mkleeneopen{}k\mkleeneclose{};  \mkleeneopen{}m\mkleeneclose{};  \mkleeneopen{}x\mkleeneclose{};  \mkleeneopen{}n\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  ((SubstReal  (-1)  0)  THENA  Auto)
  THEN  nRNorm  0
  THEN  Auto)

---

Home Index