---

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

.....antecedent..... 
1. r0 < (r1/r(2))
2. k : ℕ
3. k ≤ (2^(k + 1) - 1)
4. k ≤ (2^k - 1)
⊢ (2^k - 1) ≤ (2^(k + 1) - 1)
BY
{ (RWW "exp_add exp1" 0 THEN Auto)⋅ }

---

Latex:

---

Latex:
.....antecedent..... 
1.  r0  <  (r1/r(2))
2.  k  :  \mBbbN{}
3.  k  \mleq{}  (2\^{}(k  +  1)  -  1)
4.  k  \mleq{}  (2\^{}k  -  1)
\mvdash{}  (2\^{}k  -  1)  \mleq{}  (2\^{}(k  +  1)  -  1)


By

---

Latex:
(RWW  "exp\_add  exp1"  0  THEN  Auto)\mcdot{}

---

Home Index