---

Step * of Lemma alternating-series-converges

∀x:ℕ ⟶ ℝ. ((∃M:ℕ. ∀n:ℕ. (M < n ⇒ ((r0 ≤ x[n]) ∧ (x[n + 1] ≤ x[n])))) ⇒ lim n→∞.x[n] = r0 ⇒ Σn.-1^n * x[n]↓)
BY
{ (Auto THEN D 2 THEN (InstLemma `alternating-series-tail-bound` [⌜x⌝;⌜M + 1⌝]⋅ THENA Auto)) }

1
1. x : ℕ ⟶ ℝ
2. M : ℕ
3. ∀n:ℕ. (M < n ⇒ ((r0 ≤ x[n]) ∧ (x[n + 1] ≤ x[n])))
4. lim n→∞.x[n] = r0
5. ∀a:{M + 1...}. ∀b:ℕ.  (|Σ{-1^i * x[i] | a≤i≤b}| ≤ x[a])
⊢ Σn.-1^n * x[n]↓

---

Latex:

---

Latex:
\mforall{}x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}
    ((\mexists{}M:\mBbbN{}.  \mforall{}n:\mBbbN{}.  (M  <  n  {}\mRightarrow{}  ((r0  \mleq{}  x[n])  \mwedge{}  (x[n  +  1]  \mleq{}  x[n]))))
    {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.x[n]  =  r0
    {}\mRightarrow{}  \mSigma{}n.-1\^{}n  *  x[n]\mdownarrow{})


By

---

Latex:
(Auto  THEN  D  2  THEN  (InstLemma  `alternating-series-tail-bound`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}M  +  1\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index