---

Step * of Lemma rsum-rminus

∀[n,m:ℤ]. ∀[x:{n..m + 1-} ⟶ ℝ].  (Σ{-(x[k]) | n≤k≤m} = -(Σ{x[k] | n≤k≤m}))
BY
{ (InstLemma `rsum_linearity2` [] THEN RepeatFor 3 (ParallelLast') THEN (D -1 With ⌜r(-1)⌝  THENA Auto)) }

1
1. [n] : ℤ
2. [m] : ℤ
3. [x] : {n..m + 1-} ⟶ ℝ
4. Σ{r(-1) * x[k] | n≤k≤m} = (r(-1) * Σ{x[k] | n≤k≤m})
⊢ Σ{-(x[k]) | n≤k≤m} = -(Σ{x[k] | n≤k≤m})

---

Latex:

---

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


By

---

Latex:
(InstLemma  `rsum\_linearity2`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  (D  -1  With  \mkleeneopen{}r(-1)\mkleeneclose{}    THENA  Auto))

---

Home Index