---

Step * of Lemma rexp-approx-lemma

∀N:ℕ+. (∃k:ℕ [(N ≤ (4^k * 3 * (k)!))])
BY
{ ((D 0 THENA Auto) THEN UseWitness ⌜genfact-inv(N;3;m.4 * m)⌝⋅ THEN DoSubsume THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((D  0  THENA  Auto)  THEN  UseWitness  \mkleeneopen{}genfact-inv(N;3;m.4  *  m)\mkleeneclose{}\mcdot{}  THEN  DoSubsume  THEN  Auto)

---

Home Index