Metamath Proof Explorer

Theorem logf1o2

Description: The logarithm maps its continuous domain bijectively onto the set of numbers with imaginary part -upi < Im ( z ) < pi . The negative reals are mapped to the numbers with imaginary part equal to _pi . (Contributed by Mario Carneiro, 2-May-2015)

Ref Expression
Hypothesis logcn.d 
|- D = ( CC \ ( -oo (,] 0 ) )
Assertion logf1o2 
|- ( log |` D ) : D -1-1-onto-> ( `' Im " ( -u _pi (,) _pi ) )

Proof

Step Hyp Ref Expression
1 logcn.d 
 |-  D = ( CC \ ( -oo (,] 0 ) )
2 logf1o 
 |-  log : ( CC \ { 0 } ) -1-1-onto-> ran log
3 f1of1 
 |-  ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> log : ( CC \ { 0 } ) -1-1-> ran log )
4 2 3 ax-mp 
 |-  log : ( CC \ { 0 } ) -1-1-> ran log
5 1 logdmss 
 |-  D C_ ( CC \ { 0 } )
6 f1ores 
 |-  ( ( log : ( CC \ { 0 } ) -1-1-> ran log /\ D C_ ( CC \ { 0 } ) ) -> ( log |` D ) : D -1-1-onto-> ( log " D ) )
7 4 5 6 mp2an 
 |-  ( log |` D ) : D -1-1-onto-> ( log " D )
8 f1ofun 
 |-  ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> Fun log )
9 2 8 ax-mp 
 |-  Fun log
10 f1of 
 |-  ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> log : ( CC \ { 0 } ) --> ran log )
11 2 10 ax-mp 
 |-  log : ( CC \ { 0 } ) --> ran log
12 11 fdmi 
 |-  dom log = ( CC \ { 0 } )
13 5 12 sseqtrri 
 |-  D C_ dom log
