---

Step * 1 3 2 1 1 1 2 1 1 of Lemma harmonic-series-diverges


1. r0 < (r1/r(2))
2. k : ℕ
3. k ≤ (2^(k + 1) - 1)
4. k ≤ (2^k - 1)
5. (Σ{(r1/r(i + 1)) | 0≤i≤2^(k + 1) - 1} - Σ{(r1/r(i + 1)) | 0≤i≤2^k - 1}) = Σ{(r1/r(i + 1)) | 2^k≤i≤2^(k + 1) - 1}
6. ((r1/r(2^(k + 1))) * r((2^(k + 1) - 1 - 2^k) + 1)) ≤ Σ{(r1/r(i + 1)) | 2^k≤i≤2^(k + 1) - 1}
7. ¬2^(k + 1) - 1 < 2^k
⊢ (r1/r(2)) ≤ ((r1/r(2^(k + 1))) * r((2^(k + 1) - 1 - 2^k) + 1))
BY
{ Subst' ((2^(k + 1) - 1 - 2^k) + 1) = 2^k ∈ ℤ 0⋅ }

1
.....equality..... 
1. r0 < (r1/r(2))
2. k : ℕ
3. k ≤ (2^(k + 1) - 1)
4. k ≤ (2^k - 1)
5. (Σ{(r1/r(i + 1)) | 0≤i≤2^(k + 1) - 1} - Σ{(r1/r(i + 1)) | 0≤i≤2^k - 1}) = Σ{(r1/r(i + 1)) | 2^k≤i≤2^(k + 1) - 1}
6. ((r1/r(2^(k + 1))) * r((2^(k + 1) - 1 - 2^k) + 1)) ≤ Σ{(r1/r(i + 1)) | 2^k≤i≤2^(k + 1) - 1}
7. ¬2^(k + 1) - 1 < 2^k
⊢ ((2^(k + 1) - 1 - 2^k) + 1) = 2^k ∈ ℤ

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

---

Latex:

---

Latex:

1.  r0  <  (r1/r(2))
2.  k  :  \mBbbN{}
3.  k  \mleq{}  (2\^{}(k  +  1)  -  1)
4.  k  \mleq{}  (2\^{}k  -  1)
5.  (\mSigma{}\{(r1/r(i  +  1))  |  0\mleq{}i\mleq{}2\^{}(k  +  1)  -  1\}  -  \mSigma{}\{(r1/r(i  +  1))  |  0\mleq{}i\mleq{}2\^{}k  -  1\})
=  \mSigma{}\{(r1/r(i  +  1))  |  2\^{}k\mleq{}i\mleq{}2\^{}(k  +  1)  -  1\}
6.  ((r1/r(2\^{}(k  +  1)))  *  r((2\^{}(k  +  1)  -  1  -  2\^{}k)  +  1))  \mleq{}  \mSigma{}\{(r1/r(i  +  1))  |  2\^{}k\mleq{}i\mleq{}2\^{}(k  +  1)  -  1\}
7.  \mneg{}2\^{}(k  +  1)  -  1  <  2\^{}k
\mvdash{}  (r1/r(2))  \mleq{}  ((r1/r(2\^{}(k  +  1)))  *  r((2\^{}(k  +  1)  -  1  -  2\^{}k)  +  1))


By

---

Latex:
Subst'  ((2\^{}(k  +  1)  -  1  -  2\^{}k)  +  1)  =  2\^{}k  0\mcdot{}

---

Home Index