---

Step * 2 1 1 1 of Lemma exp-ratio_wf2


1. b : {2...}
2. k : ℕ
3. M : ℕ+
⊢ ∃c:ℕ. k < M * b^c
BY
{ Assert ⌜∀m:ℕ+. ((1 + m) ≤ (M * b^m))⌝⋅ }

1
.....assertion..... 
1. b : {2...}
2. k : ℕ
3. M : ℕ+
⊢ ∀m:ℕ+. ((1 + m) ≤ (M * b^m))

2
1. b : {2...}
2. k : ℕ
3. M : ℕ+
4. ∀m:ℕ+. ((1 + m) ≤ (M * b^m))
⊢ ∃c:ℕ. k < M * b^c

---

Latex:

---

Latex:

1.  b  :  \{2...\}
2.  k  :  \mBbbN{}
3.  M  :  \mBbbN{}\msupplus{}
\mvdash{}  \mexists{}c:\mBbbN{}.  k  <  M  *  b\^{}c


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}m:\mBbbN{}\msupplus{}.  ((1  +  m)  \mleq{}  (M  *  b\^{}m))\mkleeneclose{}\mcdot{}

---

Home Index