---

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


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

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

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

---

Latex:

---

Latex:

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


By

---

Latex:
CaseNat  0  `k'

---

Home Index