---

Step * of Lemma series-sum-linear3

∀x:ℕ ⟶ ℝ. ∀a,c:ℝ.  (Σn.x[n] = a ⇒ Σn.x[n] * c = a * c)
BY
{ ((Unfold `series-sum` 0 THEN Auto)
   THEN ParallelLast
   THEN Auto
   THEN (InstLemma `integer-bound` [⌜c⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN (Evaluate ⌜m = n ∈ ℕ+⌝⋅ THENA Auto)
   THEN Eliminate ⌜n⌝⋅
   THEN ThinVar `n'
   THEN RenameVar `n' 1) }

1
1. n : ℕ+
2. x : ℕ ⟶ ℝ
3. a : ℝ
4. c : ℝ
5. ∀k:ℕ+. (∃N:{ℕ| (∀n:ℕ. ((N ≤ n) ⇒ (|Σ{x[i] | 0≤i≤n} - a| ≤ (r1/r(k)))))})
6. k : ℕ+
7. |c| ≤ r(n)
⊢ ∃N:{ℕ| (∀n:ℕ. ((N ≤ n) ⇒ (|Σ{x[i] * c | 0≤i≤n} - a * c| ≤ (r1/r(k)))))}

---

Latex:

---

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


By

---

Latex:
((Unfold  `series-sum`  0  THEN  Auto)
  THEN  ParallelLast
  THEN  Auto
  THEN  (InstLemma  `integer-bound`  [\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (Evaluate  \mkleeneopen{}m  =  n\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Eliminate  \mkleeneopen{}n\mkleeneclose{}\mcdot{}
  THEN  ThinVar  `n'
  THEN  RenameVar  `n'  1)

---

Home Index