14 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 ) ) ) )
15 9 13 14 mp2an 
 |-  ( ( log " D ) C_ ( `' Im " ( -u _pi (,) _pi ) ) <-> A. x e. D ( log ` x ) e. ( `' Im " ( -u _pi (,) _pi ) ) )
16 1 ellogdm 
 |-  ( x e. D <-> ( x e. CC /\ ( x e. RR -> x e. RR+ ) ) )
17 16 simplbi 
 |-  ( x e. D -> x e. CC )
18 1 logdmn0 
 |-  ( x e. D -> x =/= 0 )
19 17 18 logcld 
 |-  ( x e. D -> ( log ` x ) e. CC )
20 19 imcld 
 |-  ( x e. D -> ( Im ` ( log ` x ) ) e. RR )
21 17 18 logimcld 
 |-  ( x e. D -> ( -u _pi < ( Im ` ( log ` x ) ) /\ ( Im ` ( log ` x ) ) <_ _pi ) )
22 21 simpld 
 |-  ( x e. D -> -u _pi < ( Im ` ( log ` x ) ) )
23 pire 
 |-  _pi e. RR
24 23 a1i 
 |-  ( x e. D -> _pi e. RR )
25 21 simprd 
 |-  ( x e. D -> ( Im ` ( log ` x ) ) <_ _pi )
26 1 logdmnrp 
 |-  ( x e. D -> -. -u x e. RR+ )
27 lognegb 
 |-  ( ( x e. CC /\ x =/= 0 ) -> ( -u x e. RR+ <-> ( Im ` ( log ` x ) ) = _pi ) )
28 17 18 27 syl2anc 
 |-  ( x e. D -> ( -u x e. RR+ <-> ( Im ` ( log ` x ) ) = _pi ) )
29 28 necon3bbid 
 |-  ( x e. D -> ( -. -u x e. RR+ <-> ( Im ` ( log ` x ) ) =/= _pi ) )
30 26 29 mpbid 
 |-  ( x e. D -> ( Im ` ( log ` x ) ) =/= _pi )
31 30 necomd 
 |-  ( x e. D -> _pi =/= ( Im ` ( log ` x ) ) )
32 20 24 25 31 leneltd 
 |-  ( x e. D -> ( Im ` ( log ` x ) ) < _pi )
33 23 renegcli 
 |-  -u _pi e. RR
34 33 rexri 
 |-  -u _pi e. RR*
35 23 rexri 
 |-  _pi e. RR*
36 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 ) ) )
37 34 35 36 mp2an 
 |-  ( ( Im ` ( log ` x ) ) e. ( -u _pi (,) _pi ) <-> ( ( Im ` ( log ` x ) ) e. RR /\ -u _pi < ( Im ` ( log ` x ) ) /\ ( Im ` ( log ` x ) ) < _pi ) )
38 20 22 32 37 syl3anbrc 
 |-  ( x e. D -> ( Im ` ( log ` x ) ) e. ( -u _pi (,) _pi ) )
39 imf 
 |-  Im : CC --> RR
40 ffn 
 |-  ( Im : CC --> RR -> Im Fn CC )
41 elpreima 
 |-  ( Im Fn CC -> ( ( log ` x ) e. ( `' Im " ( -u _pi (,) _pi ) ) <-> ( ( log ` x ) e. CC /\ ( Im ` ( log ` x ) ) e. ( -u _pi (,) _pi ) ) ) )
42 39 40 41 mp2b 
 |-  ( ( log ` x ) e. ( `' Im " ( -u _pi (,) _pi ) ) <-> ( ( log ` x ) e. CC /\ ( Im ` ( log ` x ) ) e. ( -u _pi (,) _pi ) ) )
43 19 38 42 sylanbrc 
 |-  ( x e. D -> ( log ` x ) e. ( `' Im " ( -u _pi (,) _pi ) ) )
44 15 43 mprgbir 
 |-  ( log " D ) C_ ( `' Im " ( -u _pi (,) _pi ) )
45 elpreima 
 |-  ( Im Fn CC -> ( x e. ( `' Im " ( -u _pi (,) _pi ) ) <-> ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) ) )
46 39 40 45 mp2b 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) <-> ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) )
47 simpl 
 |-  ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) -> x e. CC )
48 eliooord 
 |-  ( ( Im ` x ) e. ( -u _pi (,) _pi ) -> ( -u _pi < ( Im ` x ) /\ ( Im ` x ) < _pi ) )
49 48 adantl 
 |-  ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) -> ( -u _pi < ( Im ` x ) /\ ( Im ` x ) < _pi ) )
50 49 simpld 
 |-  ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) -> -u _pi < ( Im ` x ) )
51 49 simprd 
 |-  ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) -> ( Im ` x ) < _pi )
52 imcl 
 |-  ( x e. CC -> ( Im ` x ) e. RR )
53 52 adantr 
 |-  ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) -> ( Im ` x ) e. RR )
54 ltle 
 |-  ( ( ( Im ` x ) e. RR /\ _pi e. RR ) -> ( ( Im ` x ) < _pi -> ( Im ` x ) <_ _pi ) )
55 53 23 54 sylancl 
 |-  ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) -> ( ( Im ` x ) < _pi -> ( Im ` x ) <_ _pi ) )
56 51 55 mpd 
 |-  ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) -> ( Im ` x ) <_ _pi )
57 ellogrn 
 |-  ( x e. ran log <-> ( x e. CC /\ -u _pi < ( Im ` x ) /\ ( Im ` x ) <_ _pi ) )
58 47 50 56 57 syl3anbrc 
 |-  ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) -> x e. ran log )
59 logef 
 |-  ( x e. ran log -> ( log ` ( exp ` x ) ) = x )
60 58 59 syl 
 |-  ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) -> ( log ` ( exp ` x ) ) = x )
61 efcl 
 |-  ( x e. CC -> ( exp ` x ) e. CC )
62 61 adantr 
 |-  ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) -> ( exp ` x ) e. CC )
63 53 adantr 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( Im ` x ) e. RR )
64 63 recnd 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( Im ` x ) e. CC )
65 picn 
 |-  _pi e. CC
66 65 a1i 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> _pi e. CC )
67 pipos 
 |-  0 < _pi
68 23 67 gt0ne0ii 
 |-  _pi =/= 0
69 68 a1i 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> _pi =/= 0 )
70 51 adantr 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( Im ` x ) < _pi )
71 65 mulridi 
 |-  ( _pi x. 1 ) = _pi
72 70 71 breqtrrdi 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( Im ` x ) < ( _pi x. 1 ) )
73 1re 
 |-  1 e. RR
74 73 a1i 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> 1 e. RR )
75 23 a1i 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> _pi e. RR )
76 67 a1i 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> 0 < _pi )
77 ltdivmul 
 |-  ( ( ( Im ` x ) e. RR /\ 1 e. RR /\ ( _pi e. RR /\ 0 < _pi ) ) -> ( ( ( Im ` x ) / _pi ) < 1 <-> ( Im ` x ) < ( _pi x. 1 ) ) )
78 63 74 75 76 77 syl112anc 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( ( ( Im ` x ) / _pi ) < 1 <-> ( Im ` x ) < ( _pi x. 1 ) ) )
79 72 78 mpbird 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( ( Im ` x ) / _pi ) < 1 )
80 1e0p1 
 |-  1 = ( 0 + 1 )
81 79 80 breqtrdi 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( ( Im ` x ) / _pi ) < ( 0 + 1 ) )
82 63 recoscld 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( cos ` ( Im ` x ) ) e. RR )
83 63 resincld 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( sin ` ( Im ` x ) ) e. RR )
84 82 83 crimd 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( Im ` ( ( cos ` ( Im ` x ) ) + ( _i x. ( sin ` ( Im ` x ) ) ) ) ) = ( sin ` ( Im ` x ) ) )
85 efeul 
 |-  ( x e. CC -> ( exp ` x ) = ( ( exp ` ( Re ` x ) ) x. ( ( cos ` ( Im ` x ) ) + ( _i x. ( sin ` ( Im ` x ) ) ) ) ) )
86 85 ad2antrr 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( exp ` x ) = ( ( exp ` ( Re ` x ) ) x. ( ( cos ` ( Im ` x ) ) + ( _i x. ( sin ` ( Im ` x ) ) ) ) ) )
87 86 oveq1d 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( ( exp ` x ) / ( exp ` ( Re ` x ) ) ) = ( ( ( exp ` ( Re ` x ) ) x. ( ( cos ` ( Im ` x ) ) + ( _i x. ( sin ` ( Im ` x ) ) ) ) ) / ( exp ` ( Re ` x ) ) ) )
88 82 recnd 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( cos ` ( Im ` x ) ) e. CC )
89 ax-icn 
 |-  _i e. CC
90 83 recnd 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( sin ` ( Im ` x ) ) e. CC )
91 mulcl 
 |-  ( ( _i e. CC /\ ( sin ` ( Im ` x ) ) e. CC ) -> ( _i x. ( sin ` ( Im ` x ) ) ) e. CC )
92 89 90 91 sylancr 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( _i x. ( sin ` ( Im ` x ) ) ) e. CC )
93 88 92 addcld 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( ( cos ` ( Im ` x ) ) + ( _i x. ( sin ` ( Im ` x ) ) ) ) e. CC )
94 recl 
 |-  ( x e. CC -> ( Re ` x ) e. RR )
95 94 ad2antrr 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( Re ` x ) e. RR )
96 95 recnd 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( Re ` x ) e. CC )
97 efcl 
 |-  ( ( Re ` x ) e. CC -> ( exp ` ( Re ` x ) ) e. CC )
98 96 97 syl 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( exp ` ( Re ` x ) ) e. CC )
99 efne0 
 |-  ( ( Re ` x ) e. CC -> ( exp ` ( Re ` x ) ) =/= 0 )
100 96 99 syl 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( exp ` ( Re ` x ) ) =/= 0 )
101 93 98 100 divcan3d 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( ( ( exp ` ( Re ` x ) ) x. ( ( cos ` ( Im ` x ) ) + ( _i x. ( sin ` ( Im ` x ) ) ) ) ) / ( exp ` ( Re ` x ) ) ) = ( ( cos ` ( Im ` x ) ) + ( _i x. ( sin ` ( Im ` x ) ) ) ) )
102 87 101 eqtrd 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( ( exp ` x ) / ( exp ` ( Re ` x ) ) ) = ( ( cos ` ( Im ` x ) ) + ( _i x. ( sin ` ( Im ` x ) ) ) ) )
103 simpr 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( exp ` x ) e. RR )
104 95 reefcld 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( exp ` ( Re ` x ) ) e. RR )
105 103 104 100 redivcld 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( ( exp ` x ) / ( exp ` ( Re ` x ) ) ) e. RR )
106 102 105 eqeltrrd 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( ( cos ` ( Im ` x ) ) + ( _i x. ( sin ` ( Im ` x ) ) ) ) e. RR )
107 106 reim0d 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( Im ` ( ( cos ` ( Im ` x ) ) + ( _i x. ( sin ` ( Im ` x ) ) ) ) ) = 0 )
108 84 107 eqtr3d 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( sin ` ( Im ` x ) ) = 0 )
109 sineq0 
 |-  ( ( Im ` x ) e. CC -> ( ( sin ` ( Im ` x ) ) = 0 <-> ( ( Im ` x ) / _pi ) e. ZZ ) )
110 64 109 syl 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( ( sin ` ( Im ` x ) ) = 0 <-> ( ( Im ` x ) / _pi ) e. ZZ ) )
111 108 110 mpbid 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( ( Im ` x ) / _pi ) e. ZZ )
112 0z 
 |-  0 e. ZZ
113 zleltp1 
 |-  ( ( ( ( Im ` x ) / _pi ) e. ZZ /\ 0 e. ZZ ) -> ( ( ( Im ` x ) / _pi ) <_ 0 <-> ( ( Im ` x ) / _pi ) < ( 0 + 1 ) ) )
114 111 112 113 sylancl 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( ( ( Im ` x ) / _pi ) <_ 0 <-> ( ( Im ` x ) / _pi ) < ( 0 + 1 ) ) )
115 81 114 mpbird 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( ( Im ` x ) / _pi ) <_ 0 )
116 df-neg 
 |-  -u 1 = ( 0 - 1 )
117 65 mulm1i 
 |-  ( -u 1 x. _pi ) = -u _pi
118 50 adantr 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> -u _pi < ( Im ` x ) )
119 117 118 eqbrtrid 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( -u 1 x. _pi ) < ( Im ` x ) )
120 73 renegcli 
 |-  -u 1 e. RR
121 120 a1i 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> -u 1 e. RR )
122 ltmuldiv 
 |-  ( ( -u 1 e. RR /\ ( Im ` x ) e. RR /\ ( _pi e. RR /\ 0 < _pi ) ) -> ( ( -u 1 x. _pi ) < ( Im ` x ) <-> -u 1 < ( ( Im ` x ) / _pi ) ) )
123 121 63 75 76 122 syl112anc 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( ( -u 1 x. _pi ) < ( Im ` x ) <-> -u 1 < ( ( Im ` x ) / _pi ) ) )
124 119 123 mpbid 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> -u 1 < ( ( Im ` x ) / _pi ) )
125 116 124 eqbrtrrid 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( 0 - 1 ) < ( ( Im ` x ) / _pi ) )
126 zlem1lt 
 |-  ( ( 0 e. ZZ /\ ( ( Im ` x ) / _pi ) e. ZZ ) -> ( 0 <_ ( ( Im ` x ) / _pi ) <-> ( 0 - 1 ) < ( ( Im ` x ) / _pi ) ) )
127 112 111 126 sylancr 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( 0 <_ ( ( Im ` x ) / _pi ) <-> ( 0 - 1 ) < ( ( Im ` x ) / _pi ) ) )
128 125 127 mpbird 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> 0 <_ ( ( Im ` x ) / _pi ) )
129 63 75 69 redivcld 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( ( Im ` x ) / _pi ) e. RR )
130 0re 
 |-  0 e. RR
