Metamath Proof Explorer

Theorem faclbnd3

Description: A lower bound for the factorial function. (Contributed by NM, 19-Dec-2005)

Ref Expression
Assertion faclbnd3 
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( M ^ N ) <_ ( ( M ^ M ) x. ( ! ` N ) ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( M e. NN0 <-> ( M e. NN \/ M = 0 ) )
2 nnre 
 |-  ( M e. NN -> M e. RR )
3 2 adantr 
 |-  ( ( M e. NN /\ N e. NN0 ) -> M e. RR )
4 nnge1 
 |-  ( M e. NN -> 1 <_ M )
5 4 adantr 
 |-  ( ( M e. NN /\ N e. NN0 ) -> 1 <_ M )
6 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
7 6 adantl 
 |-  ( ( M e. NN /\ N e. NN0 ) -> N e. ZZ )
8 uzid 
 |-  ( N e. ZZ -> N e. ( ZZ>= ` N ) )
9 peano2uz 
 |-  ( N e. ( ZZ>= ` N ) -> ( N + 1 ) e. ( ZZ>= ` N ) )
10 7 8 9 3syl 
 |-  ( ( M e. NN /\ N e. NN0 ) -> ( N + 1 ) e. ( ZZ>= ` N ) )
11 3 5 10 leexp2ad 
 |-  ( ( M e. NN /\ N e. NN0 ) -> ( M ^ N ) <_ ( M ^ ( N + 1 ) ) )
12 nnnn0 
 |-  ( M e. NN -> M e. NN0 )
13 faclbnd 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M ^ ( N + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` N ) ) )
14 12 13 sylan 
 |-  ( ( M e. NN /\ N e. NN0 ) -> ( M ^ ( N + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` N ) ) )
15 nn0re 
 |-  ( M e. NN0 -> M e. RR )
16 reexpcl 
 |-  ( ( M e. RR /\ N e. NN0 ) -> ( M ^ N ) e. RR )
17 15 16 sylan 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M ^ N ) e. RR )
18 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
19 reexpcl 
 |-  ( ( M e. RR /\ ( N + 1 ) e. NN0 ) -> ( M ^ ( N + 1 ) ) e. RR )
20 15 18 19 syl2an 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M ^ ( N + 1 ) ) e. RR )
21 reexpcl 
 |-  ( ( M e. RR /\ M e. NN0 ) -> ( M ^ M ) e. RR )
22 15 21 mpancom 
 |-  ( M e. NN0 -> ( M ^ M ) e. RR )
23 faccl 
 |-  ( N e. NN0 -> ( ! ` N ) e. NN )
24 23 nnred 
 |-  ( N e. NN0 -> ( ! ` N ) e. RR )
25 remulcl 
 |-  ( ( ( M ^ M ) e. RR /\ ( ! ` N ) e. RR ) -> ( ( M ^ M ) x. ( ! ` N ) ) e. RR )
26 22 24 25 syl2an 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( M ^ M ) x. ( ! ` N ) ) e. RR )
27 letr 
 |-  ( ( ( M ^ N ) e. RR /\ ( M ^ ( N + 1 ) ) e. RR /\ ( ( M ^ M ) x. ( ! ` N ) ) e. RR ) -> ( ( ( M ^ N ) <_ ( M ^ ( N + 1 ) ) /\ ( M ^ ( N + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` N ) ) ) -> ( M ^ N ) <_ ( ( M ^ M ) x. ( ! ` N ) ) ) )
28 17 20 26 27 syl3anc 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( ( M ^ N ) <_ ( M ^ ( N + 1 ) ) /\ ( M ^ ( N + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` N ) ) ) -> ( M ^ N ) <_ ( ( M ^ M ) x. ( ! ` N ) ) ) )
29 12 28 sylan 
 |-  ( ( M e. NN /\ N e. NN0 ) -> ( ( ( M ^ N ) <_ ( M ^ ( N + 1 ) ) /\ ( M ^ ( N + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` N ) ) ) -> ( M ^ N ) <_ ( ( M ^ M ) x. ( ! ` N ) ) ) )
30 11 14 29 mp2and 
 |-  ( ( M e. NN /\ N e. NN0 ) -> ( M ^ N ) <_ ( ( M ^ M ) x. ( ! ` N ) ) )
31 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
32 0exp 
 |-  ( N e. NN -> ( 0 ^ N ) = 0 )
33 0le1 
 |-  0 <_ 1
34 32 33 eqbrtrdi 
 |-  ( N e. NN -> ( 0 ^ N ) <_ 1 )
35 oveq2 
 |-  ( N = 0 -> ( 0 ^ N ) = ( 0 ^ 0 ) )
36 0exp0e1 
 |-  ( 0 ^ 0 ) = 1
