---

Step * of Lemma qexpfact-property

No Annotations
∀[n:ℕ]. ∀[x:{q:ℚ| 0 ≤ q} ]. ∀[p:ℚ]. ∀[b:{b:ℤ| b = (n)! ∈ ℤ} ].  p * x ↑ qexpfact(n;x;p;b) - n < (qexpfact(n;x;p;b))!
BY
{ Assert ⌜∀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))!)⌝⋅ }

1
.....assertion..... 
∀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))!)

2
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))!

---

Latex:

---

Latex:
No  Annotations
\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:
Assert  \mkleeneopen{}\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))!)\mkleeneclose{}
\mcdot{}

---

Home Index