Step * 2 1 1 1 1 2 1 1 of Lemma qexpfact_wf


1. : ℚ
2. : ℚ
3. 0 < x
4. : ℕ
5. -(n) ≤ p
6. p ≤ n
7. n1 : ℕ
8. -(n1) ≤ x
9. x ≤ n1
10. : ℕ
11. n1 ↑ m < (m)!
12. (x ↑ n) ≤ (n1 ↑ n)
⊢ x ↑ m < (m)!
BY
(QMul ⌜x ↑ m⌝ 6⋅ THEN Auto) }

1
1. : ℚ
2. : ℚ
3. 0 < x
4. : ℕ
5. -(n) ≤ p
6. n1 : ℕ
7. -(n1) ≤ x
8. x ≤ n1
9. : ℕ
10. (x ↑ n) ≤ (n1 ↑ n)
11. n1 ↑ m < (m)!
12. (x ↑ p) ≤ (x ↑ n)
⊢ 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.  m  :  \mBbbN{}
11.  n  *  n1  \muparrow{}  m  <  (m)!
12.  (x  \muparrow{}  m  *  n)  \mleq{}  (n1  \muparrow{}  m  *  n)
\mvdash{}  p  *  x  \muparrow{}  m  <  (m)!


By


Latex:
(QMul  \mkleeneopen{}x  \muparrow{}  m\mkleeneclose{}  6\mcdot{}  THEN  Auto)




Home Index