# Metamath Proof Explorer

## Theorem faclbnd3

Description: A lower bound for the factorial function. (Contributed by NM, 19-Dec-2005)

Ref Expression
Assertion faclbnd3 ${⊢}\left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {{M}}^{{N}}\le {{M}}^{{M}}{N}!$

### Proof

Step Hyp Ref Expression
1 elnn0 ${⊢}{M}\in {ℕ}_{0}↔\left({M}\in ℕ\vee {M}=0\right)$
2 nnre ${⊢}{M}\in ℕ\to {M}\in ℝ$
3 2 adantr ${⊢}\left({M}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\to {M}\in ℝ$
4 nnge1 ${⊢}{M}\in ℕ\to 1\le {M}$
5 4 adantr ${⊢}\left({M}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\to 1\le {M}$
6 nn0z ${⊢}{N}\in {ℕ}_{0}\to {N}\in ℤ$
7 6 adantl ${⊢}\left({M}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\to {N}\in ℤ$
8 uzid ${⊢}{N}\in ℤ\to {N}\in {ℤ}_{\ge {N}}$
9 peano2uz ${⊢}{N}\in {ℤ}_{\ge {N}}\to {N}+1\in {ℤ}_{\ge {N}}$
10 7 8 9 3syl ${⊢}\left({M}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\to {N}+1\in {ℤ}_{\ge {N}}$
11 3 5 10 leexp2ad ${⊢}\left({M}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\to {{M}}^{{N}}\le {{M}}^{{N}+1}$
12 nnnn0 ${⊢}{M}\in ℕ\to {M}\in {ℕ}_{0}$
13 faclbnd ${⊢}\left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {{M}}^{{N}+1}\le {{M}}^{{M}}{N}!$
14 12 13 sylan ${⊢}\left({M}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\to {{M}}^{{N}+1}\le {{M}}^{{M}}{N}!$
15 nn0re ${⊢}{M}\in {ℕ}_{0}\to {M}\in ℝ$
16 reexpcl ${⊢}\left({M}\in ℝ\wedge {N}\in {ℕ}_{0}\right)\to {{M}}^{{N}}\in ℝ$
17 15 16 sylan ${⊢}\left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {{M}}^{{N}}\in ℝ$
18 peano2nn0 ${⊢}{N}\in {ℕ}_{0}\to {N}+1\in {ℕ}_{0}$
19 reexpcl ${⊢}\left({M}\in ℝ\wedge {N}+1\in {ℕ}_{0}\right)\to {{M}}^{{N}+1}\in ℝ$
20 15 18 19 syl2an ${⊢}\left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {{M}}^{{N}+1}\in ℝ$
21 reexpcl ${⊢}\left({M}\in ℝ\wedge {M}\in {ℕ}_{0}\right)\to {{M}}^{{M}}\in ℝ$
22 15 21 mpancom ${⊢}{M}\in {ℕ}_{0}\to {{M}}^{{M}}\in ℝ$
23 faccl ${⊢}{N}\in {ℕ}_{0}\to {N}!\in ℕ$
24 23 nnred ${⊢}{N}\in {ℕ}_{0}\to {N}!\in ℝ$
25 remulcl ${⊢}\left({{M}}^{{M}}\in ℝ\wedge {N}!\in ℝ\right)\to {{M}}^{{M}}{N}!\in ℝ$
26 22 24 25 syl2an ${⊢}\left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {{M}}^{{M}}{N}!\in ℝ$
27 letr ${⊢}\left({{M}}^{{N}}\in ℝ\wedge {{M}}^{{N}+1}\in ℝ\wedge {{M}}^{{M}}{N}!\in ℝ\right)\to \left(\left({{M}}^{{N}}\le {{M}}^{{N}+1}\wedge {{M}}^{{N}+1}\le {{M}}^{{M}}{N}!\right)\to {{M}}^{{N}}\le {{M}}^{{M}}{N}!\right)$
28 17 20 26 27 syl3anc ${⊢}\left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left(\left({{M}}^{{N}}\le {{M}}^{{N}+1}\wedge {{M}}^{{N}+1}\le {{M}}^{{M}}{N}!\right)\to {{M}}^{{N}}\le {{M}}^{{M}}{N}!\right)$
29 12 28 sylan ${⊢}\left({M}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\to \left(\left({{M}}^{{N}}\le {{M}}^{{N}+1}\wedge {{M}}^{{N}+1}\le {{M}}^{{M}}{N}!\right)\to {{M}}^{{N}}\le {{M}}^{{M}}{N}!\right)$
30 11 14 29 mp2and ${⊢}\left({M}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\to {{M}}^{{N}}\le {{M}}^{{M}}{N}!$
31 elnn0 ${⊢}{N}\in {ℕ}_{0}↔\left({N}\in ℕ\vee {N}=0\right)$
32 0exp ${⊢}{N}\in ℕ\to {0}^{{N}}=0$
33 0le1 ${⊢}0\le 1$
34 32 33 eqbrtrdi ${⊢}{N}\in ℕ\to {0}^{{N}}\le 1$
35 oveq2 ${⊢}{N}=0\to {0}^{{N}}={0}^{0}$
36 0exp0e1 ${⊢}{0}^{0}=1$
37 1le1 ${⊢}1\le 1$
38 36 37 eqbrtri ${⊢}{0}^{0}\le 1$
39 35 38 eqbrtrdi ${⊢}{N}=0\to {0}^{{N}}\le 1$
40 34 39 jaoi ${⊢}\left({N}\in ℕ\vee {N}=0\right)\to {0}^{{N}}\le 1$
41 31 40 sylbi ${⊢}{N}\in {ℕ}_{0}\to {0}^{{N}}\le 1$
42 1nn ${⊢}1\in ℕ$
43 nnmulcl ${⊢}\left(1\in ℕ\wedge {N}!\in ℕ\right)\to 1{N}!\in ℕ$
44 42 23 43 sylancr ${⊢}{N}\in {ℕ}_{0}\to 1{N}!\in ℕ$
45 44 nnge1d ${⊢}{N}\in {ℕ}_{0}\to 1\le 1{N}!$
46 0re ${⊢}0\in ℝ$
47 reexpcl ${⊢}\left(0\in ℝ\wedge {N}\in {ℕ}_{0}\right)\to {0}^{{N}}\in ℝ$
48 46 47 mpan ${⊢}{N}\in {ℕ}_{0}\to {0}^{{N}}\in ℝ$
49 1re ${⊢}1\in ℝ$
50 remulcl ${⊢}\left(1\in ℝ\wedge {N}!\in ℝ\right)\to 1{N}!\in ℝ$
51 49 24 50 sylancr ${⊢}{N}\in {ℕ}_{0}\to 1{N}!\in ℝ$
52 letr ${⊢}\left({0}^{{N}}\in ℝ\wedge 1\in ℝ\wedge 1{N}!\in ℝ\right)\to \left(\left({0}^{{N}}\le 1\wedge 1\le 1{N}!\right)\to {0}^{{N}}\le 1{N}!\right)$
53 49 52 mp3an2 ${⊢}\left({0}^{{N}}\in ℝ\wedge 1{N}!\in ℝ\right)\to \left(\left({0}^{{N}}\le 1\wedge 1\le 1{N}!\right)\to {0}^{{N}}\le 1{N}!\right)$
54 48 51 53 syl2anc ${⊢}{N}\in {ℕ}_{0}\to \left(\left({0}^{{N}}\le 1\wedge 1\le 1{N}!\right)\to {0}^{{N}}\le 1{N}!\right)$
55 41 45 54 mp2and ${⊢}{N}\in {ℕ}_{0}\to {0}^{{N}}\le 1{N}!$
56 55 adantl ${⊢}\left({M}=0\wedge {N}\in {ℕ}_{0}\right)\to {0}^{{N}}\le 1{N}!$
57 oveq1 ${⊢}{M}=0\to {{M}}^{{N}}={0}^{{N}}$
58 oveq12 ${⊢}\left({M}=0\wedge {M}=0\right)\to {{M}}^{{M}}={0}^{0}$
59 58 anidms ${⊢}{M}=0\to {{M}}^{{M}}={0}^{0}$
60 59 36 syl6eq ${⊢}{M}=0\to {{M}}^{{M}}=1$
61 60 oveq1d ${⊢}{M}=0\to {{M}}^{{M}}{N}!=1{N}!$
62 57 61 breq12d ${⊢}{M}=0\to \left({{M}}^{{N}}\le {{M}}^{{M}}{N}!↔{0}^{{N}}\le 1{N}!\right)$
63 62 adantr ${⊢}\left({M}=0\wedge {N}\in {ℕ}_{0}\right)\to \left({{M}}^{{N}}\le {{M}}^{{M}}{N}!↔{0}^{{N}}\le 1{N}!\right)$
64 56 63 mpbird ${⊢}\left({M}=0\wedge {N}\in {ℕ}_{0}\right)\to {{M}}^{{N}}\le {{M}}^{{M}}{N}!$
65 30 64 jaoian ${⊢}\left(\left({M}\in ℕ\vee {M}=0\right)\wedge {N}\in {ℕ}_{0}\right)\to {{M}}^{{N}}\le {{M}}^{{M}}{N}!$
66 1 65 sylanb ${⊢}\left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {{M}}^{{N}}\le {{M}}^{{M}}{N}!$