---

Step * of Lemma comparison-test-for-divergence

∀x,y:ℕ ⟶ ℝ.  (Σn.y[n]↑ ⇒ (∃N:ℕ. ∀n:{N...}. ((r0 ≤ y[n]) ∧ (y[n] ≤ x[n]))) ⇒ Σn.x[n]↑)
BY
{ (Auto THEN RepeatFor 4 (ParallelOp -2) THEN (D 0 THENA Auto) THEN ExRepD) }

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

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.    (\mSigma{}n.y[n]\muparrow{}  {}\mRightarrow{}  (\mexists{}N:\mBbbN{}.  \mforall{}n:\{N...\}.  ((r0  \mleq{}  y[n])  \mwedge{}  (y[n]  \mleq{}  x[n])))  {}\mRightarrow{}  \mSigma{}n.x[n]\muparrow{})


By

---

Latex:
(Auto  THEN  RepeatFor  4  (ParallelOp  -2)  THEN  (D  0  THENA  Auto)  THEN  ExRepD)

---

Home Index