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

Metamath Proof Explorer

Theorem 2expltfac

Proof