---

Step * of Lemma harmonic-series-diverges

No Annotations
Σn.(r1/r(n + 1))↑
BY
{ (With ⌜(r1/r(2))⌝ (D 0)⋅ THEN Auto) }

1
1. r0 < (r1/r(2))
2. k : ℕ
⊢ ∃m,n:ℕ. ((k ≤ m) ∧ (k ≤ n) ∧ ((r1/r(2)) ≤ |Σ{(r1/r(i + 1)) | 0≤i≤m} - Σ{(r1/r(i + 1)) | 0≤i≤n}|))

---

Latex:

---

Latex:
No  Annotations
\mSigma{}n.(r1/r(n  +  1))\muparrow{}


By

---

Latex:
(With  \mkleeneopen{}(r1/r(2))\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index