Theorem faclbnd3

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

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

Proof

Step	Hyp	Ref	Expression
1		elnn0	$$⊢M\in {\mathbb{N}}_0\leftrightarrow \left(M\in \mathbb{N}\vee M=0\right)$$
2		nnre	$$⊢M\in \mathbb{N}\to M\in ℝ$$
3	2	adantr	$$⊢\left(M\in \mathbb{N}\wedge N\in {\mathbb{N}}_0\right)\to M\in ℝ$$
4		nnge1	$$⊢M\in \mathbb{N}\to 1\le M$$
5	4	adantr	$$⊢\left(M\in \mathbb{N}\wedge N\in {\mathbb{N}}_0\right)\to 1\le M$$
6		nn0z	$$⊢N\in {\mathbb{N}}_0\to N\in \mathbb{Z}$$
7	6	adantl	$$⊢\left(M\in \mathbb{N}\wedge N\in {\mathbb{N}}_0\right)\to N\in \mathbb{Z}$$
8		uzid	$$⊢N\in \mathbb{Z}\to N\in {\mathbb{Z}}_{\ge N}$$
9		peano2uz	$$⊢N\in {\mathbb{Z}}_{\ge N}\to N+1\in {\mathbb{Z}}_{\ge N}$$
10	7 8 9	3syl	$$⊢\left(M\in \mathbb{N}\wedge N\in {\mathbb{N}}_0\right)\to N+1\in {\mathbb{Z}}_{\ge N}$$
11	3 5 10	leexp2ad	$$⊢\left(M\in \mathbb{N}\wedge N\in {\mathbb{N}}_0\right)\to M^N\le M^{N+1}$$
12		nnnn0	$$⊢M\in \mathbb{N}\to M\in {\mathbb{N}}_0$$
13		faclbnd	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to M^{N+1}\le M^{M}N!$$
14	12 13	sylan	$$⊢\left(M\in \mathbb{N}\wedge N\in {\mathbb{N}}_0\right)\to M^{N+1}\le M^{M}N!$$
15		nn0re	$$⊢M\in {\mathbb{N}}_0\to M\in ℝ$$
16		reexpcl	$$⊢\left(M\in ℝ\wedge N\in {\mathbb{N}}_0\right)\to M^N\in ℝ$$
17	15 16	sylan	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to M^N\in ℝ$$
18		peano2nn0	$$⊢N\in {\mathbb{N}}_0\to N+1\in {\mathbb{N}}_0$$
19		reexpcl	$$⊢\left(M\in ℝ\wedge N+1\in {\mathbb{N}}_0\right)\to M^{N+1}\in ℝ$$
20	15 18 19	syl2an	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to M^{N+1}\in ℝ$$
21		reexpcl	$$⊢\left(M\in ℝ\wedge M\in {\mathbb{N}}_0\right)\to M^M\in ℝ$$
22	15 21	mpancom	$$⊢M\in {\mathbb{N}}_0\to M^M\in ℝ$$
23		faccl	$$⊢N\in {\mathbb{N}}_0\to N!\in \mathbb{N}$$
24	23	nnred	$$⊢N\in {\mathbb{N}}_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 {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_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 {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_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 \mathbb{N}\wedge N\in {\mathbb{N}}_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 \mathbb{N}\wedge N\in {\mathbb{N}}_0\right)\to M^N\le M^{M}N!$$
31		elnn0	$$⊢N\in {\mathbb{N}}_0\leftrightarrow \left(N\in \mathbb{N}\vee N=0\right)$$
32		0exp	$$⊢N\in \mathbb{N}\to 0^N=0$$
33		0le1	$$⊢0\le 1$$
34	32 33	eqbrtrdi	$$⊢N\in \mathbb{N}\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 \mathbb{N}\vee N=0\right)\to 0^N\le 1$$
41	31 40	sylbi	$$⊢N\in {\mathbb{N}}_0\to 0^N\le 1$$
42		1nn	$$⊢1\in \mathbb{N}$$
43		nnmulcl	$$⊢\left(1\in \mathbb{N}\wedge N!\in \mathbb{N}\right)\to 1N!\in \mathbb{N}$$
44	42 23 43	sylancr	$$⊢N\in {\mathbb{N}}_0\to 1N!\in \mathbb{N}$$
45	44	nnge1d	$$⊢N\in {\mathbb{N}}_0\to 1\le 1N!$$
46		0re	$$⊢0\in ℝ$$
47		reexpcl	$$⊢\left(0\in ℝ\wedge N\in {\mathbb{N}}_0\right)\to 0^N\in ℝ$$
48	46 47	mpan	$$⊢N\in {\mathbb{N}}_0\to 0^N\in ℝ$$
49		1re	$$⊢1\in ℝ$$
50		remulcl	$$⊢\left(1\in ℝ\wedge N!\in ℝ\right)\to 1N!\in ℝ$$
51	49 24 50	sylancr	$$⊢N\in {\mathbb{N}}_0\to 1N!\in ℝ$$
52		letr	$$⊢\left(0^N\in ℝ\wedge 1\in ℝ\wedge 1N!\in ℝ\right)\to \left(\left(0^N\le 1\wedge 1\le 1N!\right)\to 0^N\le 1N!\right)$$
53	49 52	mp3an2	$$⊢\left(0^N\in ℝ\wedge 1N!\in ℝ\right)\to \left(\left(0^N\le 1\wedge 1\le 1N!\right)\to 0^N\le 1N!\right)$$
54	48 51 53	syl2anc	$$⊢N\in {\mathbb{N}}_0\to \left(\left(0^N\le 1\wedge 1\le 1N!\right)\to 0^N\le 1N!\right)$$
55	41 45 54	mp2and	$$⊢N\in {\mathbb{N}}_0\to 0^N\le 1N!$$
56	55	adantl	$$⊢\left(M=0\wedge N\in {\mathbb{N}}_0\right)\to 0^N\le 1N!$$
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	eqtrdi	$$⊢M=0\to M^M=1$$
61	60	oveq1d	$$⊢M=0\to M^{M}N!=1N!$$
62	57 61	breq12d	$$⊢M=0\to \left(M^N\le M^{M}N!\leftrightarrow 0^N\le 1N!\right)$$
63	62	adantr	$$⊢\left(M=0\wedge N\in {\mathbb{N}}_0\right)\to \left(M^N\le M^{M}N!\leftrightarrow 0^N\le 1N!\right)$$
64	56 63	mpbird	$$⊢\left(M=0\wedge N\in {\mathbb{N}}_0\right)\to M^N\le M^{M}N!$$
65	30 64	jaoian	$$⊢\left(\left(M\in \mathbb{N}\vee M=0\right)\wedge N\in {\mathbb{N}}_0\right)\to M^N\le M^{M}N!$$
66	1 65	sylanb	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to M^N\le M^{M}N!$$