---

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


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

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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index