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 mnfxr 
 |-  -oo e. RR*
66 0re 
 |-  0 e. RR
67 elioc2 
 |-  ( ( -oo e. RR* /\ 0 e. RR ) -> ( ( exp ` x ) e. ( -oo (,] 0 ) <-> ( ( exp ` x ) e. RR /\ -oo < ( exp ` x ) /\ ( exp ` x ) <_ 0 ) ) )
68 65 66 67 mp2an 
 |-  ( ( exp ` x ) e. ( -oo (,] 0 ) <-> ( ( exp ` x ) e. RR /\ -oo < ( exp ` x ) /\ ( exp ` x ) <_ 0 ) )
69 68 bilani 
 |-  ( ( x e. ( `' Im " ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. ( -oo (,] 0 ) ) -> ( ( exp ` x ) e. RR /\ -oo < ( exp ` x ) /\ ( exp ` x ) <_ 0 ) )
70 69 simp1d 
 |-  ( ( x e. ( `' Im " ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. ( -oo (,] 0 ) ) -> ( exp ` x ) e. RR )
71 0red 
 |-  ( ( x e. ( `' Im " ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. ( -oo (,] 0 ) ) -> 0 e. RR )
72 69 simp3d 
 |-  ( ( x e. ( `' Im " ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. ( -oo (,] 0 ) ) -> ( exp ` x ) <_ 0 )
73 efne0 
 |-  ( x e. CC -> ( exp ` x ) =/= 0 )
74 57 73 syl 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> ( exp ` x ) =/= 0 )
75 74 adantr 
 |-  ( ( x e. ( `' Im " ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. ( -oo (,] 0 ) ) -> ( exp ` x ) =/= 0 )
76 75 necomd 
 |-  ( ( x e. ( `' Im " ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. ( -oo (,] 0 ) ) -> 0 =/= ( exp ` x ) )
77 70 71 72 76 leneltd 
 |-  ( ( x e. ( `' Im " ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. ( -oo (,] 0 ) ) -> ( exp ` x ) < 0 )
78 70 77 negelrpd 
 |-  ( ( x e. ( `' Im " ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. ( -oo (,] 0 ) ) -> -u ( exp ` x ) e. RR+ )
79 lognegb 
 |-  ( ( ( exp ` x ) e. CC /\ ( exp ` x ) =/= 0 ) -> ( -u ( exp ` x ) e. RR+ <-> ( Im ` ( log ` ( exp ` x ) ) ) = _pi ) )
80 56 74 79 syl2anc 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> ( -u ( exp ` x ) e. RR+ <-> ( Im ` ( log ` ( exp ` x ) ) ) = _pi ) )
81 80 adantr 
 |-  ( ( x e. ( `' Im " ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. ( -oo (,] 0 ) ) -> ( -u ( exp ` x ) e. RR+ <-> ( Im ` ( log ` ( exp ` x ) ) ) = _pi ) )
82 78 81 mpbid 
 |-  ( ( x e. ( `' Im " ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. ( -oo (,] 0 ) ) -> ( Im ` ( log ` ( exp ` x ) ) ) = _pi )
83 64 82 eqtr3d 
 |-  ( ( x e. ( `' Im " ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. ( -oo (,] 0 ) ) -> ( Im ` x ) = _pi )
84 83 ex 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> ( ( exp ` x ) e. ( -oo (,] 0 ) -> ( Im ` x ) = _pi ) )
85 84 necon3ad 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> ( ( Im ` x ) =/= _pi -> -. ( exp ` x ) e. ( -oo (,] 0 ) ) )
86 62 85 mpd 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> -. ( exp ` x ) e. ( -oo (,] 0 ) )
87 56 86 eldifd 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> ( exp ` x ) e. ( CC \ ( -oo (,] 0 ) ) )
88 87 1 eleqtrrdi 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> ( exp ` x ) e. D )
89 funfvima2 
 |-  ( ( Fun log /\ D C_ dom log ) -> ( ( exp ` x ) e. D -> ( log ` ( exp ` x ) ) e. ( log " D ) ) )
90 4 8 89 mp2an 
 |-  ( ( exp ` x ) e. D -> ( log ` ( exp ` x ) ) e. ( log " D ) )
91 88 90 syl 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> ( log ` ( exp ` x ) ) e. ( log " D ) )
92 51 91 eqeltrrd 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> x e. ( log " D ) )
93 92 ssriv 
 |-  ( `' Im " ( -u _pi (,) _pi ) ) C_ ( log " D )
94 39 93 eqssi 
 |-  ( log " D ) = ( `' Im " ( -u _pi (,) _pi ) )
95 imcncf 
 |-  Im e. ( CC -cn-> RR )
96 ssid 
 |-  CC C_ CC
97 ax-resscn 
 |-  RR C_ CC
98 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
99 98 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
100 99 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
101 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
102 98 100 101 cncfcn 
 |-  ( ( CC C_ CC /\ RR C_ CC ) -> ( CC -cn-> RR ) = ( ( TopOpen ` CCfld ) Cn ( topGen ` ran (,) ) ) )
103 96 97 102 mp2an 
 |-  ( CC -cn-> RR ) = ( ( TopOpen ` CCfld ) Cn ( topGen ` ran (,) ) )
104 95 103 eleqtri 
 |-  Im e. ( ( TopOpen ` CCfld ) Cn ( topGen ` ran (,) ) )
105 iooretop 
 |-  ( -u _pi (,) _pi ) e. ( topGen ` ran (,) )
106 cnima 
 |-  ( ( Im e. ( ( TopOpen ` CCfld ) Cn ( topGen ` ran (,) ) ) /\ ( -u _pi (,) _pi ) e. ( topGen ` ran (,) ) ) -> ( `' Im " ( -u _pi (,) _pi ) ) e. ( TopOpen ` CCfld ) )
107 104 105 106 mp2an 
 |-  ( `' Im " ( -u _pi (,) _pi ) ) e. ( TopOpen ` CCfld )
108 94 107 eqeltri 
 |-  ( log " D ) e. ( TopOpen ` CCfld )