---

Step * of Lemma rexp-approx-lemma-ext

∀N:ℕ+. (∃k:ℕ [(N ≤ (4^k * 3 * (k)!))])
BY
{ Extract of Obid: rexp-approx-lemma
  not unfolding  genfact-inv
  finishing with Auto
  normalizes to:
  
  λN.genfact-inv(N;3;m.4 * m) }

---

Latex:

---

Latex:
\mforall{}N:\mBbbN{}\msupplus{}.  (\mexists{}k:\mBbbN{}  [(N  \mleq{}  (4\^{}k  *  3  *  (k)!))])


By

---

Latex:
Extract  of  Obid:  rexp-approx-lemma
not  unfolding    genfact-inv
finishing  with  Auto
normalizes  to:

\mlambda{}N.genfact-inv(N;3;m.4  *  m)

---

Home Index