faclbnd5

Description: The factorial function grows faster than powers and exponentiations. If we consider K and M to be constants, the right-hand side of the inequality is a constant times N -factorial. (Contributed by NM, 24-Dec-2005)

		Ref	Expression
	Assertion	faclbnd5	$⊢ (N \in ℕ_{0} \land K \in ℕ_{0} \land M \in ℕ) \to N^{K} M^{N} < 2 2^{K^{2}} M^{M + K} N!$

Proof

Step	Hyp	Ref	Expression
1		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
2		reexpcl	$⊢ (N \in ℝ \land K \in ℕ_{0}) \to N^{K} \in ℝ$
3	1 2	sylan	$⊢ (N \in ℕ_{0} \land K \in ℕ_{0}) \to N^{K} \in ℝ$
4	3	ancoms	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0}) \to N^{K} \in ℝ$
5		nnre	$⊢ M \in ℕ \to M \in ℝ$
6		reexpcl	$⊢ (M \in ℝ \land N \in ℕ_{0}) \to M^{N} \in ℝ$
7	5 6	sylan	$⊢ (M \in ℕ \land N \in ℕ_{0}) \to M^{N} \in ℝ$
8		remulcl	$⊢ (N^{K} \in ℝ \land M^{N} \in ℝ) \to N^{K} M^{N} \in ℝ$
9	4 7 8	syl2an	$⊢ ((K \in ℕ_{0} \land N \in ℕ_{0}) \land (M \in ℕ \land N \in ℕ_{0})) \to N^{K} M^{N} \in ℝ$
10	9	anandirs	$⊢ ((K \in ℕ_{0} \land M \in ℕ) \land N \in ℕ_{0}) \to N^{K} M^{N} \in ℝ$
11		2nn	$⊢ 2 \in ℕ$
12		nn0sqcl	$⊢ K \in ℕ_{0} \to K^{2} \in ℕ_{0}$
13		nnexpcl	$⊢ (2 \in ℕ \land K^{2} \in ℕ_{0}) \to 2^{K^{2}} \in ℕ$
14	11 12 13	sylancr	$⊢ K \in ℕ_{0} \to 2^{K^{2}} \in ℕ$
15		nnnn0	$⊢ M \in ℕ \to M \in ℕ_{0}$
16		nn0addcl	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0}) \to M + K \in ℕ_{0}$
17	16	ancoms	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to M + K \in ℕ_{0}$
18	15 17	sylan2	$⊢ (K \in ℕ_{0} \land M \in ℕ) \to M + K \in ℕ_{0}$
19		nnexpcl	$⊢ (M \in ℕ \land M + K \in ℕ_{0}) \to M^{M + K} \in ℕ$
20	18 19	sylan2	$⊢ (M \in ℕ \land (K \in ℕ_{0} \land M \in ℕ)) \to M^{M + K} \in ℕ$
21	20	anabss7	$⊢ (K \in ℕ_{0} \land M \in ℕ) \to M^{M + K} \in ℕ$
22		nnmulcl	$⊢ (2^{K^{2}} \in ℕ \land M^{M + K} \in ℕ) \to 2^{K^{2}} M^{M + K} \in ℕ$
23	14 21 22	syl2an2r	$⊢ (K \in ℕ_{0} \land M \in ℕ) \to 2^{K^{2}} M^{M + K} \in ℕ$
24	23	nnred	$⊢ (K \in ℕ_{0} \land M \in ℕ) \to 2^{K^{2}} M^{M + K} \in ℝ$
25		faccl	$⊢ N \in ℕ_{0} \to N! \in ℕ$
26	25	nnred	$⊢ N \in ℕ_{0} \to N! \in ℝ$
27		remulcl	$⊢ (2^{K^{2}} M^{M + K} \in ℝ \land N! \in ℝ) \to 2^{K^{2}} M^{M + K} N! \in ℝ$
28	24 26 27	syl2an	$⊢ ((K \in ℕ_{0} \land M \in ℕ) \land N \in ℕ_{0}) \to 2^{K^{2}} M^{M + K} N! \in ℝ$
29		2re	$⊢ 2 \in ℝ$
30		remulcl	$⊢ (2 \in ℝ \land 2^{K^{2}} M^{M + K} N! \in ℝ) \to 2 2^{K^{2}} M^{M + K} N! \in ℝ$
31	29 28 30	sylancr	$⊢ ((K \in ℕ_{0} \land M \in ℕ) \land N \in ℕ_{0}) \to 2 2^{K^{2}} M^{M + K} N! \in ℝ$
32		faclbnd4	$⊢ (N \in ℕ_{0} \land K \in ℕ_{0} \land M \in ℕ_{0}) \to N^{K} M^{N} \leq 2^{K^{2}} M^{M + K} N!$
33	15 32	syl3an3	$⊢ (N \in ℕ_{0} \land K \in ℕ_{0} \land M \in ℕ) \to N^{K} M^{N} \leq 2^{K^{2}} M^{M + K} N!$
34	33	3coml	$⊢ (K \in ℕ_{0} \land M \in ℕ \land N \in ℕ_{0}) \to N^{K} M^{N} \leq 2^{K^{2}} M^{M + K} N!$
35	34	3expa	$⊢ ((K \in ℕ_{0} \land M \in ℕ) \land N \in ℕ_{0}) \to N^{K} M^{N} \leq 2^{K^{2}} M^{M + K} N!$
36		1lt2	$⊢ 1 < 2$
37		nnmulcl	$⊢ (2^{K^{2}} M^{M + K} \in ℕ \land N! \in ℕ) \to 2^{K^{2}} M^{M + K} N! \in ℕ$
38	23 25 37	syl2an	$⊢ ((K \in ℕ_{0} \land M \in ℕ) \land N \in ℕ_{0}) \to 2^{K^{2}} M^{M + K} N! \in ℕ$
39	38	nngt0d	$⊢ ((K \in ℕ_{0} \land M \in ℕ) \land N \in ℕ_{0}) \to 0 < 2^{K^{2}} M^{M + K} N!$
40		ltmulgt12	$⊢ (2^{K^{2}} M^{M + K} N! \in ℝ \land 2 \in ℝ \land 0 < 2^{K^{2}} M^{M + K} N!) \to (1 < 2 \leftrightarrow 2^{K^{2}} M^{M + K} N! < 2 2^{K^{2}} M^{M + K} N!)$
41	29 40	mp3an2	$⊢ (2^{K^{2}} M^{M + K} N! \in ℝ \land 0 < 2^{K^{2}} M^{M + K} N!) \to (1 < 2 \leftrightarrow 2^{K^{2}} M^{M + K} N! < 2 2^{K^{2}} M^{M + K} N!)$
42	28 39 41	syl2anc	$⊢ ((K \in ℕ_{0} \land M \in ℕ) \land N \in ℕ_{0}) \to (1 < 2 \leftrightarrow 2^{K^{2}} M^{M + K} N! < 2 2^{K^{2}} M^{M + K} N!)$
43	36 42	mpbii	$⊢ ((K \in ℕ_{0} \land M \in ℕ) \land N \in ℕ_{0}) \to 2^{K^{2}} M^{M + K} N! < 2 2^{K^{2}} M^{M + K} N!$
44	10 28 31 35 43	lelttrd	$⊢ ((K \in ℕ_{0} \land M \in ℕ) \land N \in ℕ_{0}) \to N^{K} M^{N} < 2 2^{K^{2}} M^{M + K} N!$
45		2cn	$⊢ 2 \in ℂ$
46	23	nncnd	$⊢ (K \in ℕ_{0} \land M \in ℕ) \to 2^{K^{2}} M^{M + K} \in ℂ$
47	25	nncnd	$⊢ N \in ℕ_{0} \to N! \in ℂ$
48		mulass	$⊢ (2 \in ℂ \land 2^{K^{2}} M^{M + K} \in ℂ \land N! \in ℂ) \to 2 2^{K^{2}} M^{M + K} N! = 2 2^{K^{2}} M^{M + K} N!$
49	45 46 47 48	mp3an3an	$⊢ ((K \in ℕ_{0} \land M \in ℕ) \land N \in ℕ_{0}) \to 2 2^{K^{2}} M^{M + K} N! = 2 2^{K^{2}} M^{M + K} N!$
50	44 49	breqtrrd	$⊢ ((K \in ℕ_{0} \land M \in ℕ) \land N \in ℕ_{0}) \to N^{K} M^{N} < 2 2^{K^{2}} M^{M + K} N!$
51	50	3impa	$⊢ (K \in ℕ_{0} \land M \in ℕ \land N \in ℕ_{0}) \to N^{K} M^{N} < 2 2^{K^{2}} M^{M + K} N!$
52	51	3comr	$⊢ (N \in ℕ_{0} \land K \in ℕ_{0} \land M \in ℕ) \to N^{K} M^{N} < 2 2^{K^{2}} M^{M + K} N!$

Metamath Proof Explorer

Theorem faclbnd5

Proof