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 ( ( ๐‘ โˆˆ โ„•0 โˆง ๐พ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„• ) โ†’ ( ( ๐‘ โ†‘ ๐พ ) ยท ( ๐‘€ โ†‘ ๐‘ ) ) < ( ( 2 ยท ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ) ยท ( ! โ€˜ ๐‘ ) ) )

Proof

Step Hyp Ref Expression
1 nn0re โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ๐‘ โˆˆ โ„ )
2 reexpcl โŠข ( ( ๐‘ โˆˆ โ„ โˆง ๐พ โˆˆ โ„•0 ) โ†’ ( ๐‘ โ†‘ ๐พ ) โˆˆ โ„ )
3 1 2 sylan โŠข ( ( ๐‘ โˆˆ โ„•0 โˆง ๐พ โˆˆ โ„•0 ) โ†’ ( ๐‘ โ†‘ ๐พ ) โˆˆ โ„ )
4 3 ancoms โŠข ( ( ๐พ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ๐‘ โ†‘ ๐พ ) โˆˆ โ„ )
5 nnre โŠข ( ๐‘€ โˆˆ โ„• โ†’ ๐‘€ โˆˆ โ„ )
6 reexpcl โŠข ( ( ๐‘€ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ๐‘€ โ†‘ ๐‘ ) โˆˆ โ„ )
7 5 6 sylan โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ๐‘€ โ†‘ ๐‘ ) โˆˆ โ„ )
8 remulcl โŠข ( ( ( ๐‘ โ†‘ ๐พ ) โˆˆ โ„ โˆง ( ๐‘€ โ†‘ ๐‘ ) โˆˆ โ„ ) โ†’ ( ( ๐‘ โ†‘ ๐พ ) ยท ( ๐‘€ โ†‘ ๐‘ ) ) โˆˆ โ„ )
9 4 7 8 syl2an โŠข ( ( ( ๐พ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 ) โˆง ( ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•0 ) ) โ†’ ( ( ๐‘ โ†‘ ๐พ ) ยท ( ๐‘€ โ†‘ ๐‘ ) ) โˆˆ โ„ )
10 9 anandirs โŠข ( ( ( ๐พ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„• ) โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ( ๐‘ โ†‘ ๐พ ) ยท ( ๐‘€ โ†‘ ๐‘ ) ) โˆˆ โ„ )
11 2nn โŠข 2 โˆˆ โ„•
12 nn0sqcl โŠข ( ๐พ โˆˆ โ„•0 โ†’ ( ๐พ โ†‘ 2 ) โˆˆ โ„•0 )
13 nnexpcl โŠข ( ( 2 โˆˆ โ„• โˆง ( ๐พ โ†‘ 2 ) โˆˆ โ„•0 ) โ†’ ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) โˆˆ โ„• )
14 11 12 13 sylancr โŠข ( ๐พ โˆˆ โ„•0 โ†’ ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) โˆˆ โ„• )
15 nnnn0 โŠข ( ๐‘€ โˆˆ โ„• โ†’ ๐‘€ โˆˆ โ„•0 )
16 nn0addcl โŠข ( ( ๐‘€ โˆˆ โ„•0 โˆง ๐พ โˆˆ โ„•0 ) โ†’ ( ๐‘€ + ๐พ ) โˆˆ โ„•0 )
17 16 ancoms โŠข ( ( ๐พ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ๐‘€ + ๐พ ) โˆˆ โ„•0 )
18 15 17 sylan2 โŠข ( ( ๐พ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„• ) โ†’ ( ๐‘€ + ๐พ ) โˆˆ โ„•0 )
19 nnexpcl โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ( ๐‘€ + ๐พ ) โˆˆ โ„•0 ) โ†’ ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) โˆˆ โ„• )
20 18 19 sylan2 โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ( ๐พ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„• ) ) โ†’ ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) โˆˆ โ„• )
21 20 anabss7 โŠข ( ( ๐พ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„• ) โ†’ ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) โˆˆ โ„• )
22 nnmulcl โŠข ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) โˆˆ โ„• โˆง ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) โˆˆ โ„• ) โ†’ ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) โˆˆ โ„• )
23 14 21 22 syl2an2r โŠข ( ( ๐พ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„• ) โ†’ ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) โˆˆ โ„• )
24 23 nnred โŠข ( ( ๐พ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„• ) โ†’ ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) โˆˆ โ„ )
25 faccl โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ! โ€˜ ๐‘ ) โˆˆ โ„• )
26 25 nnred โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ! โ€˜ ๐‘ ) โˆˆ โ„ )
27 remulcl โŠข ( ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) โˆˆ โ„ โˆง ( ! โ€˜ ๐‘ ) โˆˆ โ„ ) โ†’ ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) โˆˆ โ„ )
28 24 26 27 syl2an โŠข ( ( ( ๐พ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„• ) โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) โˆˆ โ„ )
29 2re โŠข 2 โˆˆ โ„
30 remulcl โŠข ( ( 2 โˆˆ โ„ โˆง ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) โˆˆ โ„ ) โ†’ ( 2 ยท ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) ) โˆˆ โ„ )
31 29 28 30 sylancr โŠข ( ( ( ๐พ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„• ) โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( 2 ยท ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) ) โˆˆ โ„ )
32 faclbnd4 โŠข ( ( ๐‘ โˆˆ โ„•0 โˆง ๐พ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( ๐‘ โ†‘ ๐พ ) ยท ( ๐‘€ โ†‘ ๐‘ ) ) โ‰ค ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) )
33 15 32 syl3an3 โŠข ( ( ๐‘ โˆˆ โ„•0 โˆง ๐พ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„• ) โ†’ ( ( ๐‘ โ†‘ ๐พ ) ยท ( ๐‘€ โ†‘ ๐‘ ) ) โ‰ค ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) )
34 33 3coml โŠข ( ( ๐พ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ( ๐‘ โ†‘ ๐พ ) ยท ( ๐‘€ โ†‘ ๐‘ ) ) โ‰ค ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) )
35 34 3expa โŠข ( ( ( ๐พ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„• ) โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ( ๐‘ โ†‘ ๐พ ) ยท ( ๐‘€ โ†‘ ๐‘ ) ) โ‰ค ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) )
36 1lt2 โŠข 1 < 2
37 nnmulcl โŠข ( ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) โˆˆ โ„• โˆง ( ! โ€˜ ๐‘ ) โˆˆ โ„• ) โ†’ ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) โˆˆ โ„• )
38 23 25 37 syl2an โŠข ( ( ( ๐พ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„• ) โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) โˆˆ โ„• )
39 38 nngt0d โŠข ( ( ( ๐พ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„• ) โˆง ๐‘ โˆˆ โ„•0 ) โ†’ 0 < ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) )
40 ltmulgt12 โŠข ( ( ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) โˆˆ โ„ โˆง 2 โˆˆ โ„ โˆง 0 < ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) ) โ†’ ( 1 < 2 โ†” ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) < ( 2 ยท ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) ) ) )
41 29 40 mp3an2 โŠข ( ( ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) โˆˆ โ„ โˆง 0 < ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) ) โ†’ ( 1 < 2 โ†” ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) < ( 2 ยท ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) ) ) )
42 28 39 41 syl2anc โŠข ( ( ( ๐พ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„• ) โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( 1 < 2 โ†” ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) < ( 2 ยท ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) ) ) )
43 36 42 mpbii โŠข ( ( ( ๐พ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„• ) โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) < ( 2 ยท ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) ) )
44 10 28 31 35 43 lelttrd โŠข ( ( ( ๐พ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„• ) โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ( ๐‘ โ†‘ ๐พ ) ยท ( ๐‘€ โ†‘ ๐‘ ) ) < ( 2 ยท ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) ) )
45 2cn โŠข 2 โˆˆ โ„‚
46 23 nncnd โŠข ( ( ๐พ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„• ) โ†’ ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) โˆˆ โ„‚ )
47 25 nncnd โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ! โ€˜ ๐‘ ) โˆˆ โ„‚ )
48 mulass โŠข ( ( 2 โˆˆ โ„‚ โˆง ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) โˆˆ โ„‚ โˆง ( ! โ€˜ ๐‘ ) โˆˆ โ„‚ ) โ†’ ( ( 2 ยท ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ) ยท ( ! โ€˜ ๐‘ ) ) = ( 2 ยท ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) ) )
49 45 46 47 48 mp3an3an โŠข ( ( ( ๐พ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„• ) โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ( 2 ยท ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ) ยท ( ! โ€˜ ๐‘ ) ) = ( 2 ยท ( ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ยท ( ! โ€˜ ๐‘ ) ) ) )
50 44 49 breqtrrd โŠข ( ( ( ๐พ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„• ) โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ( ๐‘ โ†‘ ๐พ ) ยท ( ๐‘€ โ†‘ ๐‘ ) ) < ( ( 2 ยท ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ) ยท ( ! โ€˜ ๐‘ ) ) )
51 50 3impa โŠข ( ( ๐พ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ( ๐‘ โ†‘ ๐พ ) ยท ( ๐‘€ โ†‘ ๐‘ ) ) < ( ( 2 ยท ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ) ยท ( ! โ€˜ ๐‘ ) ) )
52 51 3comr โŠข ( ( ๐‘ โˆˆ โ„•0 โˆง ๐พ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„• ) โ†’ ( ( ๐‘ โ†‘ ๐พ ) ยท ( ๐‘€ โ†‘ ๐‘ ) ) < ( ( 2 ยท ( ( 2 โ†‘ ( ๐พ โ†‘ 2 ) ) ยท ( ๐‘€ โ†‘ ( ๐‘€ + ๐พ ) ) ) ) ยท ( ! โ€˜ ๐‘ ) ) )