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 )