---

Step * 1 1 of Lemma fact-bound


1. n : ℤ
2. 0 < n
3. (n - 1)! ≤ n - 1^n - 1
4. (n * (n - 1)!) ≤ (n * n - 1^n - 1)
⊢ (n * (n - 1)!) ≤ (n * n^n - 1)
BY
{ (InstLemma `exp_preserves_le` [⌜n - 1⌝;⌜n - 1⌝;⌜n⌝]⋅ THEN Auto)⋅ }

1
1. n : ℤ
2. 0 < n
3. (n - 1)! ≤ n - 1^n - 1
4. (n * (n - 1)!) ≤ (n * n - 1^n - 1)
5. n - 1^n - 1 ≤ n^n - 1
⊢ (n * (n - 1)!) ≤ (n * n^n - 1)

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  (n  -  1)!  \mleq{}  n  -  1\^{}n  -  1
4.  (n  *  (n  -  1)!)  \mleq{}  (n  *  n  -  1\^{}n  -  1)
\mvdash{}  (n  *  (n  -  1)!)  \mleq{}  (n  *  n\^{}n  -  1)


By

---

Latex:
(InstLemma  `exp\_preserves\_le`  [\mkleeneopen{}n  -  1\mkleeneclose{};\mkleeneopen{}n  -  1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index