Metamath Proof Explorer

Theorem dvloglem

Description: Lemma for dvlog . (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypothesis logcn.d 
|- D = ( CC \ ( -oo (,] 0 ) )
Assertion dvloglem 
|- ( log " D ) e. ( TopOpen ` CCfld )

Proof

Step Hyp Ref Expression
1 logcn.d 
 |-  D = ( CC \ ( -oo (,] 0 ) )
2 logf1o 
 |-  log : ( CC \ { 0 } ) -1-1-onto-> ran log
3 f1ofun 
 |-  ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> Fun log )
4 2 3 ax-mp 
 |-  Fun log
5 1 logdmss 
 |-  D C_ ( CC \ { 0 } )
6 f1odm 
 |-  ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> dom log = ( CC \ { 0 } ) )
7 2 6 ax-mp 
 |-  dom log = ( CC \ { 0 } )
8 5 7 sseqtrri 
 |-  D C_ dom log
9 funimass4 
 |-  ( ( Fun log /\ D C_ dom log ) -> ( ( log " D ) C_ ( `' Im " ( -u _pi (,) _pi ) ) <-> A. x e. D ( log ` x ) e. ( `' Im " ( -u _pi (,) _pi ) ) ) )
10 4 8 9 mp2an 
 |-  ( ( log " D ) C_ ( `' Im " ( -u _pi (,) _pi ) ) <-> A. x e. D ( log ` x ) e. ( `' Im " ( -u _pi (,) _pi ) ) )
11 1 ellogdm 
 |-  ( x e. D <-> ( x e. CC /\ ( x e. RR -> x e. RR+ ) ) )
12 11 simplbi 
 |-  ( x e. D -> x e. CC )
13 1 logdmn0 
 |-  ( x e. D -> x =/= 0 )
14 12 13 logcld 
 |-  ( x e. D -> ( log ` x ) e. CC )
15 14 imcld 
 |-  ( x e. D -> ( Im ` ( log ` x ) ) e. RR )
16 12 13 logimcld 
 |-  ( x e. D -> ( -u _pi < ( Im ` ( log ` x ) ) /\ ( Im ` ( log ` x ) ) <_ _pi ) )
17 16 simpld 
 |-  ( x e. D -> -u _pi < ( Im ` ( log ` x ) ) )
18 pire 
 |-  _pi e. RR
19 18 a1i 
 |-  ( x e. D -> _pi e. RR )
20 16 simprd 
 |-  ( x e. D -> ( Im ` ( log ` x ) ) <_ _pi )
21 1 logdmnrp 
 |-  ( x e. D -> -. -u x e. RR+ )
22 lognegb 
 |-  ( ( x e. CC /\ x =/= 0 ) -> ( -u x e. RR+ <-> ( Im ` ( log ` x ) ) = _pi ) )
23 12 13 22 syl2anc 
 |-  ( x e. D -> ( -u x e. RR+ <-> ( Im ` ( log ` x ) ) = _pi ) )
24 23 necon3bbid 
 |-  ( x e. D -> ( -. -u x e. RR+ <-> ( Im ` ( log ` x ) ) =/= _pi ) )
25 21 24 mpbid 
 |-  ( x e. D -> ( Im ` ( log ` x ) ) =/= _pi )
26 25 necomd 
 |-  ( x e. D -> _pi =/= ( Im ` ( log ` x ) ) )
27 15 19 20 26 leneltd 
 |-  ( x e. D -> ( Im ` ( log ` x ) ) < _pi )
28 18 renegcli 
 |-  -u _pi e. RR
29 28 rexri 
 |-  -u _pi e. RR*
30 18 rexri 
 |-  _pi e. RR*
31 elioo2 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR* ) -> ( ( Im ` ( log ` x ) ) e. ( -u _pi (,) _pi ) <-> ( ( Im ` ( log ` x ) ) e. RR /\ -u _pi < ( Im ` ( log ` x ) ) /\ ( Im ` ( log ` x ) ) < _pi ) ) )
32 29 30 31 mp2an 
 |-  ( ( Im ` ( log ` x ) ) e. ( -u _pi (,) _pi ) <-> ( ( Im ` ( log ` x ) ) e. RR /\ -u _pi < ( Im ` ( log ` x ) ) /\ ( Im ` ( log ` x ) ) < _pi ) )
33 15 17 27 32 syl3anbrc 
 |-  ( x e. D -> ( Im ` ( log ` x ) ) e. ( -u _pi (,) _pi ) )
34 imf 
 |-  Im : CC --> RR
35 ffn 
 |-  ( Im : CC --> RR -> Im Fn CC )
36 elpreima 
 |-  ( Im Fn CC -> ( ( log ` x ) e. ( `' Im " ( -u _pi (,) _pi ) ) <-> ( ( log ` x ) e. CC /\ ( Im ` ( log ` x ) ) e. ( -u _pi (,) _pi ) ) ) )
37 34 35 36 mp2b 
 |-  ( ( log ` x ) e. ( `' Im " ( -u _pi (,) _pi ) ) <-> ( ( log ` x ) e. CC /\ ( Im ` ( log ` x ) ) e. ( -u _pi (,) _pi ) ) )
38 14 33 37 sylanbrc 
 |-  ( x e. D -> ( log ` x ) e. ( `' Im " ( -u _pi (,) _pi ) ) )
39 10 38 mprgbir 
 |-  ( log " D ) C_ ( `' Im " ( -u _pi (,) _pi ) )
40 df-ioo 
 |-  (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
41 df-ioc 
 |-  (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
42 idd 
 |-  ( ( -u _pi e. RR* /\ w e. RR* ) -> ( -u _pi < w -> -u _pi < w ) )
43 xrltle 
 |-  ( ( w e. RR* /\ _pi e. RR* ) -> ( w < _pi -> w <_ _pi ) )
44 40 41 42 43 ixxssixx 
 |-  ( -u _pi (,) _pi ) C_ ( -u _pi (,] _pi )
45 imass2 
 |-  ( ( -u _pi (,) _pi ) C_ ( -u _pi (,] _pi ) -> ( `' Im " ( -u _pi (,) _pi ) ) C_ ( `' Im " ( -u _pi (,] _pi ) ) )
46 44 45 ax-mp 
 |-  ( `' Im " ( -u _pi (,) _pi ) ) C_ ( `' Im " ( -u _pi (,] _pi ) )
47 logrn 
 |-  ran log = ( `' Im " ( -u _pi (,] _pi ) )
48 46 47 sseqtrri 
 |-  ( `' Im " ( -u _pi (,) _pi ) ) C_ ran log
49 48 sseli 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> x e. ran log )
50 logef 
 |-  ( x e. ran log -> ( log ` ( exp ` x ) ) = x )
51 49 50 syl 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> ( log ` ( exp ` x ) ) = x )
52 elpreima 
 |-  ( Im Fn CC -> ( x e. ( `' Im " ( -u _pi (,) _pi ) ) <-> ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) ) )
53 34 35 52 mp2b 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) <-> ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) )
54 efcl 
 |-  ( x e. CC -> ( exp ` x ) e. CC )
55 54 adantr 
 |-  ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) -> ( exp ` x ) e. CC )
56 53 55 sylbi 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> ( exp ` x ) e. CC )
57 53 simplbi 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> x e. CC )
58 57 imcld 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> ( Im ` x ) e. RR )
59 eliooord 
 |-  ( ( Im ` x ) e. ( -u _pi (,) _pi ) -> ( -u _pi < ( Im ` x ) /\ ( Im ` x ) < _pi ) )
60 53 59 simplbiim 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> ( -u _pi < ( Im ` x ) /\ ( Im ` x ) < _pi ) )
61 60 simprd 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> ( Im ` x ) < _pi )
62 58 61 ltned 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> ( Im ` x ) =/= _pi )
63 51 adantr 
 |-  ( ( x e. ( `' Im " ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. ( -oo (,] 0 ) ) -> ( log ` ( exp ` x ) ) = x )
64 63 fveq2d 
 |-  ( ( x e. ( `' Im " ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. ( -oo (,] 0 ) ) -> ( Im ` ( log ` ( exp ` x ) ) ) = ( Im ` x ) )
65 simpr 
 |-  ( ( x e. ( `' Im " ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. ( -oo (,] 0 ) ) -> ( exp ` x ) e. ( -oo (,] 0 ) )
66 mnfxr 
 |-  -oo e. RR*
67 0re 
 |-  0 e. RR
68 elioc2 
 |-  ( ( -oo e. RR* /\ 0 e. RR ) -> ( ( exp ` x ) e. ( -oo (,] 0 ) <-> ( ( exp ` x ) e. RR /\ -oo < ( exp ` x ) /\ ( exp ` x ) <_ 0 ) ) )
69 66 67 68 mp2an 
 |-  ( ( exp ` x ) e. ( -oo (,] 0 ) <-> ( ( exp ` x ) e. RR /\ -oo < ( exp ` x ) /\ ( exp ` x ) <_ 0 ) )
70 65 69 sylib 
 |-  ( ( x e. ( `' Im " ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. ( -oo (,] 0 ) ) -> ( ( exp ` x ) e. RR /\ -oo < ( exp ` x ) /\ ( exp ` x ) <_ 0 ) )
71 70 simp1d 
 |-  ( ( x e. ( `' Im " ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. ( -oo (,] 0 ) ) -> ( exp ` x ) e. RR )
72 0red 
 |-  ( ( x e. ( `' Im " ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. ( -oo (,] 0 ) ) -> 0 e. RR )
73 70 simp3d 
 |-  ( ( x e. ( `' Im " ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. ( -oo (,] 0 ) ) -> ( exp ` x ) <_ 0 )
74 efne0 
 |-  ( x e. CC -> ( exp ` x ) =/= 0 )
75 57 74 syl 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> ( exp ` x ) =/= 0 )
76 75 adantr 
 |-  ( ( x e. ( `' Im " ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. ( -oo (,] 0 ) ) -> ( exp ` x ) =/= 0 )
77 76 necomd 
 |-  ( ( x e. ( `' Im " ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. ( -oo (,] 0 ) ) -> 0 =/= ( exp ` x ) )
78 71 72 73 77 leneltd 
 |-  ( ( x e. ( `' Im " ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. ( -oo (,] 0 ) ) -> ( exp ` x ) < 0 )
79 71 78 negelrpd 
 |-  ( ( x e. ( `' Im " ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. ( -oo (,] 0 ) ) -> -u ( exp ` x ) e. RR+ )
80 lognegb 
 |-  ( ( ( exp ` x ) e. CC /\ ( exp ` x ) =/= 0 ) -> ( -u ( exp ` x ) e. RR+ <-> ( Im ` ( log ` ( exp ` x ) ) ) = _pi ) )
81 56 75 80 syl2anc 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> ( -u ( exp ` x ) e. RR+ <-> ( Im ` ( log ` ( exp ` x ) ) ) = _pi ) )
82 81 adantr 
 |-  ( ( x e. ( `' Im " ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. ( -oo (,] 0 ) ) -> ( -u ( exp ` x ) e. RR+ <-> ( Im ` ( log ` ( exp ` x ) ) ) = _pi ) )
83 79 82 mpbid 
 |-  ( ( x e. ( `' Im " ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. ( -oo (,] 0 ) ) -> ( Im ` ( log ` ( exp ` x ) ) ) = _pi )
84 64 83 eqtr3d 
 |-  ( ( x e. ( `' Im " ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. ( -oo (,] 0 ) ) -> ( Im ` x ) = _pi )
85 84 ex 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> ( ( exp ` x ) e. ( -oo (,] 0 ) -> ( Im ` x ) = _pi ) )
86 85 necon3ad 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> ( ( Im ` x ) =/= _pi -> -. ( exp ` x ) e. ( -oo (,] 0 ) ) )
87 62 86 mpd 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> -. ( exp ` x ) e. ( -oo (,] 0 ) )
88 56 87 eldifd 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> ( exp ` x ) e. ( CC \ ( -oo (,] 0 ) ) )
89 88 1 eleqtrrdi 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> ( exp ` x ) e. D )
90 funfvima2 
 |-  ( ( Fun log /\ D C_ dom log ) -> ( ( exp ` x ) e. D -> ( log ` ( exp ` x ) ) e. ( log " D ) ) )
91 4 8 90 mp2an 
 |-  ( ( exp ` x ) e. D -> ( log ` ( exp ` x ) ) e. ( log " D ) )
92 89 91 syl 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> ( log ` ( exp ` x ) ) e. ( log " D ) )
93 51 92 eqeltrrd 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> x e. ( log " D ) )
94 93 ssriv 
 |-  ( `' Im " ( -u _pi (,) _pi ) ) C_ ( log " D )
95 39 94 eqssi 
 |-  ( log " D ) = ( `' Im " ( -u _pi (,) _pi ) )
96 imcncf 
 |-  Im e. ( CC -cn-> RR )
97 ssid 
 |-  CC C_ CC
98 ax-resscn 
 |-  RR C_ CC
99 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
100 99 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
101 100 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
102 99 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
103 99 101 102 cncfcn 
 |-  ( ( CC C_ CC /\ RR C_ CC ) -> ( CC -cn-> RR ) = ( ( TopOpen ` CCfld ) Cn ( topGen ` ran (,) ) ) )
104 97 98 103 mp2an 
 |-  ( CC -cn-> RR ) = ( ( TopOpen ` CCfld ) Cn ( topGen ` ran (,) ) )
105 96 104 eleqtri 
 |-  Im e. ( ( TopOpen ` CCfld ) Cn ( topGen ` ran (,) ) )
106 iooretop 
 |-  ( -u _pi (,) _pi ) e. ( topGen ` ran (,) )
107 cnima 
 |-  ( ( Im e. ( ( TopOpen ` CCfld ) Cn ( topGen ` ran (,) ) ) /\ ( -u _pi (,) _pi ) e. ( topGen ` ran (,) ) ) -> ( `' Im " ( -u _pi (,) _pi ) ) e. ( TopOpen ` CCfld ) )
108 105 106 107 mp2an 
 |-  ( `' Im " ( -u _pi (,) _pi ) ) e. ( TopOpen ` CCfld )
109 95 108 eqeltri 
 |-  ( log " D ) e. ( TopOpen ` CCfld )