---

Step * of Lemma factorial-greater-qexp

∀x:{q:ℚ| 0 ≤ q} . ∀p:ℚ.  ∃n:ℕ. p * x ↑ n < (n)!
BY
{ (Auto
   THEN With ⌜qexpfact(0;x;p;1)⌝ (D 0)⋅
   THEN Auto
   THEN InstLemma `qexpfact-property` [⌜0⌝;⌜x⌝;⌜p⌝;⌜1⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x:\{q:\mBbbQ{}|  0  \mleq{}  q\}  .  \mforall{}p:\mBbbQ{}.    \mexists{}n:\mBbbN{}.  p  *  x  \muparrow{}  n  <  (n)!


By

---

Latex:
(Auto
  THEN  With  \mkleeneopen{}qexpfact(0;x;p;1)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  InstLemma  `qexpfact-property`  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index