Metamath Proof Explorer

Theorem logno1

Description: The logarithm function is not eventually bounded. (Contributed by Mario Carneiro, 30-Apr-2016) (Proof shortened by Mario Carneiro, 30-May-2016)

Ref Expression
Assertion logno1 
|- -. ( x e. RR+ |-> ( log ` x ) ) e. O(1)

Proof

Step Hyp Ref Expression
1 elioore 
 |-  ( y e. ( 1 (,) +oo ) -> y e. RR )
2 1 adantl 
 |-  ( ( ( x e. RR+ |-> ( log ` x ) ) e. O(1) /\ y e. ( 1 (,) +oo ) ) -> y e. RR )
3 1rp 
 |-  1 e. RR+
4 3 a1i 
 |-  ( ( ( x e. RR+ |-> ( log ` x ) ) e. O(1) /\ y e. ( 1 (,) +oo ) ) -> 1 e. RR+ )
5 1red 
 |-  ( ( ( x e. RR+ |-> ( log ` x ) ) e. O(1) /\ y e. ( 1 (,) +oo ) ) -> 1 e. RR )
6 eliooord 
 |-  ( y e. ( 1 (,) +oo ) -> ( 1 < y /\ y < +oo ) )
7 6 adantl 
 |-  ( ( ( x e. RR+ |-> ( log ` x ) ) e. O(1) /\ y e. ( 1 (,) +oo ) ) -> ( 1 < y /\ y < +oo ) )
8 7 simpld 
 |-  ( ( ( x e. RR+ |-> ( log ` x ) ) e. O(1) /\ y e. ( 1 (,) +oo ) ) -> 1 < y )
9 5 2 8 ltled 
 |-  ( ( ( x e. RR+ |-> ( log ` x ) ) e. O(1) /\ y e. ( 1 (,) +oo ) ) -> 1 <_ y )
10 2 4 9 rpgecld 
 |-  ( ( ( x e. RR+ |-> ( log ` x ) ) e. O(1) /\ y e. ( 1 (,) +oo ) ) -> y e. RR+ )
11 10 ex 
 |-  ( ( x e. RR+ |-> ( log ` x ) ) e. O(1) -> ( y e. ( 1 (,) +oo ) -> y e. RR+ ) )
12 11 ssrdv 
 |-  ( ( x e. RR+ |-> ( log ` x ) ) e. O(1) -> ( 1 (,) +oo ) C_ RR+ )
13 fveq2 
 |-  ( x = y -> ( log ` x ) = ( log ` y ) )
14 13 cbvmptv 
 |-  ( x e. RR+ |-> ( log ` x ) ) = ( y e. RR+ |-> ( log ` y ) )
15 14 eleq1i 
 |-  ( ( x e. RR+ |-> ( log ` x ) ) e. O(1) <-> ( y e. RR+ |-> ( log ` y ) ) e. O(1) )
16 15 biimpi 
 |-  ( ( x e. RR+ |-> ( log ` x ) ) e. O(1) -> ( y e. RR+ |-> ( log ` y ) ) e. O(1) )
17 12 16 o1res2 
 |-  ( ( x e. RR+ |-> ( log ` x ) ) e. O(1) -> ( y e. ( 1 (,) +oo ) |-> ( log ` y ) ) e. O(1) )
18 1red 
 |-  ( ( x e. RR+ |-> ( log ` x ) ) e. O(1) -> 1 e. RR )
19 18 rexrd 
 |-  ( ( x e. RR+ |-> ( log ` x ) ) e. O(1) -> 1 e. RR* )
20 18 renepnfd 
 |-  ( ( x e. RR+ |-> ( log ` x ) ) e. O(1) -> 1 =/= +oo )
21 ioopnfsup 
 |-  ( ( 1 e. RR* /\ 1 =/= +oo ) -> sup ( ( 1 (,) +oo ) , RR* , < ) = +oo )
22 19 20 21 syl2anc 
 |-  ( ( x e. RR+ |-> ( log ` x ) ) e. O(1) -> sup ( ( 1 (,) +oo ) , RR* , < ) = +oo )
23 divlogrlim 
 |-  ( y e. ( 1 (,) +oo ) |-> ( 1 / ( log ` y ) ) ) ~~>r 0
24 23 a1i 
 |-  ( ( x e. RR+ |-> ( log ` x ) ) e. O(1) -> ( y e. ( 1 (,) +oo ) |-> ( 1 / ( log ` y ) ) ) ~~>r 0 )
25 2 8 rplogcld 
 |-  ( ( ( x e. RR+ |-> ( log ` x ) ) e. O(1) /\ y e. ( 1 (,) +oo ) ) -> ( log ` y ) e. RR+ )
26 25 rpcnd 
 |-  ( ( ( x e. RR+ |-> ( log ` x ) ) e. O(1) /\ y e. ( 1 (,) +oo ) ) -> ( log ` y ) e. CC )
27 25 rpne0d 
 |-  ( ( ( x e. RR+ |-> ( log ` x ) ) e. O(1) /\ y e. ( 1 (,) +oo ) ) -> ( log ` y ) =/= 0 )
28 22 24 26 27 rlimno1 
 |-  ( ( x e. RR+ |-> ( log ` x ) ) e. O(1) -> -. ( y e. ( 1 (,) +oo ) |-> ( log ` y ) ) e. O(1) )
29 17 28 pm2.65i 
 |-  -. ( x e. RR+ |-> ( log ` x ) ) e. O(1)