---

Step * 2 1 1 1 2 1 of Lemma exp-ratio_wf2


1. b : {2...}
2. k : ℕ
3. M : ℕ+
4. ∀m:ℕ+. ((1 + m) ≤ (M * b^m))
5. k = 0 ∈ ℤ
⊢ ∃c:ℕ. 0 < M * b^c
BY
{ (With ⌜0⌝ (D 0)⋅ THEN Reduce 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  b  :  \{2...\}
2.  k  :  \mBbbN{}
3.  M  :  \mBbbN{}\msupplus{}
4.  \mforall{}m:\mBbbN{}\msupplus{}.  ((1  +  m)  \mleq{}  (M  *  b\^{}m))
5.  k  =  0
\mvdash{}  \mexists{}c:\mBbbN{}.  0  <  M  *  b\^{}c


By

---

Latex:
(With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  Reduce  0  THEN  Auto)\mcdot{}

---

Home Index