---

Step * of Lemma rsum-difference2

∀[k,n,m:ℤ]. ∀[x,y:{k..m + 1-} ⟶ ℝ].
  ((Σ{x[i] | k≤i≤m} - Σ{y[i] | k≤i≤n}) = Σ{x[i] | n + 1≤i≤m}) supposing 
     ((∀i:{k..n + 1-}. (x[i] = y[i])) and 
     (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) }

1
1. k : ℤ
2. n : ℤ
3. m : ℤ
4. x : {k..m + 1-} ⟶ ℝ
5. y : {k..m + 1-} ⟶ ℝ
6. k ≤ n
7. n ≤ m
8. ∀i:{k..n + 1-}. (x[i] = y[i])
9. Σ{x[i] | k≤i≤m} = (Σ{x[i] | k≤i≤n} + Σ{x[i] | n + 1≤i≤m})
⊢ (Σ{x[i] | n + 1≤i≤m} + Σ{x[i] | k≤i≤n} + -(Σ{y[i] | k≤i≤n})) = Σ{x[i] | n + 1≤i≤m}

---

Latex:

---

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