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 } ) ) |