---

Step * 1 2 of Lemma harmonic-series-diverges


1. r0 < (r1/r(2))
2. k : ℕ
3. k ≤ (2^(k + 1) - 1)
⊢ k ≤ (2^k - 1)
BY
{ (InstLemma `exp-greater` [⌜2⌝;⌜k⌝]⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:

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


By

---

Latex:
(InstLemma  `exp-greater`  [\mkleeneopen{}2\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index