Theorem faclbnd5 6953

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		axmulrcl 5274	. . . . . . 7 |- (((N^K) e. RR /\ (M^N) e. RR) -> ((N^K) x. (M^N)) e. RR)
2		reexpclt 6580	. . . . . . . . 9 |- ((N e. RR /\ K e. NN0) -> (N^K) e. RR)
3		nn0ret 6108	. . . . . . . . 9 |- (N e. NN0 -> N e. RR)
4	2, 3	sylan 448	. . . . . . . 8 |- ((N e. NN0 /\ K e. NN0) -> (N^K) e. RR)
5	4	ancoms 436	. . . . . . 7 |- ((K e. NN0 /\ N e. NN0) -> (N^K) e. RR)
6		reexpclt 6580	. . . . . . . 8 |- ((M e. RR /\ N e. NN0) -> (M^N) e. RR)
7		nnret 5929	. . . . . . . 8 |- (M e. NN -> M e. RR)
8	6, 7	sylan 448	. . . . . . 7 |- ((M e. NN /\ N e. NN0) -> (M^N) e. RR)
9	1, 5, 8	syl2an 454	. . . . . 6 |- (((K e. NN0 /\ N e. NN0) /\ (M e. NN /\ N e. NN0)) -> ((N^K) x. (M^N)) e. RR)
10	9	anandirs 513	. . . . 5 |- (((K e. NN0 /\ M e. NN) /\ N e. NN0) -> ((N^K) x. (M^N)) e. RR)
11		axmulrcl 5274	. . . . . 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		nnmulclt 5941	. . . . . . . . 9 |- (((2^(K^2)) e. NN /\ (M^(M + K)) e. NN) -> ((2^(K^2)) x. (M^(M + K))) e. NN)
13		2nn0 6115	. . . . . . . . . . 11 |- 2 e. NN0
14		nn0expclt 6577	. . . . . . . . . . 11 |- ((K e. NN0 /\ 2 e. NN0) -> (K^2) e. NN0)
15	13, 14	mpan2 696	. . . . . . . . . 10 |- (K e. NN0 -> (K^2) e. NN0)
16		2nn 5999	. . . . . . . . . . 11 |- 2 e. NN
17		nnexpclt 6576	. . . . . . . . . . 11 |- ((2 e. NN /\ (K^2) e. NN0) -> (2^(K^2)) e. NN)
18	16, 17	mpan 695	. . . . . . . . . 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		nnexpclt 6576	. . . . . . . . . . 11 |- ((M e. NN /\ (M + K) e. NN0) -> (M^(M + K)) e. NN)
21		nn0addclt 6120	. . . . . . . . . . . . 13 |- ((M e. NN0 /\ K e. NN0) -> (M + K) e. NN0)
22	21	ancoms 436	. . . . . . . . . . . 12 |- ((K e. NN0 /\ M e. NN0) -> (M + K) e. NN0)
23		nnnn0t 6106	. . . . . . . . . . . 12 |- (M e. NN -> M e. NN0)
24	22, 23	sylan2 451	. . . . . . . . . . 11 |- ((K e. NN0 /\ M e. NN) -> (M + K) e. NN0)
25	20, 24	sylan2 451	. . . . . . . . . 10 |- ((M e. NN /\ (K e. NN0 /\ M e. NN)) -> (M^(M + K)) e. NN)
26	25	anabss7 503	. . . . . . . . 9 |- ((K e. NN0 /\ M e. NN) -> (M^(M + K)) e. NN)
27	12, 19, 26	syl2an 454	. . . . . . . 8 |- ((K e. NN0 /\ (K e. NN0 /\ M e. NN)) -> ((2^(K^2)) x. (M^(M + K))) e. NN)
28	27	anabss5 502	. . . . . . 7 |- ((K e. NN0 /\ M e. NN) -> ((2^(K^2)) x. (M^(M + K))) e. NN)
29		nnret 5929	. . . . . . 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		facclt 6940	. . . . . . 7 |- (N e. NN0 -> (!` N) e. NN)
32		nnret 5929	. . . . . . 7 |- ((!` N) e. NN -> (!` N) e. RR)
33	31, 32	syl 10	. . . . . 6 |- (N e. NN0 -> (!` N) e. RR)
34	11, 30, 33	syl2an 454	. . . . 5 |- (((K e. NN0 /\ M e. NN) /\ N e. NN0) -> (((2^(K^2)) x. (M^(M + K))) x. (!` N)) e. RR)
35		2re 5979	. . . . . . 7 |- 2 e. RR
36		axmulrcl 5274	. . . . . . 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 695	. . . . . 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 6952	. . . . . . . 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 861	. . . . . . 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 840	. . . . . 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 833	. . . . 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 6028	. . . . . 6 |- 1 < 2
44		ltmulgt12t 5847	. . . . . . . 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 904	. . . . . . 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		nnmulclt 5941	. . . . . . . . 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 454	. . . . . . . 8 |- (((K e. NN0 /\ M e. NN) /\ N e. NN0) -> (((2^(K^2)) x. (M^(M + K))) x. (!` N)) e. NN)
48		nngt0t 5946	. . . . . . . 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 471	. . . . . 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 193	. . . . 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)))