---

Step * of Lemma series-diverges-tail-iff

∀x:ℕ ⟶ ℝ. ∀N:ℕ.  (Σn.x[N + n]↑ ⇐⇒ Σn.x[n]↑)
BY
{ (InstLemma `series-diverges-tail` []
   THEN RepeatFor 2 (ParallelLast')
   THEN Auto
   THEN RepeatFor 4 (ParallelLast')
   THEN Auto) }

1
1. x : ℕ ⟶ ℝ
2. N : ℕ
3. Σn.x[N + n]↑ ⇒ Σn.x[n]↑
4. e : ℝ
5. r0 < e
6. ∀k:ℕ. ∃m,n:ℕ. ((k ≤ m) ∧ (k ≤ n) ∧ (e ≤ |Σ{x[i] | 0≤i≤m} - Σ{x[i] | 0≤i≤n}|))
7. k : ℕ
⊢ ∃m,n:ℕ. ((k ≤ m) ∧ (k ≤ n) ∧ (e ≤ |Σ{x[N + i] | 0≤i≤m} - Σ{x[N + i] | 0≤i≤n}|))

---

Latex:

---

Latex:
\mforall{}x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}N:\mBbbN{}.    (\mSigma{}n.x[N  +  n]\muparrow{}  \mLeftarrow{}{}\mRightarrow{}  \mSigma{}n.x[n]\muparrow{})


By

---

Latex:
(InstLemma  `series-diverges-tail`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  Auto
  THEN  RepeatFor  4  (ParallelLast')
  THEN  Auto)

---

Home Index