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 ffvelrni
 |-  ( 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 ffvelrni
 |-  ( ( 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 ffvelrnd
 |-  ( ( 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 } ) )