Step
*
2
1
1
1
1
1
2
1
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 : ℕ
11. n * n1^m < (m)!
⊢ n * n1 ↑ m < (m)!
BY
{ ((RWO "qexp-exp" 0 THENA Auto) THEN (RWO "qmul-mul" 0 THENA 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)!
⊢ n * n1^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.  m  :  \mBbbN{}
11.  n  *  n1\^{}m  <  (m)!
\mvdash{}  n  *  n1  \muparrow{}  m  <  (m)!
By
Latex:
((RWO  "qexp-exp"  0  THENA  Auto)  THEN  (RWO  "qmul-mul"  0  THENA  Auto))\mcdot{}
Home
Index