---

Step * 1 of Lemma harmonic-series-diverges


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}|))
BY
{ (InstConcl [⌜2^(k + 1) - 1⌝;⌜2^k - 1⌝]⋅ THEN Auto) }

1
1. r0 < (r1/r(2))
2. k : ℕ
⊢ k ≤ (2^(k + 1) - 1)

2
1. r0 < (r1/r(2))
2. k : ℕ
3. k ≤ (2^(k + 1) - 1)
⊢ k ≤ (2^k - 1)

3
1. r0 < (r1/r(2))
2. k : ℕ
3. k ≤ (2^(k + 1) - 1)
4. k ≤ (2^k - 1)
⊢ (r1/r(2)) ≤ |Σ{(r1/r(i + 1)) | 0≤i≤2^(k + 1) - 1} - Σ{(r1/r(i + 1)) | 0≤i≤2^k - 1}|

---

Latex:

---

Latex:

1.  r0  <  (r1/r(2))
2.  k  :  \mBbbN{}
\mvdash{}  \mexists{}m,n:\mBbbN{}.  ((k  \mleq{}  m)  \mwedge{}  (k  \mleq{}  n)  \mwedge{}  ((r1/r(2))  \mleq{}  |\mSigma{}\{(r1/r(i  +  1))  |  0\mleq{}i\mleq{}m\}  -  \mSigma{}\{(r1/r(i  +  1))  |  0\mleq{}i\mleq{}n\}|))


By

---

Latex:
(InstConcl  [\mkleeneopen{}2\^{}(k  +  1)  -  1\mkleeneclose{};\mkleeneopen{}2\^{}k  -  1\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index