Metamath Proof Explorer

Theorem eff1olem

Description: The exponential function maps the set S , of complex numbers with imaginary part in a real interval of length 2 x. _pi , one-to-one onto the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008) (Proof shortened by Mario Carneiro, 13-May-2014)

Ref Expression
Hypotheses eff1olem.1 
|- F = ( w e. D |-> ( exp ` ( _i x. w ) ) )
eff1olem.2 
|- S = ( `' Im " D )
eff1olem.3 
|- ( ph -> D C_ RR )
eff1olem.4 
|- ( ( ph /\ ( x e. D /\ y e. D ) ) -> ( abs ` ( x - y ) ) < ( 2 x. _pi ) )
eff1olem.5 
|- ( ( ph /\ z e. RR ) -> E. y e. D ( ( z - y ) / ( 2 x. _pi ) ) e. ZZ )
Assertion eff1olem 
|- ( ph -> ( exp |` S ) : S -1-1-onto-> ( CC \ { 0 } ) )

Proof

Step Hyp Ref Expression
1 eff1olem.1 
 |-  F = ( w e. D |-> ( exp ` ( _i x. w ) ) )
2 eff1olem.2 
 |-  S = ( `' Im " D )
3 eff1olem.3 
 |-  ( ph -> D C_ RR )
4 eff1olem.4 
 |-  ( ( ph /\ ( x e. D /\ y e. D ) ) -> ( abs ` ( x - y ) ) < ( 2 x. _pi ) )
5 eff1olem.5 
 |-  ( ( ph /\ z e. RR ) -> E. y e. D ( ( z - y ) / ( 2 x. _pi ) ) e. ZZ )
6 cnvimass 
 |-  ( `' Im " D ) C_ dom Im
7 imf 
 |-  Im : CC --> RR
8 7 fdmi 
 |-  dom Im = CC
9 8 eqcomi 
 |-  CC = dom Im
10 6 2 9 3sstr4i 
 |-  S C_ CC
11 eff2 
 |-  exp : CC --> ( CC \ { 0 } )
12 11 a1i 
 |-  ( S C_ CC -> exp : CC --> ( CC \ { 0 } ) )
13 12 feqmptd 
 |-  ( S C_ CC -> exp = ( y e. CC |-> ( exp ` y ) ) )
14 13 reseq1d 
 |-  ( S C_ CC -> ( exp |` S ) = ( ( y e. CC |-> ( exp ` y ) ) |` S ) )
15 resmpt 
 |-  ( S C_ CC -> ( ( y e. CC |-> ( exp ` y ) ) |` S ) = ( y e. S |-> ( exp ` y ) ) )
16 14 15 eqtrd 
 |-  ( S C_ CC -> ( exp |` S ) = ( y e. S |-> ( exp ` y ) ) )
17 10 16 ax-mp 
 |-  ( exp |` S ) = ( y e. S |-> ( exp ` y ) )
18 10 sseli 
 |-  ( y e. S -> y e. CC )
19 11 ffvelcdmi 
 |-  ( y e. CC -> ( exp ` y ) e. ( CC \ { 0 } ) )
20 18 19 syl 
 |-  ( y e. S -> ( exp ` y ) e. ( CC \ { 0 } ) )
21 20 adantl 
 |-  ( ( ph /\ y e. S ) -> ( exp ` y ) e. ( CC \ { 0 } ) )
22 simpr 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> x e. ( CC \ { 0 } ) )
23 eldifsn 
 |-  ( x e. ( CC \ { 0 } ) <-> ( x e. CC /\ x =/= 0 ) )
24 22 23 sylib 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( x e. CC /\ x =/= 0 ) )
25 24 simpld 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> x e. CC )
26 24 simprd 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> x =/= 0 )
27 25 26 absrpcld 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( abs ` x ) e. RR+ )
28 reeff1o 
 |-  ( exp |` RR ) : RR -1-1-onto-> RR+
29 f1ocnv 
 |-  ( ( exp |` RR ) : RR -1-1-onto-> RR+ -> `' ( exp |` RR ) : RR+ -1-1-onto-> RR )
30 f1of 
 |-  ( `' ( exp |` RR ) : RR+ -1-1-onto-> RR -> `' ( exp |` RR ) : RR+ --> RR )
31 28 29 30 mp2b 
 |-  `' ( exp |` RR ) : RR+ --> RR
32 31 ffvelcdmi 
 |-  ( ( abs ` x ) e. RR+ -> ( `' ( exp |` RR ) ` ( abs ` x ) ) e. RR )
33 27 32 syl 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( `' ( exp |` RR ) ` ( abs ` x ) ) e. RR )
34 33 recnd 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( `' ( exp |` RR ) ` ( abs ` x ) ) e. CC )
35 ax-icn 
 |-  _i e. CC
36 3 adantr 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> D C_ RR )
37 eqid 
 |-  ( `' abs " { 1 } ) = ( `' abs " { 1 } )
38 eqid 
 |-  ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) = ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
39 1 37 3 4 5 38 efif1olem4 
 |-  ( ph -> F : D -1-1-onto-> ( `' abs " { 1 } ) )
40 f1ocnv 
 |-  ( F : D -1-1-onto-> ( `' abs " { 1 } ) -> `' F : ( `' abs " { 1 } ) -1-1-onto-> D )
41 f1of 
 |-  ( `' F : ( `' abs " { 1 } ) -1-1-onto-> D -> `' F : ( `' abs " { 1 } ) --> D )
42 39 40 41 3syl 
 |-  ( ph -> `' F : ( `' abs " { 1 } ) --> D )
43 42 adantr 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> `' F : ( `' abs " { 1 } ) --> D )
44 25 abscld 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( abs ` x ) e. RR )
45 44 recnd 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( abs ` x ) e. CC )
46 25 26 absne0d 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( abs ` x ) =/= 0 )
47 25 45 46 divcld 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( x / ( abs ` x ) ) e. CC )
48 25 45 46 absdivd 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( abs ` ( x / ( abs ` x ) ) ) = ( ( abs ` x ) / ( abs ` ( abs ` x ) ) ) )
49 absidm 
 |-  ( x e. CC -> ( abs ` ( abs ` x ) ) = ( abs ` x ) )
50 25 49 syl 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( abs ` ( abs ` x ) ) = ( abs ` x ) )
51 50 oveq2d 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( ( abs ` x ) / ( abs ` ( abs ` x ) ) ) = ( ( abs ` x ) / ( abs ` x ) ) )
52 45 46 dividd 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( ( abs ` x ) / ( abs ` x ) ) = 1 )
53 48 51 52 3eqtrd 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( abs ` ( x / ( abs ` x ) ) ) = 1 )
54 absf 
 |-  abs : CC --> RR
