---

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


1. b : {2...}
2. k : ℕ
3. M : ℕ+
4. ∀m:ℕ+. ((1 + m) ≤ (M * b^m))
5. ¬(k = 0 ∈ ℤ)
⊢ k < M * b^k
BY
{ (InstHyp [⌜k⌝] (-2)⋅ 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.  \mneg{}(k  =  0)
\mvdash{}  k  <  M  *  b\^{}k


By

---

Latex:
(InstHyp  [\mkleeneopen{}k\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index