Metamath Proof Explorer

Theorem divlogrlim

Description: The inverse logarithm function converges to zero. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Assertion divlogrlim 
|- ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~>r 0

Proof

Step Hyp Ref Expression
1 elioore 
 |-  ( x e. ( 1 (,) +oo ) -> x e. RR )
2 eliooord 
 |-  ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
3 2 simpld 
 |-  ( x e. ( 1 (,) +oo ) -> 1 < x )
4 1 3 rplogcld 
 |-  ( x e. ( 1 (,) +oo ) -> ( log ` x ) e. RR+ )
5 4 rprecred 
 |-  ( x e. ( 1 (,) +oo ) -> ( 1 / ( log ` x ) ) e. RR )
6 5 recnd 
 |-  ( x e. ( 1 (,) +oo ) -> ( 1 / ( log ` x ) ) e. CC )
7 6 rgen 
 |-  A. x e. ( 1 (,) +oo ) ( 1 / ( log ` x ) ) e. CC
8 7 a1i 
 |-  ( T. -> A. x e. ( 1 (,) +oo ) ( 1 / ( log ` x ) ) e. CC )
9 ioossre 
 |-  ( 1 (,) +oo ) C_ RR
10 9 a1i 
 |-  ( T. -> ( 1 (,) +oo ) C_ RR )
11 8 10 rlim0lt 
 |-  ( T. -> ( ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~>r 0 <-> A. y e. RR+ E. c e. RR A. x e. ( 1 (,) +oo ) ( c < x -> ( abs ` ( 1 / ( log ` x ) ) ) < y ) ) )
12 11 mptru 
 |-  ( ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~>r 0 <-> A. y e. RR+ E. c e. RR A. x e. ( 1 (,) +oo ) ( c < x -> ( abs ` ( 1 / ( log ` x ) ) ) < y ) )
13 id 
 |-  ( y e. RR+ -> y e. RR+ )
14 13 rprecred 
 |-  ( y e. RR+ -> ( 1 / y ) e. RR )
15 14 reefcld 
 |-  ( y e. RR+ -> ( exp ` ( 1 / y ) ) e. RR )
16 5 ad2antlr 
 |-  ( ( ( y e. RR+ /\ x e. ( 1 (,) +oo ) ) /\ ( exp ` ( 1 / y ) ) < x ) -> ( 1 / ( log ` x ) ) e. RR )
17 1 ad2antlr 
 |-  ( ( ( y e. RR+ /\ x e. ( 1 (,) +oo ) ) /\ ( exp ` ( 1 / y ) ) < x ) -> x e. RR )
18 3 ad2antlr 
 |-  ( ( ( y e. RR+ /\ x e. ( 1 (,) +oo ) ) /\ ( exp ` ( 1 / y ) ) < x ) -> 1 < x )
19 17 18 rplogcld 
 |-  ( ( ( y e. RR+ /\ x e. ( 1 (,) +oo ) ) /\ ( exp ` ( 1 / y ) ) < x ) -> ( log ` x ) e. RR+ )
20 19 rpreccld 
 |-  ( ( ( y e. RR+ /\ x e. ( 1 (,) +oo ) ) /\ ( exp ` ( 1 / y ) ) < x ) -> ( 1 / ( log ` x ) ) e. RR+ )
21 20 rpge0d 
 |-  ( ( ( y e. RR+ /\ x e. ( 1 (,) +oo ) ) /\ ( exp ` ( 1 / y ) ) < x ) -> 0 <_ ( 1 / ( log ` x ) ) )
22 16 21 absidd 
 |-  ( ( ( y e. RR+ /\ x e. ( 1 (,) +oo ) ) /\ ( exp ` ( 1 / y ) ) < x ) -> ( abs ` ( 1 / ( log ` x ) ) ) = ( 1 / ( log ` x ) ) )
23 simpll 
 |-  ( ( ( y e. RR+ /\ x e. ( 1 (,) +oo ) ) /\ ( exp ` ( 1 / y ) ) < x ) -> y e. RR+ )
24 4 ad2antlr 
 |-  ( ( ( y e. RR+ /\ x e. ( 1 (,) +oo ) ) /\ ( exp ` ( 1 / y ) ) < x ) -> ( log ` x ) e. RR+ )
25 simpr 
 |-  ( ( ( y e. RR+ /\ x e. ( 1 (,) +oo ) ) /\ ( exp ` ( 1 / y ) ) < x ) -> ( exp ` ( 1 / y ) ) < x )
26 1rp 
 |-  1 e. RR+
27 26 a1i 
 |-  ( ( ( y e. RR+ /\ x e. ( 1 (,) +oo ) ) /\ ( exp ` ( 1 / y ) ) < x ) -> 1 e. RR+ )
28 27 rpred 
 |-  ( ( ( y e. RR+ /\ x e. ( 1 (,) +oo ) ) /\ ( exp ` ( 1 / y ) ) < x ) -> 1 e. RR )
29 28 17 18 ltled 
 |-  ( ( ( y e. RR+ /\ x e. ( 1 (,) +oo ) ) /\ ( exp ` ( 1 / y ) ) < x ) -> 1 <_ x )
30 17 27 29 rpgecld 
 |-  ( ( ( y e. RR+ /\ x e. ( 1 (,) +oo ) ) /\ ( exp ` ( 1 / y ) ) < x ) -> x e. RR+ )
31 30 reeflogd 
 |-  ( ( ( y e. RR+ /\ x e. ( 1 (,) +oo ) ) /\ ( exp ` ( 1 / y ) ) < x ) -> ( exp ` ( log ` x ) ) = x )
32 25 31 breqtrrd 
 |-  ( ( ( y e. RR+ /\ x e. ( 1 (,) +oo ) ) /\ ( exp ` ( 1 / y ) ) < x ) -> ( exp ` ( 1 / y ) ) < ( exp ` ( log ` x ) ) )
33 23 rprecred 
 |-  ( ( ( y e. RR+ /\ x e. ( 1 (,) +oo ) ) /\ ( exp ` ( 1 / y ) ) < x ) -> ( 1 / y ) e. RR )
34 24 rpred 
 |-  ( ( ( y e. RR+ /\ x e. ( 1 (,) +oo ) ) /\ ( exp ` ( 1 / y ) ) < x ) -> ( log ` x ) e. RR )
35 eflt 
 |-  ( ( ( 1 / y ) e. RR /\ ( log ` x ) e. RR ) -> ( ( 1 / y ) < ( log ` x ) <-> ( exp ` ( 1 / y ) ) < ( exp ` ( log ` x ) ) ) )
36 33 34 35 syl2anc 
 |-  ( ( ( y e. RR+ /\ x e. ( 1 (,) +oo ) ) /\ ( exp ` ( 1 / y ) ) < x ) -> ( ( 1 / y ) < ( log ` x ) <-> ( exp ` ( 1 / y ) ) < ( exp ` ( log ` x ) ) ) )
37 32 36 mpbird 
 |-  ( ( ( y e. RR+ /\ x e. ( 1 (,) +oo ) ) /\ ( exp ` ( 1 / y ) ) < x ) -> ( 1 / y ) < ( log ` x ) )
38 23 24 37 ltrec1d 
 |-  ( ( ( y e. RR+ /\ x e. ( 1 (,) +oo ) ) /\ ( exp ` ( 1 / y ) ) < x ) -> ( 1 / ( log ` x ) ) < y )
39 22 38 eqbrtrd 
 |-  ( ( ( y e. RR+ /\ x e. ( 1 (,) +oo ) ) /\ ( exp ` ( 1 / y ) ) < x ) -> ( abs ` ( 1 / ( log ` x ) ) ) < y )
40 39 ex 
 |-  ( ( y e. RR+ /\ x e. ( 1 (,) +oo ) ) -> ( ( exp ` ( 1 / y ) ) < x -> ( abs ` ( 1 / ( log ` x ) ) ) < y ) )
41 40 ralrimiva 
 |-  ( y e. RR+ -> A. x e. ( 1 (,) +oo ) ( ( exp ` ( 1 / y ) ) < x -> ( abs ` ( 1 / ( log ` x ) ) ) < y ) )
42 breq1 
 |-  ( c = ( exp ` ( 1 / y ) ) -> ( c < x <-> ( exp ` ( 1 / y ) ) < x ) )
43 42 rspceaimv 
 |-  ( ( ( exp ` ( 1 / y ) ) e. RR /\ A. x e. ( 1 (,) +oo ) ( ( exp ` ( 1 / y ) ) < x -> ( abs ` ( 1 / ( log ` x ) ) ) < y ) ) -> E. c e. RR A. x e. ( 1 (,) +oo ) ( c < x -> ( abs ` ( 1 / ( log ` x ) ) ) < y ) )
44 15 41 43 syl2anc 
 |-  ( y e. RR+ -> E. c e. RR A. x e. ( 1 (,) +oo ) ( c < x -> ( abs ` ( 1 / ( log ` x ) ) ) < y ) )
45 12 44 mprgbir 
 |-  ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~>r 0