Metamath Proof Explorer

Theorem cxploglim

Description: The logarithm grows slower than any positive power. (Contributed by Mario Carneiro, 18-Sep-2014)

Ref Expression
Assertion cxploglim 
|- ( A e. RR+ -> ( n e. RR+ |-> ( ( log ` n ) / ( n ^c A ) ) ) ~~>r 0 )

Proof

Step Hyp Ref Expression
1 rpre 
 |-  ( A e. RR+ -> A e. RR )
2 reefcl 
 |-  ( A e. RR -> ( exp ` A ) e. RR )
3 1 2 syl 
 |-  ( A e. RR+ -> ( exp ` A ) e. RR )
4 efgt1 
 |-  ( A e. RR+ -> 1 < ( exp ` A ) )
5 cxp2limlem 
 |-  ( ( ( exp ` A ) e. RR /\ 1 < ( exp ` A ) ) -> ( m e. RR+ |-> ( m / ( ( exp ` A ) ^c m ) ) ) ~~>r 0 )
6 3 4 5 syl2anc 
 |-  ( A e. RR+ -> ( m e. RR+ |-> ( m / ( ( exp ` A ) ^c m ) ) ) ~~>r 0 )
7 reefcl 
 |-  ( z e. RR -> ( exp ` z ) e. RR )
8 7 adantl 
 |-  ( ( A e. RR+ /\ z e. RR ) -> ( exp ` z ) e. RR )
9 1re 
 |-  1 e. RR
10 ifcl 
 |-  ( ( ( exp ` z ) e. RR /\ 1 e. RR ) -> if ( 1 <_ ( exp ` z ) , ( exp ` z ) , 1 ) e. RR )
11 8 9 10 sylancl 
 |-  ( ( A e. RR+ /\ z e. RR ) -> if ( 1 <_ ( exp ` z ) , ( exp ` z ) , 1 ) e. RR )
12 rpre 
 |-  ( n e. RR+ -> n e. RR )
13 maxlt 
 |-  ( ( 1 e. RR /\ ( exp ` z ) e. RR /\ n e. RR ) -> ( if ( 1 <_ ( exp ` z ) , ( exp ` z ) , 1 ) < n <-> ( 1 < n /\ ( exp ` z ) < n ) ) )
14 9 8 12 13 mp3an3an 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ n e. RR+ ) -> ( if ( 1 <_ ( exp ` z ) , ( exp ` z ) , 1 ) < n <-> ( 1 < n /\ ( exp ` z ) < n ) ) )
15 simprrr 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> ( exp ` z ) < n )
16 reeflog 
 |-  ( n e. RR+ -> ( exp ` ( log ` n ) ) = n )
17 16 ad2antrl 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> ( exp ` ( log ` n ) ) = n )
18 15 17 breqtrrd 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> ( exp ` z ) < ( exp ` ( log ` n ) ) )
19 simplr 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> z e. RR )
20 12 ad2antrl 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> n e. RR )
21 simprrl 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> 1 < n )
22 20 21 rplogcld 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> ( log ` n ) e. RR+ )
23 22 rpred 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> ( log ` n ) e. RR )
24 eflt 
 |-  ( ( z e. RR /\ ( log ` n ) e. RR ) -> ( z < ( log ` n ) <-> ( exp ` z ) < ( exp ` ( log ` n ) ) ) )
25 19 23 24 syl2anc 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> ( z < ( log ` n ) <-> ( exp ` z ) < ( exp ` ( log ` n ) ) ) )
26 18 25 mpbird 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> z < ( log ` n ) )
27 breq2 
 |-  ( m = ( log ` n ) -> ( z < m <-> z < ( log ` n ) ) )
28 id 
 |-  ( m = ( log ` n ) -> m = ( log ` n ) )
29 oveq2 
 |-  ( m = ( log ` n ) -> ( ( exp ` A ) ^c m ) = ( ( exp ` A ) ^c ( log ` n ) ) )
30 28 29 oveq12d 
 |-  ( m = ( log ` n ) -> ( m / ( ( exp ` A ) ^c m ) ) = ( ( log ` n ) / ( ( exp ` A ) ^c ( log ` n ) ) ) )
31 30 fveq2d 
 |-  ( m = ( log ` n ) -> ( abs ` ( m / ( ( exp ` A ) ^c m ) ) ) = ( abs ` ( ( log ` n ) / ( ( exp ` A ) ^c ( log ` n ) ) ) ) )
