Metamath Proof Explorer

Theorem faclbnd2

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

Ref Expression
Assertion faclbnd2 
|- ( N e. NN0 -> ( ( 2 ^ N ) / 2 ) <_ ( ! ` N ) )

Proof

Step Hyp Ref Expression
1 sq2 
 |-  ( 2 ^ 2 ) = 4
2 2t2e4 
 |-  ( 2 x. 2 ) = 4
3 1 2 eqtr4i 
 |-  ( 2 ^ 2 ) = ( 2 x. 2 )
4 3 oveq2i 
 |-  ( ( 2 ^ ( N + 1 ) ) / ( 2 ^ 2 ) ) = ( ( 2 ^ ( N + 1 ) ) / ( 2 x. 2 ) )
5 2cn 
 |-  2 e. CC
6 expp1 
 |-  ( ( 2 e. CC /\ N e. NN0 ) -> ( 2 ^ ( N + 1 ) ) = ( ( 2 ^ N ) x. 2 ) )
7 5 6 mpan 
 |-  ( N e. NN0 -> ( 2 ^ ( N + 1 ) ) = ( ( 2 ^ N ) x. 2 ) )
8 7 oveq1d 
 |-  ( N e. NN0 -> ( ( 2 ^ ( N + 1 ) ) / ( 2 x. 2 ) ) = ( ( ( 2 ^ N ) x. 2 ) / ( 2 x. 2 ) ) )
9 4 8 syl5eq 
 |-  ( N e. NN0 -> ( ( 2 ^ ( N + 1 ) ) / ( 2 ^ 2 ) ) = ( ( ( 2 ^ N ) x. 2 ) / ( 2 x. 2 ) ) )
10 expcl 
 |-  ( ( 2 e. CC /\ N e. NN0 ) -> ( 2 ^ N ) e. CC )
11 5 10 mpan 
 |-  ( N e. NN0 -> ( 2 ^ N ) e. CC )
12 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
13 divmuldiv 
 |-  ( ( ( ( 2 ^ N ) e. CC /\ 2 e. CC ) /\ ( ( 2 e. CC /\ 2 =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) ) -> ( ( ( 2 ^ N ) / 2 ) x. ( 2 / 2 ) ) = ( ( ( 2 ^ N ) x. 2 ) / ( 2 x. 2 ) ) )
14 12 12 13 mpanr12 
 |-  ( ( ( 2 ^ N ) e. CC /\ 2 e. CC ) -> ( ( ( 2 ^ N ) / 2 ) x. ( 2 / 2 ) ) = ( ( ( 2 ^ N ) x. 2 ) / ( 2 x. 2 ) ) )
15 11 5 14 sylancl 
 |-  ( N e. NN0 -> ( ( ( 2 ^ N ) / 2 ) x. ( 2 / 2 ) ) = ( ( ( 2 ^ N ) x. 2 ) / ( 2 x. 2 ) ) )
16 2div2e1 
 |-  ( 2 / 2 ) = 1
17 16 oveq2i 
 |-  ( ( ( 2 ^ N ) / 2 ) x. ( 2 / 2 ) ) = ( ( ( 2 ^ N ) / 2 ) x. 1 )
18 11 halfcld 
 |-  ( N e. NN0 -> ( ( 2 ^ N ) / 2 ) e. CC )
19 18 mulid1d 
 |-  ( N e. NN0 -> ( ( ( 2 ^ N ) / 2 ) x. 1 ) = ( ( 2 ^ N ) / 2 ) )
20 17 19 syl5eq 
 |-  ( N e. NN0 -> ( ( ( 2 ^ N ) / 2 ) x. ( 2 / 2 ) ) = ( ( 2 ^ N ) / 2 ) )
21 9 15 20 3eqtr2rd 
 |-  ( N e. NN0 -> ( ( 2 ^ N ) / 2 ) = ( ( 2 ^ ( N + 1 ) ) / ( 2 ^ 2 ) ) )
22 2nn0 
 |-  2 e. NN0
23 faclbnd 
 |-  ( ( 2 e. NN0 /\ N e. NN0 ) -> ( 2 ^ ( N + 1 ) ) <_ ( ( 2 ^ 2 ) x. ( ! ` N ) ) )
24 22 23 mpan 
 |-  ( N e. NN0 -> ( 2 ^ ( N + 1 ) ) <_ ( ( 2 ^ 2 ) x. ( ! ` N ) ) )
25 2re 
 |-  2 e. RR
26 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
27 reexpcl 
 |-  ( ( 2 e. RR /\ ( N + 1 ) e. NN0 ) -> ( 2 ^ ( N + 1 ) ) e. RR )
28 25 26 27 sylancr 
 |-  ( N e. NN0 -> ( 2 ^ ( N + 1 ) ) e. RR )
29 faccl 
 |-  ( N e. NN0 -> ( ! ` N ) e. NN )
30 29 nnred 
 |-  ( N e. NN0 -> ( ! ` N ) e. RR )
31 4re 
 |-  4 e. RR
32 1 31 eqeltri 
 |-  ( 2 ^ 2 ) e. RR
33 4pos 
 |-  0 < 4
34 33 1 breqtrri 
 |-  0 < ( 2 ^ 2 )
35 32 34 pm3.2i 
 |-  ( ( 2 ^ 2 ) e. RR /\ 0 < ( 2 ^ 2 ) )
36 ledivmul 
 |-  ( ( ( 2 ^ ( N + 1 ) ) e. RR /\ ( ! ` N ) e. RR /\ ( ( 2 ^ 2 ) e. RR /\ 0 < ( 2 ^ 2 ) ) ) -> ( ( ( 2 ^ ( N + 1 ) ) / ( 2 ^ 2 ) ) <_ ( ! ` N ) <-> ( 2 ^ ( N + 1 ) ) <_ ( ( 2 ^ 2 ) x. ( ! ` N ) ) ) )
37 35 36 mp3an3 
 |-  ( ( ( 2 ^ ( N + 1 ) ) e. RR /\ ( ! ` N ) e. RR ) -> ( ( ( 2 ^ ( N + 1 ) ) / ( 2 ^ 2 ) ) <_ ( ! ` N ) <-> ( 2 ^ ( N + 1 ) ) <_ ( ( 2 ^ 2 ) x. ( ! ` N ) ) ) )
38 28 30 37 syl2anc 
 |-  ( N e. NN0 -> ( ( ( 2 ^ ( N + 1 ) ) / ( 2 ^ 2 ) ) <_ ( ! ` N ) <-> ( 2 ^ ( N + 1 ) ) <_ ( ( 2 ^ 2 ) x. ( ! ` N ) ) ) )
39 24 38 mpbird 
 |-  ( N e. NN0 -> ( ( 2 ^ ( N + 1 ) ) / ( 2 ^ 2 ) ) <_ ( ! ` N ) )
40 21 39 eqbrtrd 
 |-  ( N e. NN0 -> ( ( 2 ^ N ) / 2 ) <_ ( ! ` N ) )