55 ffn 
 |-  ( abs : CC --> RR -> abs Fn CC )
56 fniniseg 
 |-  ( abs Fn CC -> ( ( x / ( abs ` x ) ) e. ( `' abs " { 1 } ) <-> ( ( x / ( abs ` x ) ) e. CC /\ ( abs ` ( x / ( abs ` x ) ) ) = 1 ) ) )
57 54 55 56 mp2b 
 |-  ( ( x / ( abs ` x ) ) e. ( `' abs " { 1 } ) <-> ( ( x / ( abs ` x ) ) e. CC /\ ( abs ` ( x / ( abs ` x ) ) ) = 1 ) )
58 47 53 57 sylanbrc 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( x / ( abs ` x ) ) e. ( `' abs " { 1 } ) )
59 43 58 ffvelcdmd 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( `' F ` ( x / ( abs ` x ) ) ) e. D )
60 36 59 sseldd 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( `' F ` ( x / ( abs ` x ) ) ) e. RR )
61 60 recnd 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( `' F ` ( x / ( abs ` x ) ) ) e. CC )
62 mulcl 
 |-  ( ( _i e. CC /\ ( `' F ` ( x / ( abs ` x ) ) ) e. CC ) -> ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) e. CC )
63 35 61 62 sylancr 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) e. CC )
64 34 63 addcld 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( ( `' ( exp |` RR ) ` ( abs ` x ) ) + ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) e. CC )
65 33 60 crimd 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( Im ` ( ( `' ( exp |` RR ) ` ( abs ` x ) ) + ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) ) = ( `' F ` ( x / ( abs ` x ) ) ) )
66 65 59 eqeltrd 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( Im ` ( ( `' ( exp |` RR ) ` ( abs ` x ) ) + ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) ) e. D )
67 ffn 
 |-  ( Im : CC --> RR -> Im Fn CC )
68 elpreima 
 |-  ( Im Fn CC -> ( ( ( `' ( exp |` RR ) ` ( abs ` x ) ) + ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) e. ( `' Im " D ) <-> ( ( ( `' ( exp |` RR ) ` ( abs ` x ) ) + ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) e. CC /\ ( Im ` ( ( `' ( exp |` RR ) ` ( abs ` x ) ) + ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) ) e. D ) ) )
69 7 67 68 mp2b 
 |-  ( ( ( `' ( exp |` RR ) ` ( abs ` x ) ) + ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) e. ( `' Im " D ) <-> ( ( ( `' ( exp |` RR ) ` ( abs ` x ) ) + ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) e. CC /\ ( Im ` ( ( `' ( exp |` RR ) ` ( abs ` x ) ) + ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) ) e. D ) )
70 64 66 69 sylanbrc 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( ( `' ( exp |` RR ) ` ( abs ` x ) ) + ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) e. ( `' Im " D ) )
71 70 2 eleqtrrdi 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( ( `' ( exp |` RR ) ` ( abs ` x ) ) + ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) e. S )
72 efadd 
 |-  ( ( ( `' ( exp |` RR ) ` ( abs ` x ) ) e. CC /\ ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) e. CC ) -> ( exp ` ( ( `' ( exp |` RR ) ` ( abs ` x ) ) + ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) ) = ( ( exp ` ( `' ( exp |` RR ) ` ( abs ` x ) ) ) x. ( exp ` ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) ) )
73 34 63 72 syl2anc 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( exp ` ( ( `' ( exp |` RR ) ` ( abs ` x ) ) + ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) ) = ( ( exp ` ( `' ( exp |` RR ) ` ( abs ` x ) ) ) x. ( exp ` ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) ) )
74 33 fvresd 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( ( exp |` RR ) ` ( `' ( exp |` RR ) ` ( abs ` x ) ) ) = ( exp ` ( `' ( exp |` RR ) ` ( abs ` x ) ) ) )
75 f1ocnvfv2 
 |-  ( ( ( exp |` RR ) : RR -1-1-onto-> RR+ /\ ( abs ` x ) e. RR+ ) -> ( ( exp |` RR ) ` ( `' ( exp |` RR ) ` ( abs ` x ) ) ) = ( abs ` x ) )
76 28 27 75 sylancr 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( ( exp |` RR ) ` ( `' ( exp |` RR ) ` ( abs ` x ) ) ) = ( abs ` x ) )
77 74 76 eqtr3d 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( exp ` ( `' ( exp |` RR ) ` ( abs ` x ) ) ) = ( abs ` x ) )
78 oveq2 
 |-  ( z = ( `' F ` ( x / ( abs ` x ) ) ) -> ( _i x. z ) = ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) )
79 78 fveq2d 
 |-  ( z = ( `' F ` ( x / ( abs ` x ) ) ) -> ( exp ` ( _i x. z ) ) = ( exp ` ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) )
80 oveq2 
 |-  ( w = z -> ( _i x. w ) = ( _i x. z ) )
81 80 fveq2d 
 |-  ( w = z -> ( exp ` ( _i x. w ) ) = ( exp ` ( _i x. z ) ) )
82 81 cbvmptv 
 |-  ( w e. D |-> ( exp ` ( _i x. w ) ) ) = ( z e. D |-> ( exp ` ( _i x. z ) ) )
83 1 82 eqtri 
 |-  F = ( z e. D |-> ( exp ` ( _i x. z ) ) )
84 fvex 
 |-  ( exp ` ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) e. _V
85 79 83 84 fvmpt 
 |-  ( ( `' F ` ( x / ( abs ` x ) ) ) e. D -> ( F ` ( `' F ` ( x / ( abs ` x ) ) ) ) = ( exp ` ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) )
86 59 85 syl 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( F ` ( `' F ` ( x / ( abs ` x ) ) ) ) = ( exp ` ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) )
87 39 adantr 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> F : D -1-1-onto-> ( `' abs " { 1 } ) )
88 f1ocnvfv2 
 |-  ( ( F : D -1-1-onto-> ( `' abs " { 1 } ) /\ ( x / ( abs ` x ) ) e. ( `' abs " { 1 } ) ) -> ( F ` ( `' F ` ( x / ( abs ` x ) ) ) ) = ( x / ( abs ` x ) ) )
89 87 58 88 syl2anc 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( F ` ( `' F ` ( x / ( abs ` x ) ) ) ) = ( x / ( abs ` x ) ) )
90 86 89 eqtr3d 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( exp ` ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) = ( x / ( abs ` x ) ) )
91 77 90 oveq12d 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( ( exp ` ( `' ( exp |` RR ) ` ( abs ` x ) ) ) x. ( exp ` ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) ) = ( ( abs ` x ) x. ( x / ( abs ` x ) ) ) )
92 25 45 46 divcan2d 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( ( abs ` x ) x. ( x / ( abs ` x ) ) ) = x )
93 73 91 92 3eqtrrd 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> x = ( exp ` ( ( `' ( exp |` RR ) ` ( abs ` x ) ) + ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) ) )
94 93 adantrl 
 |-  ( ( ph /\ ( y e. S /\ x e. ( CC \ { 0 } ) ) ) -> x = ( exp ` ( ( `' ( exp |` RR ) ` ( abs ` x ) ) + ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) ) )
95 fveq2 
 |-  ( y = ( ( `' ( exp |` RR ) ` ( abs ` x ) ) + ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) -> ( exp ` y ) = ( exp ` ( ( `' ( exp |` RR ) ` ( abs ` x ) ) + ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) ) )
96 95 eqeq2d 
 |-  ( y = ( ( `' ( exp |` RR ) ` ( abs ` x ) ) + ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) -> ( x = ( exp ` y ) <-> x = ( exp ` ( ( `' ( exp |` RR ) ` ( abs ` x ) ) + ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) ) ) )
97 94 96 syl5ibrcom 
 |-  ( ( ph /\ ( y e. S /\ x e. ( CC \ { 0 } ) ) ) -> ( y = ( ( `' ( exp |` RR ) ` ( abs ` x ) ) + ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) -> x = ( exp ` y ) ) )
98 18 adantl 
 |-  ( ( ph /\ y e. S ) -> y e. CC )
99 98 replimd 
 |-  ( ( ph /\ y e. S ) -> y = ( ( Re ` y ) + ( _i x. ( Im ` y ) ) ) )
100 absef 
 |-  ( y e. CC -> ( abs ` ( exp ` y ) ) = ( exp ` ( Re ` y ) ) )
101 98 100 syl 
 |-  ( ( ph /\ y e. S ) -> ( abs ` ( exp ` y ) ) = ( exp ` ( Re ` y ) ) )
102 98 recld 
 |-  ( ( ph /\ y e. S ) -> ( Re ` y ) e. RR )
103 102 fvresd 
 |-  ( ( ph /\ y e. S ) -> ( ( exp |` RR ) ` ( Re ` y ) ) = ( exp ` ( Re ` y ) ) )
104 101 103 eqtr4d 
 |-  ( ( ph /\ y e. S ) -> ( abs ` ( exp ` y ) ) = ( ( exp |` RR ) ` ( Re ` y ) ) )
105 104 fveq2d 
 |-  ( ( ph /\ y e. S ) -> ( `' ( exp |` RR ) ` ( abs ` ( exp ` y ) ) ) = ( `' ( exp |` RR ) ` ( ( exp |` RR ) ` ( Re ` y ) ) ) )
106 f1ocnvfv1 
 |-  ( ( ( exp |` RR ) : RR -1-1-onto-> RR+ /\ ( Re ` y ) e. RR ) -> ( `' ( exp |` RR ) ` ( ( exp |` RR ) ` ( Re ` y ) ) ) = ( Re ` y ) )
107 28 102 106 sylancr 
 |-  ( ( ph /\ y e. S ) -> ( `' ( exp |` RR ) ` ( ( exp |` RR ) ` ( Re ` y ) ) ) = ( Re ` y ) )
108 105 107 eqtrd 
 |-  ( ( ph /\ y e. S ) -> ( `' ( exp |` RR ) ` ( abs ` ( exp ` y ) ) ) = ( Re ` y ) )
109 98 imcld 
 |-  ( ( ph /\ y e. S ) -> ( Im ` y ) e. RR )
110 109 recnd 
 |-  ( ( ph /\ y e. S ) -> ( Im ` y ) e. CC )
111 mulcl 
 |-  ( ( _i e. CC /\ ( Im ` y ) e. CC ) -> ( _i x. ( Im ` y ) ) e. CC )
112 35 110 111 sylancr 
 |-  ( ( ph /\ y e. S ) -> ( _i x. ( Im ` y ) ) e. CC )
113 efcl 
 |-  ( ( _i x. ( Im ` y ) ) e. CC -> ( exp ` ( _i x. ( Im ` y ) ) ) e. CC )
114 112 113 syl 
 |-  ( ( ph /\ y e. S ) -> ( exp ` ( _i x. ( Im ` y ) ) ) e. CC )
115 102 recnd 
 |-  ( ( ph /\ y e. S ) -> ( Re ` y ) e. CC )
116 efcl 
 |-  ( ( Re ` y ) e. CC -> ( exp ` ( Re ` y ) ) e. CC )
117 115 116 syl 
 |-  ( ( ph /\ y e. S ) -> ( exp ` ( Re ` y ) ) e. CC )
118 efne0 
 |-  ( ( Re ` y ) e. CC -> ( exp ` ( Re ` y ) ) =/= 0 )
119 115 118 syl 
 |-  ( ( ph /\ y e. S ) -> ( exp ` ( Re ` y ) ) =/= 0 )
120 114 117 119 divcan3d 
 |-  ( ( ph /\ y e. S ) -> ( ( ( exp ` ( Re ` y ) ) x. ( exp ` ( _i x. ( Im ` y ) ) ) ) / ( exp ` ( Re ` y ) ) ) = ( exp ` ( _i x. ( Im ` y ) ) ) )
121 99 fveq2d 
 |-  ( ( ph /\ y e. S ) -> ( exp ` y ) = ( exp ` ( ( Re ` y ) + ( _i x. ( Im ` y ) ) ) ) )
122 efadd 
 |-  ( ( ( Re ` y ) e. CC /\ ( _i x. ( Im ` y ) ) e. CC ) -> ( exp ` ( ( Re ` y ) + ( _i x. ( Im ` y ) ) ) ) = ( ( exp ` ( Re ` y ) ) x. ( exp ` ( _i x. ( Im ` y ) ) ) ) )
123 115 112 122 syl2anc 
 |-  ( ( ph /\ y e. S ) -> ( exp ` ( ( Re ` y ) + ( _i x. ( Im ` y ) ) ) ) = ( ( exp ` ( Re ` y ) ) x. ( exp ` ( _i x. ( Im ` y ) ) ) ) )
124 121 123 eqtrd 
 |-  ( ( ph /\ y e. S ) -> ( exp ` y ) = ( ( exp ` ( Re ` y ) ) x. ( exp ` ( _i x. ( Im ` y ) ) ) ) )
125 124 101 oveq12d 
 |-  ( ( ph /\ y e. S ) -> ( ( exp ` y ) / ( abs ` ( exp ` y ) ) ) = ( ( ( exp ` ( Re ` y ) ) x. ( exp ` ( _i x. ( Im ` y ) ) ) ) / ( exp ` ( Re ` y ) ) ) )
126 elpreima 
 |-  ( Im Fn CC -> ( y e. ( `' Im " D ) <-> ( y e. CC /\ ( Im ` y ) e. D ) ) )
127 7 67 126 mp2b 
 |-  ( y e. ( `' Im " D ) <-> ( y e. CC /\ ( Im ` y ) e. D ) )
128 127 simprbi 
 |-  ( y e. ( `' Im " D ) -> ( Im ` y ) e. D )
129 128 2 eleq2s 
 |-  ( y e. S -> ( Im ` y ) e. D )
130 129 adantl 
 |-  ( ( ph /\ y e. S ) -> ( Im ` y ) e. D )
131 oveq2 
 |-  ( w = ( Im ` y ) -> ( _i x. w ) = ( _i x. ( Im ` y ) ) )
132 131 fveq2d 
 |-  ( w = ( Im ` y ) -> ( exp ` ( _i x. w ) ) = ( exp ` ( _i x. ( Im ` y ) ) ) )
133 fvex 
 |-  ( exp ` ( _i x. ( Im ` y ) ) ) e. _V
134 132 1 133 fvmpt 
 |-  ( ( Im ` y ) e. D -> ( F ` ( Im ` y ) ) = ( exp ` ( _i x. ( Im ` y ) ) ) )
135 130 134 syl 
 |-  ( ( ph /\ y e. S ) -> ( F ` ( Im ` y ) ) = ( exp ` ( _i x. ( Im ` y ) ) ) )
136 120 125 135 3eqtr4d 
 |-  ( ( ph /\ y e. S ) -> ( ( exp ` y ) / ( abs ` ( exp ` y ) ) ) = ( F ` ( Im ` y ) ) )
137 136 fveq2d 
 |-  ( ( ph /\ y e. S ) -> ( `' F ` ( ( exp ` y ) / ( abs ` ( exp ` y ) ) ) ) = ( `' F ` ( F ` ( Im ` y ) ) ) )
138 f1ocnvfv1 
 |-  ( ( F : D -1-1-onto-> ( `' abs " { 1 } ) /\ ( Im ` y ) e. D ) -> ( `' F ` ( F ` ( Im ` y ) ) ) = ( Im ` y ) )
139 39 129 138 syl2an 
 |-  ( ( ph /\ y e. S ) -> ( `' F ` ( F ` ( Im ` y ) ) ) = ( Im ` y ) )
140 137 139 eqtrd 
 |-  ( ( ph /\ y e. S ) -> ( `' F ` ( ( exp ` y ) / ( abs ` ( exp ` y ) ) ) ) = ( Im ` y ) )
141 140 oveq2d 
 |-  ( ( ph /\ y e. S ) -> ( _i x. ( `' F ` ( ( exp ` y ) / ( abs ` ( exp ` y ) ) ) ) ) = ( _i x. ( Im ` y ) ) )
142 108 141 oveq12d 
 |-  ( ( ph /\ y e. S ) -> ( ( `' ( exp |` RR ) ` ( abs ` ( exp ` y ) ) ) + ( _i x. ( `' F ` ( ( exp ` y ) / ( abs ` ( exp ` y ) ) ) ) ) ) = ( ( Re ` y ) + ( _i x. ( Im ` y ) ) ) )
143 99 142 eqtr4d 
 |-  ( ( ph /\ y e. S ) -> y = ( ( `' ( exp |` RR ) ` ( abs ` ( exp ` y ) ) ) + ( _i x. ( `' F ` ( ( exp ` y ) / ( abs ` ( exp ` y ) ) ) ) ) ) )
144 fveq2 
 |-  ( x = ( exp ` y ) -> ( abs ` x ) = ( abs ` ( exp ` y ) ) )
145 144 fveq2d 
 |-  ( x = ( exp ` y ) -> ( `' ( exp |` RR ) ` ( abs ` x ) ) = ( `' ( exp |` RR ) ` ( abs ` ( exp ` y ) ) ) )
146 id 
 |-  ( x = ( exp ` y ) -> x = ( exp ` y ) )
147 146 144 oveq12d 
 |-  ( x = ( exp ` y ) -> ( x / ( abs ` x ) ) = ( ( exp ` y ) / ( abs ` ( exp ` y ) ) ) )
148 147 fveq2d 
 |-  ( x = ( exp ` y ) -> ( `' F ` ( x / ( abs ` x ) ) ) = ( `' F ` ( ( exp ` y ) / ( abs ` ( exp ` y ) ) ) ) )
149 148 oveq2d 
 |-  ( x = ( exp ` y ) -> ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) = ( _i x. ( `' F ` ( ( exp ` y ) / ( abs ` ( exp ` y ) ) ) ) ) )
150 145 149 oveq12d 
 |-  ( x = ( exp ` y ) -> ( ( `' ( exp |` RR ) ` ( abs ` x ) ) + ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) = ( ( `' ( exp |` RR ) ` ( abs ` ( exp ` y ) ) ) + ( _i x. ( `' F ` ( ( exp ` y ) / ( abs ` ( exp ` y ) ) ) ) ) ) )
151 150 eqeq2d 
 |-  ( x = ( exp ` y ) -> ( y = ( ( `' ( exp |` RR ) ` ( abs ` x ) ) + ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) <-> y = ( ( `' ( exp |` RR ) ` ( abs ` ( exp ` y ) ) ) + ( _i x. ( `' F ` ( ( exp ` y ) / ( abs ` ( exp ` y ) ) ) ) ) ) ) )
152 143 151 syl5ibrcom 
 |-  ( ( ph /\ y e. S ) -> ( x = ( exp ` y ) -> y = ( ( `' ( exp |` RR ) ` ( abs ` x ) ) + ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) ) )
153 152 adantrr 
 |-  ( ( ph /\ ( y e. S /\ x e. ( CC \ { 0 } ) ) ) -> ( x = ( exp ` y ) -> y = ( ( `' ( exp |` RR ) ` ( abs ` x ) ) + ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) ) )
154 97 153 impbid 
 |-  ( ( ph /\ ( y e. S /\ x e. ( CC \ { 0 } ) ) ) -> ( y = ( ( `' ( exp |` RR ) ` ( abs ` x ) ) + ( _i x. ( `' F ` ( x / ( abs ` x ) ) ) ) ) <-> x = ( exp ` y ) ) )
155 17 21 71 154 f1o2d 
 |-  ( ph -> ( exp |` S ) : S -1-1-onto-> ( CC \ { 0 } ) )