---

Step * 2 of Lemma qexpfact-property


1. ∀d:ℕ
     ∀[n:ℕ]. ∀[x:{q:ℚ| 0 ≤ q} ]. ∀[p:ℚ]. ∀[b:{b:ℤ| b = (n)! ∈ ℤ} ].
       (((qexpfact(n;x;p;b) - n) ≤ d) ⇒ p * x ↑ qexpfact(n;x;p;b) - n < (qexpfact(n;x;p;b))!)
⊢ ∀[n:ℕ]. ∀[x:{q:ℚ| 0 ≤ q} ]. ∀[p:ℚ]. ∀[b:{b:ℤ| b = (n)! ∈ ℤ} ].  p * x ↑ qexpfact(n;x;p;b) - n < (qexpfact(n;x;p;b))!
BY
{ TACTIC:((Auto THEN InstHyp [⌜qexpfact(n;x;p;b) - n⌝;⌜n⌝;⌜x⌝;⌜p⌝;⌜b⌝] 1⋅) THEN Auto') }

---

Latex:

---

Latex:

1.  \mforall{}d:\mBbbN{}
          \mforall{}[n:\mBbbN{}].  \mforall{}[x:\{q:\mBbbQ{}|  0  \mleq{}  q\}  ].  \mforall{}[p:\mBbbQ{}].  \mforall{}[b:\{b:\mBbbZ{}|  b  =  (n)!\}  ].
              (((qexpfact(n;x;p;b)  -  n)  \mleq{}  d)  {}\mRightarrow{}  p  *  x  \muparrow{}  qexpfact(n;x;p;b)  -  n  <  (qexpfact(n;x;p;b))!)
\mvdash{}  \mforall{}[n:\mBbbN{}].  \mforall{}[x:\{q:\mBbbQ{}|  0  \mleq{}  q\}  ].  \mforall{}[p:\mBbbQ{}].  \mforall{}[b:\{b:\mBbbZ{}|  b  =  (n)!\}  ].
        p  *  x  \muparrow{}  qexpfact(n;x;p;b)  -  n  <  (qexpfact(n;x;p;b))!


By

---

Latex:
TACTIC:((Auto  THEN  InstHyp  [\mkleeneopen{}qexpfact(n;x;p;b)  -  n\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  1\mcdot{})  THEN  Auto')

---

Home Index