---

Step * 2 of Lemma qexpfact_wf


1. n : ℕ
2. x : ℚ
3. 0 ≤ x
4. p : ℚ
5. ¬(x = 0 ∈ ℚ)
⊢ qexpfact(n;x;p;(n)!) ∈ {n...}
BY
{ ((Assert 0 < x BY
          (TACTIC:BLemma `qle_complement_qorder` THEN Auto THEN ParallelLast THEN RelRST THEN Auto))
   THEN Thin (-2)
   THEN Thin (-3)) }

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

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  x  :  \mBbbQ{}
3.  0  \mleq{}  x
4.  p  :  \mBbbQ{}
5.  \mneg{}(x  =  0)
\mvdash{}  qexpfact(n;x;p;(n)!)  \mmember{}  \{n...\}


By

---

Latex:
((Assert  0  <  x  BY
                (TACTIC:BLemma  `qle\_complement\_qorder`  THEN  Auto  THEN  ParallelLast  THEN  RelRST  THEN  Auto))
  THEN  Thin  (-2)
  THEN  Thin  (-3))

---

Home Index