---

Step * of Lemma series-sum-linear2

∀x:ℕ ⟶ ℝ. ∀a,c:ℝ.  (Σn.x[n] = a ⇒ Σn.c * x[n] = c * a)
BY
{ ((Unfold `series-sum` 0 THEN Auto)
   THEN (Assert lim n→∞.c = c BY
               (BLemma `constant-limit` THEN Auto))
   THEN FLemma `rmul-limit` [-1;-2]
   THEN Auto
   THEN MoveToConcl (-1)
   THEN BLemma `converges-to_functionality`
   THEN Auto
   THEN RWO "rsum_linearity2<" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}a,c:\mBbbR{}.    (\mSigma{}n.x[n]  =  a  {}\mRightarrow{}  \mSigma{}n.c  *  x[n]  =  c  *  a)


By

---

Latex:
((Unfold  `series-sum`  0  THEN  Auto)
  THEN  (Assert  lim  n\mrightarrow{}\minfty{}.c  =  c  BY
                          (BLemma  `constant-limit`  THEN  Auto))
  THEN  FLemma  `rmul-limit`  [-1;-2]
  THEN  Auto
  THEN  MoveToConcl  (-1)
  THEN  BLemma  `converges-to\_functionality`
  THEN  Auto
  THEN  RWO  "rsum\_linearity2<"  0
  THEN  Auto)

---

Home Index