131 letri3 
 |-  ( ( ( ( Im ` x ) / _pi ) e. RR /\ 0 e. RR ) -> ( ( ( Im ` x ) / _pi ) = 0 <-> ( ( ( Im ` x ) / _pi ) <_ 0 /\ 0 <_ ( ( Im ` x ) / _pi ) ) ) )
132 129 130 131 sylancl 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( ( ( Im ` x ) / _pi ) = 0 <-> ( ( ( Im ` x ) / _pi ) <_ 0 /\ 0 <_ ( ( Im ` x ) / _pi ) ) ) )
133 115 128 132 mpbir2and 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( ( Im ` x ) / _pi ) = 0 )
134 64 66 69 133 diveq0d 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( Im ` x ) = 0 )
135 reim0b 
 |-  ( x e. CC -> ( x e. RR <-> ( Im ` x ) = 0 ) )
136 135 ad2antrr 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( x e. RR <-> ( Im ` x ) = 0 ) )
137 134 136 mpbird 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> x e. RR )
138 137 rpefcld 
 |-  ( ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) /\ ( exp ` x ) e. RR ) -> ( exp ` x ) e. RR+ )
139 138 ex 
 |-  ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) -> ( ( exp ` x ) e. RR -> ( exp ` x ) e. RR+ ) )
140 1 ellogdm 
 |-  ( ( exp ` x ) e. D <-> ( ( exp ` x ) e. CC /\ ( ( exp ` x ) e. RR -> ( exp ` x ) e. RR+ ) ) )
141 62 139 140 sylanbrc 
 |-  ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) -> ( exp ` x ) e. D )
