Theorem facubnd

Description: An upper bound for the factorial function. (Contributed by Mario Carneiro, 15-Apr-2016)

	Ref	Expression
Assertion	facubnd	$$⊢N\in {\mathbb{N}}_0\to N!\le N^N$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢m=0\to m!=0!$$
2		fac0	$$⊢0!=1$$
3	1 2	eqtrdi	$$⊢m=0\to m!=1$$
4		id	$$⊢m=0\to m=0$$
5	4 4	oveq12d	$$⊢m=0\to m^m=0^0$$
6		0exp0e1	$$⊢0^0=1$$
7	5 6	eqtrdi	$$⊢m=0\to m^m=1$$
8	3 7	breq12d	$$⊢m=0\to \left(m!\le m^m\leftrightarrow 1\le 1\right)$$
9		fveq2	$$⊢m=k\to m!=k!$$
10		id	$$⊢m=k\to m=k$$
11	10 10	oveq12d	$$⊢m=k\to m^m=k^k$$
12	9 11	breq12d	$$⊢m=k\to \left(m!\le m^m\leftrightarrow k!\le k^k\right)$$
13		fveq2	$$⊢m=k+1\to m!=\left(k+1\right)!$$
14		id	$$⊢m=k+1\to m=k+1$$
15	14 14	oveq12d	$$⊢m=k+1\to m^m={\left(k+1\right)}^{k+1}$$
16	13 15	breq12d	$$⊢m=k+1\to \left(m!\le m^m\leftrightarrow \left(k+1\right)!\le {\left(k+1\right)}^{k+1}\right)$$
17		fveq2	$$⊢m=N\to m!=N!$$
18		id	$$⊢m=N\to m=N$$
19	18 18	oveq12d	$$⊢m=N\to m^m=N^N$$
20	17 19	breq12d	$$⊢m=N\to \left(m!\le m^m\leftrightarrow N!\le N^N\right)$$
21		1le1	$$⊢1\le 1$$
22		faccl	$$⊢k\in {\mathbb{N}}_0\to k!\in \mathbb{N}$$
23	22	adantr	$$⊢\left(k\in {\mathbb{N}}_0\wedge k!\le k^k\right)\to k!\in \mathbb{N}$$
24	23	nnred	$$⊢\left(k\in {\mathbb{N}}_0\wedge k!\le k^k\right)\to k!\in ℝ$$
25		nn0re	$$⊢k\in {\mathbb{N}}_0\to k\in ℝ$$
26	25	adantr	$$⊢\left(k\in {\mathbb{N}}_0\wedge k!\le k^k\right)\to k\in ℝ$$
27		simpl	$$⊢\left(k\in {\mathbb{N}}_0\wedge k!\le k^k\right)\to k\in {\mathbb{N}}_0$$
28	26 27	reexpcld	$$⊢\left(k\in {\mathbb{N}}_0\wedge k!\le k^k\right)\to k^k\in ℝ$$
29		nn0p1nn	$$⊢k\in {\mathbb{N}}_0\to k+1\in \mathbb{N}$$
30	29	adantr	$$⊢\left(k\in {\mathbb{N}}_0\wedge k!\le k^k\right)\to k+1\in \mathbb{N}$$
31	30	nnred	$$⊢\left(k\in {\mathbb{N}}_0\wedge k!\le k^k\right)\to k+1\in ℝ$$
32	31 27	reexpcld	$$⊢\left(k\in {\mathbb{N}}_0\wedge k!\le k^k\right)\to {\left(k+1\right)}^k\in ℝ$$
33		simpr	$$⊢\left(k\in {\mathbb{N}}_0\wedge k!\le k^k\right)\to k!\le k^k$$
34		nn0ge0	$$⊢k\in {\mathbb{N}}_0\to 0\le k$$
35	34	adantr	$$⊢\left(k\in {\mathbb{N}}_0\wedge k!\le k^k\right)\to 0\le k$$
36	26	lep1d	$$⊢\left(k\in {\mathbb{N}}_0\wedge k!\le k^k\right)\to k\le k+1$$
37		leexp1a	$$⊢\left(\left(k\in ℝ\wedge k+1\in ℝ\wedge k\in {\mathbb{N}}_0\right)\wedge \left(0\le k\wedge k\le k+1\right)\right)\to k^k\le {\left(k+1\right)}^k$$
38	26 31 27 35 36 37	syl32anc	$$⊢\left(k\in {\mathbb{N}}_0\wedge k!\le k^k\right)\to k^k\le {\left(k+1\right)}^k$$
39	24 28 32 33 38	letrd	$$⊢\left(k\in {\mathbb{N}}_0\wedge k!\le k^k\right)\to k!\le {\left(k+1\right)}^k$$
40	30	nngt0d	$$⊢\left(k\in {\mathbb{N}}_0\wedge k!\le k^k\right)\to 0<k+1$$
41		lemul1	$$⊢\left(k!\in ℝ\wedge {\left(k+1\right)}^k\in ℝ\wedge \left(k+1\in ℝ\wedge 0<k+1\right)\right)\to \left(k!\le {\left(k+1\right)}^k\leftrightarrow k!\left(k+1\right)\le {\left(k+1\right)}^k\left(k+1\right)\right)$$
42	24 32 31 40 41	syl112anc	$$⊢\left(k\in {\mathbb{N}}_0\wedge k!\le k^k\right)\to \left(k!\le {\left(k+1\right)}^k\leftrightarrow k!\left(k+1\right)\le {\left(k+1\right)}^k\left(k+1\right)\right)$$
43	39 42	mpbid	$$⊢\left(k\in {\mathbb{N}}_0\wedge k!\le k^k\right)\to k!\left(k+1\right)\le {\left(k+1\right)}^k\left(k+1\right)$$
44		facp1	$$⊢k\in {\mathbb{N}}_0\to \left(k+1\right)!=k!\left(k+1\right)$$
45	44	adantr	$$⊢\left(k\in {\mathbb{N}}_0\wedge k!\le k^k\right)\to \left(k+1\right)!=k!\left(k+1\right)$$
46	30	nncnd	$$⊢\left(k\in {\mathbb{N}}_0\wedge k!\le k^k\right)\to k+1\in ℂ$$
47	46 27	expp1d	$$⊢\left(k\in {\mathbb{N}}_0\wedge k!\le k^k\right)\to {\left(k+1\right)}^{k+1}={\left(k+1\right)}^k\left(k+1\right)$$
48	43 45 47	3brtr4d	$$⊢\left(k\in {\mathbb{N}}_0\wedge k!\le k^k\right)\to \left(k+1\right)!\le {\left(k+1\right)}^{k+1}$$
49	48	ex	$$⊢k\in {\mathbb{N}}_0\to \left(k!\le k^k\to \left(k+1\right)!\le {\left(k+1\right)}^{k+1}\right)$$
50	8 12 16 20 21 49	nn0ind	$$⊢N\in {\mathbb{N}}_0\to N!\le N^N$$