Metamath Proof Explorer

Theorem 2expltfac

Description: The factorial grows faster than two to the power N . (Contributed by Mario Carneiro, 15-Sep-2016)

Ref Expression
Assertion 2expltfac 
|- ( N e. ( ZZ>= ` 4 ) -> ( 2 ^ N ) < ( ! ` N ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = 4 -> ( 2 ^ x ) = ( 2 ^ 4 ) )
2 2exp4 
 |-  ( 2 ^ 4 ) = ; 1 6
3 1 2 eqtrdi 
 |-  ( x = 4 -> ( 2 ^ x ) = ; 1 6 )
4 fveq2 
 |-  ( x = 4 -> ( ! ` x ) = ( ! ` 4 ) )
5 fac4 
 |-  ( ! ` 4 ) = ; 2 4
6 4 5 eqtrdi 
 |-  ( x = 4 -> ( ! ` x ) = ; 2 4 )
7 3 6 breq12d 
 |-  ( x = 4 -> ( ( 2 ^ x ) < ( ! ` x ) <-> ; 1 6 < ; 2 4 ) )
8 oveq2 
 |-  ( x = n -> ( 2 ^ x ) = ( 2 ^ n ) )
9 fveq2 
 |-  ( x = n -> ( ! ` x ) = ( ! ` n ) )
10 8 9 breq12d 
 |-  ( x = n -> ( ( 2 ^ x ) < ( ! ` x ) <-> ( 2 ^ n ) < ( ! ` n ) ) )
11 oveq2 
 |-  ( x = ( n + 1 ) -> ( 2 ^ x ) = ( 2 ^ ( n + 1 ) ) )
12 fveq2 
 |-  ( x = ( n + 1 ) -> ( ! ` x ) = ( ! ` ( n + 1 ) ) )
13 11 12 breq12d 
 |-  ( x = ( n + 1 ) -> ( ( 2 ^ x ) < ( ! ` x ) <-> ( 2 ^ ( n + 1 ) ) < ( ! ` ( n + 1 ) ) ) )
14 oveq2 
 |-  ( x = N -> ( 2 ^ x ) = ( 2 ^ N ) )
15 fveq2 
 |-  ( x = N -> ( ! ` x ) = ( ! ` N ) )
16 14 15 breq12d 
 |-  ( x = N -> ( ( 2 ^ x ) < ( ! ` x ) <-> ( 2 ^ N ) < ( ! ` N ) ) )
17 1nn0 
 |-  1 e. NN0
18 2nn0 
 |-  2 e. NN0
19 6nn0 
 |-  6 e. NN0
20 4nn0 
 |-  4 e. NN0
21 6lt10 
 |-  6 < ; 1 0
22 1lt2 
 |-  1 < 2
23 17 18 19 20 21 22 decltc 
 |-  ; 1 6 < ; 2 4
24 2nn 
 |-  2 e. NN
25 24 a1i 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> 2 e. NN )
26 4nn 
 |-  4 e. NN
27 simpl 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> n e. ( ZZ>= ` 4 ) )
28 eluznn 
 |-  ( ( 4 e. NN /\ n e. ( ZZ>= ` 4 ) ) -> n e. NN )
29 26 27 28 sylancr 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> n e. NN )
30 29 nnnn0d 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> n e. NN0 )
31 25 30 nnexpcld 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> ( 2 ^ n ) e. NN )
32 31 nnred 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> ( 2 ^ n ) e. RR )
33 2re 
 |-  2 e. RR
34 33 a1i 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> 2 e. RR )
35 32 34 remulcld 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> ( ( 2 ^ n ) x. 2 ) e. RR )
36 30 faccld 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> ( ! ` n ) e. NN )
37 36 nnred 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> ( ! ` n ) e. RR )
38 37 34 remulcld 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> ( ( ! ` n ) x. 2 ) e. RR )
39 29 nnred 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> n e. RR )
40 1red 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> 1 e. RR )
41 39 40 readdcld 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> ( n + 1 ) e. RR )
42 37 41 remulcld 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> ( ( ! ` n ) x. ( n + 1 ) ) e. RR )
43 2rp 
 |-  2 e. RR+
44 43 a1i 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> 2 e. RR+ )
45 simpr 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> ( 2 ^ n ) < ( ! ` n ) )
46 32 37 44 45 ltmul1dd 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> ( ( 2 ^ n ) x. 2 ) < ( ( ! ` n ) x. 2 ) )
47 36 nnnn0d 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> ( ! ` n ) e. NN0 )
48 47 nn0ge0d 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> 0 <_ ( ! ` n ) )
49 df-2 
 |-  2 = ( 1 + 1 )
50 29 nnge1d 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> 1 <_ n )
51 40 39 40 50 leadd1dd 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> ( 1 + 1 ) <_ ( n + 1 ) )
52 49 51 eqbrtrid 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> 2 <_ ( n + 1 ) )
53 34 41 37 48 52 lemul2ad 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> ( ( ! ` n ) x. 2 ) <_ ( ( ! ` n ) x. ( n + 1 ) ) )
54 35 38 42 46 53 ltletrd 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> ( ( 2 ^ n ) x. 2 ) < ( ( ! ` n ) x. ( n + 1 ) ) )
55 2cnd 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> 2 e. CC )
56 55 30 expp1d 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> ( 2 ^ ( n + 1 ) ) = ( ( 2 ^ n ) x. 2 ) )
57 facp1 
 |-  ( n e. NN0 -> ( ! ` ( n + 1 ) ) = ( ( ! ` n ) x. ( n + 1 ) ) )
58 30 57 syl 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> ( ! ` ( n + 1 ) ) = ( ( ! ` n ) x. ( n + 1 ) ) )
59 54 56 58 3brtr4d 
 |-  ( ( n e. ( ZZ>= ` 4 ) /\ ( 2 ^ n ) < ( ! ` n ) ) -> ( 2 ^ ( n + 1 ) ) < ( ! ` ( n + 1 ) ) )
60 59 ex 
 |-  ( n e. ( ZZ>= ` 4 ) -> ( ( 2 ^ n ) < ( ! ` n ) -> ( 2 ^ ( n + 1 ) ) < ( ! ` ( n + 1 ) ) ) )
61 7 10 13 16 23 60 uzind4i 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( 2 ^ N ) < ( ! ` N ) )