142 funfvima2 
 |-  ( ( Fun log /\ D C_ dom log ) -> ( ( exp ` x ) e. D -> ( log ` ( exp ` x ) ) e. ( log " D ) ) )
143 9 13 142 mp2an 
 |-  ( ( exp ` x ) e. D -> ( log ` ( exp ` x ) ) e. ( log " D ) )
144 141 143 syl 
 |-  ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) -> ( log ` ( exp ` x ) ) e. ( log " D ) )
145 60 144 eqeltrrd 
 |-  ( ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) -> x e. ( log " D ) )
146 46 145 sylbi 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) -> x e. ( log " D ) )
147 146 ssriv 
 |-  ( `' Im " ( -u _pi (,) _pi ) ) C_ ( log " D )
148 44 147 eqssi 
 |-  ( log " D ) = ( `' Im " ( -u _pi (,) _pi ) )
149 f1oeq3 
 |-  ( ( log " D ) = ( `' Im " ( -u _pi (,) _pi ) ) -> ( ( log |` D ) : D -1-1-onto-> ( log " D ) <-> ( log |` D ) : D -1-1-onto-> ( `' Im " ( -u _pi (,) _pi ) ) ) )
150 148 149 ax-mp 
 |-  ( ( log |` D ) : D -1-1-onto-> ( log " D ) <-> ( log |` D ) : D -1-1-onto-> ( `' Im " ( -u _pi (,) _pi ) ) )
151 7 150 mpbi 
 |-  ( log |` D ) : D -1-1-onto-> ( `' Im " ( -u _pi (,) _pi ) )