Theorem faclbnd5 7076

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.

Assertion

Ref	Expression
faclbnd5	|- ((N e. NN0 /\ K e. NN0 /\ M e. NN) -> ((N^K) x. (M^N)) < ((2 x. ((2^(K^2)) x. (M^(M + K)))) x. (!` N)))

Proof of Theorem faclbnd5

Step	Hyp	Ref	Expression
1		remulcl 5393	. . . . . . 7 |- (((N^K) e. RR /\ (M^N) e. RR) -> ((N^K) x. (M^N)) e. RR)
2		reexpcl 6703	. . . . . . . . 9 |- ((N e. RR /\ K e. NN0) -> (N^K) e. RR)
3		nn0re 6218	. . . . . . . . 9 |- (N e. NN0 -> N e. RR)
4	2, 3	sylan 450	. . . . . . . 8 |- ((N e. NN0 /\ K e. NN0) -> (N^K) e. RR)
5	4	ancoms 438	. . . . . . 7 |- ((K e. NN0 /\ N e. NN0) -> (N^K) e. RR)
6		reexpcl 6703	. . . . . . . 8 |- ((M e. RR /\ N e. NN0) -> (M^N) e. RR)
7		nnre 6016	. . . . . . . 8 |- (M e. NN -> M e. RR)
8	6, 7	sylan 450	. . . . . . 7 |- ((M e. NN /\ N e. NN0) -> (M^N) e. RR)
9	1, 5, 8	syl2an 456	. . . . . 6 |- (((K e. NN0 /\ N e. NN0) /\ (M e. NN /\ N e. NN0)) -> ((N^K) x. (M^N)) e. RR)
10	9	anandirs 515	. . . . 5 |- (((K e. NN0 /\ M e. NN) /\ N e. NN0) -> ((N^K) x. (M^N)) e. RR)
11		remulcl 5393	. . . . . 6 |- ((((2^(K^2)) x. (M^(M + K))) e. RR /\ (!` N) e. RR) -> (((2^(K^2)) x. (M^(M + K))) x. (!` N)) e. RR)
12		nnmulcl 6028	. . . . . . . . 9 |- (((2^(K^2)) e. NN /\ (M^(M + K)) e. NN) -> ((2^(K^2)) x. (M^(M + K))) e. NN)
13		2nn0 6225	. . . . . . . . . . 11 |- 2 e. NN0
14		nn0expcl 6700	. . . . . . . . . . 11 |- ((K e. NN0 /\ 2 e. NN0) -> (K^2) e. NN0)
15	13, 14	mpan2 699	. . . . . . . . . 10 |- (K e. NN0 -> (K^2) e. NN0)
16		2nn 6087	. . . . . . . . . . 11 |- 2 e. NN
17		nnexpcl 6699	. . . . . . . . . . 11 |- ((2 e. NN /\ (K^2) e. NN0) -> (2^(K^2)) e. NN)
18	16, 17	mpan 698	. . . . . . . . . 10 |- ((K^2) e. NN0 -> (2^(K^2)) e. NN)
19	15, 18	syl 10	. . . . . . . . 9 |- (K e. NN0 -> (2^(K^2)) e. NN)
20		nnexpcl 6699	. . . . . . . . . . 11 |- ((M e. NN /\ (M + K) e. NN0) -> (M^(M + K)) e. NN)
21		nn0addcl 6230	. . . . . . . . . . . . 13 |- ((M e. NN0 /\ K e. NN0) -> (M + K) e. NN0)
22	21	ancoms 438	. . . . . . . . . . . 12 |- ((K e. NN0 /\ M e. NN0) -> (M + K) e. NN0)
23		nnnn0 6216	. . . . . . . . . . . 12 |- (M e. NN -> M e. NN0)
24	22, 23	sylan2 453	. . . . . . . . . . 11 |- ((K e. NN0 /\ M e. NN) -> (M + K) e. NN0)
25	20, 24	sylan2 453	. . . . . . . . . 10 |- ((M e. NN /\ (K e. NN0 /\ M e. NN)) -> (M^(M + K)) e. NN)
26	25	anabss7 505	. . . . . . . . 9 |- ((K e. NN0 /\ M e. NN) -> (M^(M + K)) e. NN)
27	12, 19, 26	syl2an 456	. . . . . . . 8 |- ((K e. NN0 /\ (K e. NN0 /\ M e. NN)) -> ((2^(K^2)) x. (M^(M + K))) e. NN)
28	27	anabss5 504	. . . . . . 7 |- ((K e. NN0 /\ M e. NN) -> ((2^(K^2)) x. (M^(M + K))) e. NN)
29		nnre 6016	. . . . . . 7 |- (((2^(K^2)) x. (M^(M + K))) e. NN -> ((2^(K^2)) x. (M^(M + K))) e. RR)
30	28, 29	syl 10	. . . . . 6 |- ((K e. NN0 /\ M e. NN) -> ((2^(K^2)) x. (M^(M + K))) e. RR)
31		faccl 7063	. . . . . . 7 |- (N e. NN0 -> (!` N) e. NN)
32		nnre 6016	. . . . . . 7 |- ((!` N) e. NN -> (!` N) e. RR)
33	31, 32	syl 10	. . . . . 6 |- (N e. NN0 -> (!` N) e. RR)
34	11, 30, 33	syl2an 456	. . . . 5 |- (((K e. NN0 /\ M e. NN) /\ N e. NN0) -> (((2^(K^2)) x. (M^(M + K))) x. (!` N)) e. RR)
35		2re 6067	. . . . . . 7 |- 2 e. RR
36		remulcl 5393	. . . . . . 7 |- ((2 e. RR /\ (((2^(K^2)) x. (M^(M + K))) x. (!` N)) e. RR) -> (2 x. (((2^(K^2)) x. (M^(M + K))) x. (!` N))) e. RR)
37	35, 36	mpan 698	. . . . . 6 |- ((((2^(K^2)) x. (M^(M + K))) x. (!` N)) e. RR -> (2 x. (((2^(K^2)) x. (M^(M + K))) x. (!` N))) e. RR)
38	34, 37	syl 10	. . . . 5 |- (((K e. NN0 /\ M e. NN) /\ N e. NN0) -> (2 x. (((2^(K^2)) x. (M^(M + K))) x. (!` N))) e. RR)
39		faclbnd4 7075	. . . . . . . 8 |- ((N e. NN0 /\ K e. NN0 /\ M e. NN0) -> ((N^K) x. (M^N)) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` N)))
40	39, 23	syl3an3 864	. . . . . . 7 |- ((N e. NN0 /\ K e. NN0 /\ M e. NN) -> ((N^K) x. (M^N)) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` N)))
41	40	3coml 843	. . . . . 6 |- ((K e. NN0 /\ M e. NN /\ N e. NN0) -> ((N^K) x. (M^N)) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` N)))
42	41	3expa 836	. . . . 5 |- (((K e. NN0 /\ M e. NN) /\ N e. NN0) -> ((N^K) x. (M^N)) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` N)))
43		1lt2 6116	. . . . . 6 |- 1 < 2
44		ltmulgt12 5932	. . . . . . . 8 |- (((((2^(K^2)) x. (M^(M + K))) x. (!` N)) e. RR /\ 2 e. RR /\ 0 < (((2^(K^2)) x. (M^(M + K))) x. (!` N))) -> (1 < 2 <-> (((2^(K^2)) x. (M^(M + K))) x. (!` N)) < (2 x. (((2^(K^2)) x. (M^(M + K))) x. (!` N)))))
45	35, 44	mp3an2 907	. . . . . . 7 |- (((((2^(K^2)) x. (M^(M + K))) x. (!` N)) e. RR /\ 0 < (((2^(K^2)) x. (M^(M + K))) x. (!` N))) -> (1 < 2 <-> (((2^(K^2)) x. (M^(M + K))) x. (!` N)) < (2 x. (((2^(K^2)) x. (M^(M + K))) x. (!` N)))))
46		nnmulcl 6028	. . . . . . . . 9 |- ((((2^(K^2)) x. (M^(M + K))) e. NN /\ (!` N) e. NN) -> (((2^(K^2)) x. (M^(M + K))) x. (!` N)) e. NN)
47	46, 28, 31	syl2an 456	. . . . . . . 8 |- (((K e. NN0 /\ M e. NN) /\ N e. NN0) -> (((2^(K^2)) x. (M^(M + K))) x. (!` N)) e. NN)
48		nngt0 6033	. . . . . . . 8 |- ((((2^(K^2)) x. (M^(M + K))) x. (!` N)) e. NN -> 0 < (((2^(K^2)) x. (M^(M + K))) x. (!` N)))
49	47, 48	syl 10	. . . . . . 7 |- (((K e. NN0 /\ M e. NN) /\ N e. NN0) -> 0 < (((2^(K^2)) x. (M^(M + K))) x. (!` N)))
50	45, 34, 49	sylanc 473	. . . . . 6 |- (((K e. NN0 /\ M e. NN) /\ N e. NN0) -> (1 < 2 <-> (((2^(K^2)) x. (M^(M + K))) x. (!` N)) < (2 x. (((2^(K^2)) x. (M^(M + K))) x. (!` N)))))
51	43, 50	mpbii 191	. . . . 5 |- (((K e. NN0 /\ M e. NN) /\ N e. NN0) -> (((2^(K^2)) x. (M^(M + K))) x. (!` N)) < (2 x. (((2^(K^2)) x. (M^(M + K))) x. (