37 1le1 
 |-  1 <_ 1
38 36 37 eqbrtri 
 |-  ( 0 ^ 0 ) <_ 1
39 35 38 eqbrtrdi 
 |-  ( N = 0 -> ( 0 ^ N ) <_ 1 )
40 34 39 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> ( 0 ^ N ) <_ 1 )
41 31 40 sylbi 
 |-  ( N e. NN0 -> ( 0 ^ N ) <_ 1 )
42 1nn 
 |-  1 e. NN
43 nnmulcl 
 |-  ( ( 1 e. NN /\ ( ! ` N ) e. NN ) -> ( 1 x. ( ! ` N ) ) e. NN )
44 42 23 43 sylancr 
 |-  ( N e. NN0 -> ( 1 x. ( ! ` N ) ) e. NN )
45 44 nnge1d 
 |-  ( N e. NN0 -> 1 <_ ( 1 x. ( ! ` N ) ) )
46 0re 
 |-  0 e. RR
47 reexpcl 
 |-  ( ( 0 e. RR /\ N e. NN0 ) -> ( 0 ^ N ) e. RR )
48 46 47 mpan 
 |-  ( N e. NN0 -> ( 0 ^ N ) e. RR )
49 1re 
 |-  1 e. RR
50 remulcl 
 |-  ( ( 1 e. RR /\ ( ! ` N ) e. RR ) -> ( 1 x. ( ! ` N ) ) e. RR )
51 49 24 50 sylancr 
 |-  ( N e. NN0 -> ( 1 x. ( ! ` N ) ) e. RR )
52 letr 
 |-  ( ( ( 0 ^ N ) e. RR /\ 1 e. RR /\ ( 1 x. ( ! ` N ) ) e. RR ) -> ( ( ( 0 ^ N ) <_ 1 /\ 1 <_ ( 1 x. ( ! ` N ) ) ) -> ( 0 ^ N ) <_ ( 1 x. ( ! ` N ) ) ) )
53 49 52 mp3an2 
 |-  ( ( ( 0 ^ N ) e. RR /\ ( 1 x. ( ! ` N ) ) e. RR ) -> ( ( ( 0 ^ N ) <_ 1 /\ 1 <_ ( 1 x. ( ! ` N ) ) ) -> ( 0 ^ N ) <_ ( 1 x. ( ! ` N ) ) ) )
54 48 51 53 syl2anc 
 |-  ( N e. NN0 -> ( ( ( 0 ^ N ) <_ 1 /\ 1 <_ ( 1 x. ( ! ` N ) ) ) -> ( 0 ^ N ) <_ ( 1 x. ( ! ` N ) ) ) )
55 41 45 54 mp2and 
 |-  ( N e. NN0 -> ( 0 ^ N ) <_ ( 1 x. ( ! ` N ) ) )
56 55 adantl 
 |-  ( ( M = 0 /\ N e. NN0 ) -> ( 0 ^ N ) <_ ( 1 x. ( ! ` N ) ) )
57 oveq1 
 |-  ( M = 0 -> ( M ^ N ) = ( 0 ^ N ) )
58 oveq12 
 |-  ( ( M = 0 /\ M = 0 ) -> ( M ^ M ) = ( 0 ^ 0 ) )
59 58 anidms 
 |-  ( M = 0 -> ( M ^ M ) = ( 0 ^ 0 ) )
60 59 36 eqtrdi 
 |-  ( M = 0 -> ( M ^ M ) = 1 )
61 60 oveq1d 
 |-  ( M = 0 -> ( ( M ^ M ) x. ( ! ` N ) ) = ( 1 x. ( ! ` N ) ) )
62 57 61 breq12d 
 |-  ( M = 0 -> ( ( M ^ N ) <_ ( ( M ^ M ) x. ( ! ` N ) ) <-> ( 0 ^ N ) <_ ( 1 x. ( ! ` N ) ) ) )
63 62 adantr 
 |-  ( ( M = 0 /\ N e. NN0 ) -> ( ( M ^ N ) <_ ( ( M ^ M ) x. ( ! ` N ) ) <-> ( 0 ^ N ) <_ ( 1 x. ( ! ` N ) ) ) )
64 56 63 mpbird 
 |-  ( ( M = 0 /\ N e. NN0 ) -> ( M ^ N ) <_ ( ( M ^ M ) x. ( ! ` N ) ) )
65 30 64 jaoian 
 |-  ( ( ( M e. NN \/ M = 0 ) /\ N e. NN0 ) -> ( M ^ N ) <_ ( ( M ^ M ) x. ( ! ` N ) ) )
66 1 65 sylanb 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M ^ N ) <_ ( ( M ^ M ) x. ( ! ` N ) ) )