32 31 breq1d 
 |-  ( m = ( log ` n ) -> ( ( abs ` ( m / ( ( exp ` A ) ^c m ) ) ) < x <-> ( abs ` ( ( log ` n ) / ( ( exp ` A ) ^c ( log ` n ) ) ) ) < x ) )
33 27 32 imbi12d 
 |-  ( m = ( log ` n ) -> ( ( z < m -> ( abs ` ( m / ( ( exp ` A ) ^c m ) ) ) < x ) <-> ( z < ( log ` n ) -> ( abs ` ( ( log ` n ) / ( ( exp ` A ) ^c ( log ` n ) ) ) ) < x ) ) )
34 33 rspcv 
 |-  ( ( log ` n ) e. RR+ -> ( A. m e. RR+ ( z < m -> ( abs ` ( m / ( ( exp ` A ) ^c m ) ) ) < x ) -> ( z < ( log ` n ) -> ( abs ` ( ( log ` n ) / ( ( exp ` A ) ^c ( log ` n ) ) ) ) < x ) ) )
35 22 34 syl 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> ( A. m e. RR+ ( z < m -> ( abs ` ( m / ( ( exp ` A ) ^c m ) ) ) < x ) -> ( z < ( log ` n ) -> ( abs ` ( ( log ` n ) / ( ( exp ` A ) ^c ( log ` n ) ) ) ) < x ) ) )
36 26 35 mpid 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> ( A. m e. RR+ ( z < m -> ( abs ` ( m / ( ( exp ` A ) ^c m ) ) ) < x ) -> ( abs ` ( ( log ` n ) / ( ( exp ` A ) ^c ( log ` n ) ) ) ) < x ) )
37 1 ad2antrr 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> A e. RR )
38 37 relogefd 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> ( log ` ( exp ` A ) ) = A )
39 38 oveq2d 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> ( ( log ` n ) x. ( log ` ( exp ` A ) ) ) = ( ( log ` n ) x. A ) )
40 22 rpcnd 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> ( log ` n ) e. CC )
41 rpcn 
 |-  ( A e. RR+ -> A e. CC )
42 41 ad2antrr 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> A e. CC )
43 40 42 mulcomd 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> ( ( log ` n ) x. A ) = ( A x. ( log ` n ) ) )
44 39 43 eqtrd 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> ( ( log ` n ) x. ( log ` ( exp ` A ) ) ) = ( A x. ( log ` n ) ) )
45 44 fveq2d 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> ( exp ` ( ( log ` n ) x. ( log ` ( exp ` A ) ) ) ) = ( exp ` ( A x. ( log ` n ) ) ) )
46 3 ad2antrr 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> ( exp ` A ) e. RR )
47 46 recnd 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> ( exp ` A ) e. CC )
48 efne0 
 |-  ( A e. CC -> ( exp ` A ) =/= 0 )
49 42 48 syl 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> ( exp ` A ) =/= 0 )
50 47 49 40 cxpefd 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> ( ( exp ` A ) ^c ( log ` n ) ) = ( exp ` ( ( log ` n ) x. ( log ` ( exp ` A ) ) ) ) )
51 rpcn 
 |-  ( n e. RR+ -> n e. CC )
52 51 ad2antrl 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> n e. CC )
53 rpne0 
 |-  ( n e. RR+ -> n =/= 0 )
54 53 ad2antrl 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> n =/= 0 )
55 52 54 42 cxpefd 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> ( n ^c A ) = ( exp ` ( A x. ( log ` n ) ) ) )
56 45 50 55 3eqtr4d 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> ( ( exp ` A ) ^c ( log ` n ) ) = ( n ^c A ) )
57 56 oveq2d 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> ( ( log ` n ) / ( ( exp ` A ) ^c ( log ` n ) ) ) = ( ( log ` n ) / ( n ^c A ) ) )
58 57 fveq2d 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> ( abs ` ( ( log ` n ) / ( ( exp ` A ) ^c ( log ` n ) ) ) ) = ( abs ` ( ( log ` n ) / ( n ^c A ) ) ) )
59 58 breq1d 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> ( ( abs ` ( ( log ` n ) / ( ( exp ` A ) ^c ( log ` n ) ) ) ) < x <-> ( abs ` ( ( log ` n ) / ( n ^c A ) ) ) < x ) )
60 36 59 sylibd 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ ( n e. RR+ /\ ( 1 < n /\ ( exp ` z ) < n ) ) ) -> ( A. m e. RR+ ( z < m -> ( abs ` ( m / ( ( exp ` A ) ^c m ) ) ) < x ) -> ( abs ` ( ( log ` n ) / ( n ^c A ) ) ) < x ) )
61 60 expr 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ n e. RR+ ) -> ( ( 1 < n /\ ( exp ` z ) < n ) -> ( A. m e. RR+ ( z < m -> ( abs ` ( m / ( ( exp ` A ) ^c m ) ) ) < x ) -> ( abs ` ( ( log ` n ) / ( n ^c A ) ) ) < x ) ) )
62 14 61 sylbid 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ n e. RR+ ) -> ( if ( 1 <_ ( exp ` z ) , ( exp ` z ) , 1 ) < n -> ( A. m e. RR+ ( z < m -> ( abs ` ( m / ( ( exp ` A ) ^c m ) ) ) < x ) -> ( abs ` ( ( log ` n ) / ( n ^c A ) ) ) < x ) ) )
63 62 com23 
 |-  ( ( ( A e. RR+ /\ z e. RR ) /\ n e. RR+ ) -> ( A. m e. RR+ ( z < m -> ( abs ` ( m / ( ( exp ` A ) ^c m ) ) ) < x ) -> ( if ( 1 <_ ( exp ` z ) , ( exp ` z ) , 1 ) < n -> ( abs ` ( ( log ` n ) / ( n ^c A ) ) ) < x ) ) )
64 63 ralrimdva 
 |-  ( ( A e. RR+ /\ z e. RR ) -> ( A. m e. RR+ ( z < m -> ( abs ` ( m / ( ( exp ` A ) ^c m ) ) ) < x ) -> A. n e. RR+ ( if ( 1 <_ ( exp ` z ) , ( exp ` z ) , 1 ) < n -> ( abs ` ( ( log ` n ) / ( n ^c A ) ) ) < x ) ) )
65 breq1 
 |-  ( y = if ( 1 <_ ( exp ` z ) , ( exp ` z ) , 1 ) -> ( y < n <-> if ( 1 <_ ( exp ` z ) , ( exp ` z ) , 1 ) < n ) )
66 65 rspceaimv 
 |-  ( ( if ( 1 <_ ( exp ` z ) , ( exp ` z ) , 1 ) e. RR /\ A. n e. RR+ ( if ( 1 <_ ( exp ` z ) , ( exp ` z ) , 1 ) < n -> ( abs ` ( ( log ` n ) / ( n ^c A ) ) ) < x ) ) -> E. y e. RR A. n e. RR+ ( y < n -> ( abs ` ( ( log ` n ) / ( n ^c A ) ) ) < x ) )
67 11 64 66 syl6an 
 |-  ( ( A e. RR+ /\ z e. RR ) -> ( A. m e. RR+ ( z < m -> ( abs ` ( m / ( ( exp ` A ) ^c m ) ) ) < x ) -> E. y e. RR A. n e. RR+ ( y < n -> ( abs ` ( ( log ` n ) / ( n ^c A ) ) ) < x ) ) )
68 67 rexlimdva 
 |-  ( A e. RR+ -> ( E. z e. RR A. m e. RR+ ( z < m -> ( abs ` ( m / ( ( exp ` A ) ^c m ) ) ) < x ) -> E. y e. RR A. n e. RR+ ( y < n -> ( abs ` ( ( log ` n ) / ( n ^c A ) ) ) < x ) ) )
69 68 ralimdv 
 |-  ( A e. RR+ -> ( A. x e. RR+ E. z e. RR A. m e. RR+ ( z < m -> ( abs ` ( m / ( ( exp ` A ) ^c m ) ) ) < x ) -> A. x e. RR+ E. y e. RR A. n e. RR+ ( y < n -> ( abs ` ( ( log ` n ) / ( n ^c A ) ) ) < x ) ) )
70 simpr 
 |-  ( ( A e. RR+ /\ m e. RR+ ) -> m e. RR+ )
71 1 adantr 
 |-  ( ( A e. RR+ /\ m e. RR+ ) -> A e. RR )
72 71 rpefcld 
 |-  ( ( A e. RR+ /\ m e. RR+ ) -> ( exp ` A ) e. RR+ )
73 rpre 
 |-  ( m e. RR+ -> m e. RR )
74 73 adantl 
 |-  ( ( A e. RR+ /\ m e. RR+ ) -> m e. RR )
75 72 74 rpcxpcld 
 |-  ( ( A e. RR+ /\ m e. RR+ ) -> ( ( exp ` A ) ^c m ) e. RR+ )
76 70 75 rpdivcld 
 |-  ( ( A e. RR+ /\ m e. RR+ ) -> ( m / ( ( exp ` A ) ^c m ) ) e. RR+ )
77 76 rpcnd 
 |-  ( ( A e. RR+ /\ m e. RR+ ) -> ( m / ( ( exp ` A ) ^c m ) ) e. CC )
78 77 ralrimiva 
 |-  ( A e. RR+ -> A. m e. RR+ ( m / ( ( exp ` A ) ^c m ) ) e. CC )
79 rpssre 
 |-  RR+ C_ RR
80 79 a1i 
 |-  ( A e. RR+ -> RR+ C_ RR )
81 78 80 rlim0lt 
 |-  ( A e. RR+ -> ( ( m e. RR+ |-> ( m / ( ( exp ` A ) ^c m ) ) ) ~~>r 0 <-> A. x e. RR+ E. z e. RR A. m e. RR+ ( z < m -> ( abs ` ( m / ( ( exp ` A ) ^c m ) ) ) < x ) ) )
82 relogcl 
 |-  ( n e. RR+ -> ( log ` n ) e. RR )
83 82 adantl 
 |-  ( ( A e. RR+ /\ n e. RR+ ) -> ( log ` n ) e. RR )
84 simpr 
 |-  ( ( A e. RR+ /\ n e. RR+ ) -> n e. RR+ )
85 1 adantr 
 |-  ( ( A e. RR+ /\ n e. RR+ ) -> A e. RR )
86 84 85 rpcxpcld 
 |-  ( ( A e. RR+ /\ n e. RR+ ) -> ( n ^c A ) e. RR+ )
87 83 86 rerpdivcld 
 |-  ( ( A e. RR+ /\ n e. RR+ ) -> ( ( log ` n ) / ( n ^c A ) ) e. RR )
88 87 recnd 
 |-  ( ( A e. RR+ /\ n e. RR+ ) -> ( ( log ` n ) / ( n ^c A ) ) e. CC )
89 88 ralrimiva 
 |-  ( A e. RR+ -> A. n e. RR+ ( ( log ` n ) / ( n ^c A ) ) e. CC )
90 89 80 rlim0lt 
 |-  ( A e. RR+ -> ( ( n e. RR+ |-> ( ( log ` n ) / ( n ^c A ) ) ) ~~>r 0 <-> A. x e. RR+ E. y e. RR A. n e. RR+ ( y < n -> ( abs ` ( ( log ` n ) / ( n ^c A ) ) ) < x ) ) )
91 69 81 90 3imtr4d 
 |-  ( A e. RR+ -> ( ( m e. RR+ |-> ( m / ( ( exp ` A ) ^c m ) ) ) ~~>r 0 -> ( n e. RR+ |-> ( ( log ` n ) / ( n ^c A ) ) ) ~~>r 0 ) )
92 6 91 mpd 
 |-  ( A e. RR+ -> ( n e. RR+ |-> ( ( log ` n ) / ( n ^c A ) ) ) ~~>r 0 )