---

Step * 1 of Lemma fact-greater-exp

.....assertion..... 
∀k:ℕ+. ∀m:ℕ.  (((k - 1)! * k^m * (m + k)) ≤ (m + k)!)
BY
{ ((D 0 THENA Auto) THEN InductionOnNat THEN Reduce 0 THEN RW (AddrC [2] (LemmaC `fact_unroll_1`)) 0 THEN Auto) }

1
1. k : ℕ+@i
2. m : ℤ
⊢ ((k - 1)! * 1 * (0 + k)) ≤ ((0 + k) * ((0 + k) - 1)!)

2
1. k : ℕ+@i
2. m : ℤ
3. 0 < m
4. ((k - 1)! * k^m - 1 * ((m - 1) + k)) ≤ ((m - 1) + k)!
⊢ ((k - 1)! * k^m * (m + k)) ≤ ((m + k) * ((m + k) - 1)!)

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}k:\mBbbN{}\msupplus{}.  \mforall{}m:\mBbbN{}.    (((k  -  1)!  *  k\^{}m  *  (m  +  k))  \mleq{}  (m  +  k)!)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  InductionOnNat
  THEN  Reduce  0
  THEN  RW  (AddrC  [2]  (LemmaC  `fact\_unroll\_1`))  0
  THEN  Auto)

---

Home Index