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