---

Step * 2 1 1 1 1 2 of Lemma qexpfact_wf


1. x : ℚ
2. p : ℚ
3. 0 < x
4. n : ℕ
5. -(n) ≤ p
6. p ≤ n
7. n1 : ℕ
8. -(n1) ≤ x
9. x ≤ n1
10. ∃m:ℕ. n * n1 ↑ m < (m)!
⊢ ∃m:ℕ. p * x ↑ m < (m)!
BY
{ (ParallelLast THEN InstLemma `qexp_preserves_qle` [⌜x⌝;⌜n1⌝;⌜m⌝]⋅ THEN Auto) }

1
1. x : ℚ
2. p : ℚ
3. 0 < x
4. n : ℕ
5. -(n) ≤ p
6. p ≤ n
7. n1 : ℕ
8. -(n1) ≤ x
9. x ≤ n1
10. m : ℕ
11. n * n1 ↑ m < (m)!
12. x ↑ m ≤ n1 ↑ m
⊢ p * x ↑ m < (m)!

---

Latex:

---

Latex:

1.  x  :  \mBbbQ{}
2.  p  :  \mBbbQ{}
3.  0  <  x
4.  n  :  \mBbbN{}
5.  -(n)  \mleq{}  p
6.  p  \mleq{}  n
7.  n1  :  \mBbbN{}
8.  -(n1)  \mleq{}  x
9.  x  \mleq{}  n1
10.  \mexists{}m:\mBbbN{}.  n  *  n1  \muparrow{}  m  <  (m)!
\mvdash{}  \mexists{}m:\mBbbN{}.  p  *  x  \muparrow{}  m  <  (m)!


By

---

Latex:
(ParallelLast  THEN  InstLemma  `qexp\_preserves\_qle`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}n1\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index