Theorem 2expltfac

Description: The factorial grows faster than two to the power N . (Contributed by Mario Carneiro, 15-Sep-2016)

	Ref	Expression
Assertion	2expltfac	$$⊢N\in {\mathbb{Z}}_{\ge 4}\to 2^N<N!$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢x=4\to 2^x=2^4$$
2		2exp4	$$⊢2^4=16$$
3	1 2	eqtrdi	$$⊢x=4\to 2^x=16$$
4		fveq2	$$⊢x=4\to x!=4!$$
5		fac4	$$⊢4!=24$$
6	4 5	eqtrdi	$$⊢x=4\to x!=24$$
7	3 6	breq12d	$$⊢x=4\to \left(2^x<x!\leftrightarrow 16<24\right)$$
8		oveq2	$$⊢x=n\to 2^x=2^n$$
9		fveq2	$$⊢x=n\to x!=n!$$
10	8 9	breq12d	$$⊢x=n\to \left(2^x<x!\leftrightarrow 2^n<n!\right)$$
11		oveq2	$$⊢x=n+1\to 2^x=2^{n+1}$$
12		fveq2	$$⊢x=n+1\to x!=\left(n+1\right)!$$
13	11 12	breq12d	$$⊢x=n+1\to \left(2^x<x!\leftrightarrow 2^{n+1}<\left(n+1\right)!\right)$$
14		oveq2	$$⊢x=N\to 2^x=2^N$$
15		fveq2	$$⊢x=N\to x!=N!$$
16	14 15	breq12d	$$⊢x=N\to \left(2^x<x!\leftrightarrow 2^N<N!\right)$$
17		1nn0	$$⊢1\in {\mathbb{N}}_0$$
18		2nn0	$$⊢2\in {\mathbb{N}}_0$$
19		6nn0	$$⊢6\in {\mathbb{N}}_0$$
20		4nn0	$$⊢4\in {\mathbb{N}}_0$$
21		6lt10	$$⊢6<10$$
22		1lt2	$$⊢1<2$$
23	17 18 19 20 21 22	decltc	$$⊢16<24$$
24		2nn	$$⊢2\in \mathbb{N}$$
25	24	a1i	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to 2\in \mathbb{N}$$
26		4nn	$$⊢4\in \mathbb{N}$$
27		simpl	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to n\in {\mathbb{Z}}_{\ge 4}$$
28		eluznn	$$⊢\left(4\in \mathbb{N}\wedge n\in {\mathbb{Z}}_{\ge 4}\right)\to n\in \mathbb{N}$$
29	26 27 28	sylancr	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to n\in \mathbb{N}$$
30	29	nnnn0d	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to n\in {\mathbb{N}}_0$$
31	25 30	nnexpcld	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to 2^n\in \mathbb{N}$$
32	31	nnred	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to 2^n\in ℝ$$
33		2re	$$⊢2\in ℝ$$
34	33	a1i	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to 2\in ℝ$$
35	32 34	remulcld	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to 2^n\cdot 2\in ℝ$$
36	30	faccld	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to n!\in \mathbb{N}$$
37	36	nnred	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to n!\in ℝ$$
38	37 34	remulcld	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to n!\cdot 2\in ℝ$$
39	29	nnred	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to n\in ℝ$$
40		1red	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to 1\in ℝ$$
41	39 40	readdcld	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to n+1\in ℝ$$
42	37 41	remulcld	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to n!\left(n+1\right)\in ℝ$$
43		2rp	$$⊢2\in {ℝ}^{+}$$
44	43	a1i	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to 2\in {ℝ}^{+}$$
45		simpr	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to 2^n<n!$$
46	32 37 44 45	ltmul1dd	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to 2^n\cdot 2<n!\cdot 2$$
47	36	nnnn0d	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to n!\in {\mathbb{N}}_0$$
48	47	nn0ge0d	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to 0\le n!$$
49		df-2	$$⊢2=1+1$$
50	29	nnge1d	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to 1\le n$$
51	40 39 40 50	leadd1dd	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to 1+1\le n+1$$
52	49 51	eqbrtrid	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to 2\le n+1$$
53	34 41 37 48 52	lemul2ad	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to n!\cdot 2\le n!\left(n+1\right)$$
54	35 38 42 46 53	ltletrd	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to 2^n\cdot 2<n!\left(n+1\right)$$
55		2cnd	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to 2\in ℂ$$
56	55 30	expp1d	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to 2^{n+1}=2^n\cdot 2$$
57		facp1	$$⊢n\in {\mathbb{N}}_0\to \left(n+1\right)!=n!\left(n+1\right)$$
58	30 57	syl	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to \left(n+1\right)!=n!\left(n+1\right)$$
59	54 56 58	3brtr4d	$$⊢\left(n\in {\mathbb{Z}}_{\ge 4}\wedge 2^n<n!\right)\to 2^{n+1}<\left(n+1\right)!$$
60	59	ex	$$⊢n\in {\mathbb{Z}}_{\ge 4}\to \left(2^n<n!\to 2^{n+1}<\left(n+1\right)!\right)$$
61	7 10 13 16 23 60	uzind4i	$$⊢N\in {\mathbb{Z}}_{\ge 4}\to 2^N<N!$$