Metamath Proof Explorer

Theorem 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 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

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