---

Step * of Lemma qexpfact_wf

No Annotations
∀[n:ℕ]. ∀[x:{q:ℚ| 0 ≤ q} ]. ∀[p:ℚ]. ∀[b:{b:ℤ| b = (n)! ∈ ℤ} ].  (qexpfact(n;x;p;b) ∈ {n...})
BY
{ ((UnivCD THENA Auto)
   THEN D -1
   THEN HypSubst'  (-1) 0
   THEN ThinVar `b'
   THEN DVar `x'
   THEN ( Decide ⌜x = 0 ∈ ℚ⌝⋅ THENA Auto)) }

1
1. n : ℕ
2. x : ℚ
3. 0 ≤ x
4. p : ℚ
5. x = 0 ∈ ℚ
⊢ qexpfact(n;x;p;(n)!) ∈ {n...}

2
1. n : ℕ
2. x : ℚ
3. 0 ≤ x
4. p : ℚ
5. ¬(x = 0 ∈ ℚ)
⊢ qexpfact(n;x;p;(n)!) ∈ {n...}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbN{}].  \mforall{}[x:\{q:\mBbbQ{}|  0  \mleq{}  q\}  ].  \mforall{}[p:\mBbbQ{}].  \mforall{}[b:\{b:\mBbbZ{}|  b  =  (n)!\}  ].    (qexpfact(n;x;p;b)  \mmember{}  \{n...\})


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  D  -1
  THEN  HypSubst'    (-1)  0
  THEN  ThinVar  `b'
  THEN  DVar  `x'
  THEN  (  Decide  \mkleeneopen{}x  =  0\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index