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