Metamath Proof Explorer

Theorem efif1olem4

Description: The exponential function of an imaginary number maps any interval of length 2 _pi one-to-one onto the unit circle. (Contributed by Paul Chapman, 16-Mar-2008) (Proof shortened by Mario Carneiro, 13-May-2014)

Ref Expression
Hypotheses efif1o.1 
|- F = ( w e. D |-> ( exp ` ( _i x. w ) ) )
efif1o.2 
|- C = ( `' abs " { 1 } )
efif1olem4.3 
|- ( ph -> D C_ RR )
efif1olem4.4 
|- ( ( ph /\ ( x e. D /\ y e. D ) ) -> ( abs ` ( x - y ) ) < ( 2 x. _pi ) )
efif1olem4.5 
|- ( ( ph /\ z e. RR ) -> E. y e. D ( ( z - y ) / ( 2 x. _pi ) ) e. ZZ )
efif1olem4.6 
|- S = ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
Assertion efif1olem4 
|- ( ph -> F : D -1-1-onto-> C )

Proof

Step Hyp Ref Expression
1 efif1o.1 
 |-  F = ( w e. D |-> ( exp ` ( _i x. w ) ) )
2 efif1o.2 
 |-  C = ( `' abs " { 1 } )
3 efif1olem4.3 
 |-  ( ph -> D C_ RR )
4 efif1olem4.4 
 |-  ( ( ph /\ ( x e. D /\ y e. D ) ) -> ( abs ` ( x - y ) ) < ( 2 x. _pi ) )
5 efif1olem4.5 
 |-  ( ( ph /\ z e. RR ) -> E. y e. D ( ( z - y ) / ( 2 x. _pi ) ) e. ZZ )
6 efif1olem4.6 
 |-  S = ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
7 3 sselda 
 |-  ( ( ph /\ w e. D ) -> w e. RR )
8 ax-icn 
 |-  _i e. CC
9 recn 
 |-  ( w e. RR -> w e. CC )
10 mulcl 
 |-  ( ( _i e. CC /\ w e. CC ) -> ( _i x. w ) e. CC )
11 8 9 10 sylancr 
 |-  ( w e. RR -> ( _i x. w ) e. CC )
12 efcl 
 |-  ( ( _i x. w ) e. CC -> ( exp ` ( _i x. w ) ) e. CC )
13 11 12 syl 
 |-  ( w e. RR -> ( exp ` ( _i x. w ) ) e. CC )
14 absefi 
 |-  ( w e. RR -> ( abs ` ( exp ` ( _i x. w ) ) ) = 1 )
15 absf 
 |-  abs : CC --> RR
16 ffn 
 |-  ( abs : CC --> RR -> abs Fn CC )
17 15 16 ax-mp 
 |-  abs Fn CC
18 fniniseg 
 |-  ( abs Fn CC -> ( ( exp ` ( _i x. w ) ) e. ( `' abs " { 1 } ) <-> ( ( exp ` ( _i x. w ) ) e. CC /\ ( abs ` ( exp ` ( _i x. w ) ) ) = 1 ) ) )
19 17 18 ax-mp 
 |-  ( ( exp ` ( _i x. w ) ) e. ( `' abs " { 1 } ) <-> ( ( exp ` ( _i x. w ) ) e. CC /\ ( abs ` ( exp ` ( _i x. w ) ) ) = 1 ) )
20 13 14 19 sylanbrc 
 |-  ( w e. RR -> ( exp ` ( _i x. w ) ) e. ( `' abs " { 1 } ) )
21 20 2 eleqtrrdi 
 |-  ( w e. RR -> ( exp ` ( _i x. w ) ) e. C )
22 7 21 syl 
 |-  ( ( ph /\ w e. D ) -> ( exp ` ( _i x. w ) ) e. C )
23 22 1 fmptd 
 |-  ( ph -> F : D --> C )
24 3 ad2antrr 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> D C_ RR )
25 simplrl 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> x e. D )
26 24 25 sseldd 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> x e. RR )
27 26 recnd 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> x e. CC )
28 simplrr 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> y e. D )
29 24 28 sseldd 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> y e. RR )
30 29 recnd 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> y e. CC )
31 27 30 subcld 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( x - y ) e. CC )
32 2re 
 |-  2 e. RR
33 pire 
 |-  _pi e. RR
34 32 33 remulcli 
 |-  ( 2 x. _pi ) e. RR
35 34 recni 
 |-  ( 2 x. _pi ) e. CC
36 2pos 
 |-  0 < 2
37 pipos 
 |-  0 < _pi
38 32 33 36 37 mulgt0ii 
 |-  0 < ( 2 x. _pi )
39 34 38 gt0ne0ii 
 |-  ( 2 x. _pi ) =/= 0
40 divcl 
 |-  ( ( ( x - y ) e. CC /\ ( 2 x. _pi ) e. CC /\ ( 2 x. _pi ) =/= 0 ) -> ( ( x - y ) / ( 2 x. _pi ) ) e. CC )
41 35 39 40 mp3an23 
 |-  ( ( x - y ) e. CC -> ( ( x - y ) / ( 2 x. _pi ) ) e. CC )
42 31 41 syl 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( ( x - y ) / ( 2 x. _pi ) ) e. CC )
43 absdiv 
 |-  ( ( ( x - y ) e. CC /\ ( 2 x. _pi ) e. CC /\ ( 2 x. _pi ) =/= 0 ) -> ( abs ` ( ( x - y ) / ( 2 x. _pi ) ) ) = ( ( abs ` ( x - y ) ) / ( abs ` ( 2 x. _pi ) ) ) )
44 35 39 43 mp3an23 
 |-  ( ( x - y ) e. CC -> ( abs ` ( ( x - y ) / ( 2 x. _pi ) ) ) = ( ( abs ` ( x - y ) ) / ( abs ` ( 2 x. _pi ) ) ) )
45 31 44 syl 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( abs ` ( ( x - y ) / ( 2 x. _pi ) ) ) = ( ( abs ` ( x - y ) ) / ( abs ` ( 2 x. _pi ) ) ) )
46 0re 
 |-  0 e. RR
47 46 34 38 ltleii 
 |-  0 <_ ( 2 x. _pi )
48 absid 
 |-  ( ( ( 2 x. _pi ) e. RR /\ 0 <_ ( 2 x. _pi ) ) -> ( abs ` ( 2 x. _pi ) ) = ( 2 x. _pi ) )
49 34 47 48 mp2an 
 |-  ( abs ` ( 2 x. _pi ) ) = ( 2 x. _pi )
50 49 oveq2i 
 |-  ( ( abs ` ( x - y ) ) / ( abs ` ( 2 x. _pi ) ) ) = ( ( abs ` ( x - y ) ) / ( 2 x. _pi ) )
51 45 50 eqtrdi 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( abs ` ( ( x - y ) / ( 2 x. _pi ) ) ) = ( ( abs ` ( x - y ) ) / ( 2 x. _pi ) ) )
52 4 adantr 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( abs ` ( x - y ) ) < ( 2 x. _pi ) )
53 35 mulridi 
 |-  ( ( 2 x. _pi ) x. 1 ) = ( 2 x. _pi )
54 52 53 breqtrrdi 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( abs ` ( x - y ) ) < ( ( 2 x. _pi ) x. 1 ) )
55 31 abscld 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( abs ` ( x - y ) ) e. RR )
56 1re 
 |-  1 e. RR
57 34 38 pm3.2i 
 |-  ( ( 2 x. _pi ) e. RR /\ 0 < ( 2 x. _pi ) )
58 ltdivmul 
 |-  ( ( ( abs ` ( x - y ) ) e. RR /\ 1 e. RR /\ ( ( 2 x. _pi ) e. RR /\ 0 < ( 2 x. _pi ) ) ) -> ( ( ( abs ` ( x - y ) ) / ( 2 x. _pi ) ) < 1 <-> ( abs ` ( x - y ) ) < ( ( 2 x. _pi ) x. 1 ) ) )
59 56 57 58 mp3an23 
 |-  ( ( abs ` ( x - y ) ) e. RR -> ( ( ( abs ` ( x - y ) ) / ( 2 x. _pi ) ) < 1 <-> ( abs ` ( x - y ) ) < ( ( 2 x. _pi ) x. 1 ) ) )
60 55 59 syl 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( ( ( abs ` ( x - y ) ) / ( 2 x. _pi ) ) < 1 <-> ( abs ` ( x - y ) ) < ( ( 2 x. _pi ) x. 1 ) ) )
61 54 60 mpbird 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( ( abs ` ( x - y ) ) / ( 2 x. _pi ) ) < 1 )
62 51 61 eqbrtrd 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( abs ` ( ( x - y ) / ( 2 x. _pi ) ) ) < 1 )
63 35 39 pm3.2i 
 |-  ( ( 2 x. _pi ) e. CC /\ ( 2 x. _pi ) =/= 0 )
64 ine0 
 |-  _i =/= 0
65 8 64 pm3.2i 
 |-  ( _i e. CC /\ _i =/= 0 )
66 divcan5 
 |-  ( ( ( x - y ) e. CC /\ ( ( 2 x. _pi ) e. CC /\ ( 2 x. _pi ) =/= 0 ) /\ ( _i e. CC /\ _i =/= 0 ) ) -> ( ( _i x. ( x - y ) ) / ( _i x. ( 2 x. _pi ) ) ) = ( ( x - y ) / ( 2 x. _pi ) ) )
67 63 65 66 mp3an23 
 |-  ( ( x - y ) e. CC -> ( ( _i x. ( x - y ) ) / ( _i x. ( 2 x. _pi ) ) ) = ( ( x - y ) / ( 2 x. _pi ) ) )
68 31 67 syl 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( ( _i x. ( x - y ) ) / ( _i x. ( 2 x. _pi ) ) ) = ( ( x - y ) / ( 2 x. _pi ) ) )
69 8 a1i 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> _i e. CC )
70 69 27 30 subdid 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( _i x. ( x - y ) ) = ( ( _i x. x ) - ( _i x. y ) ) )
71 70 fveq2d 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( exp ` ( _i x. ( x - y ) ) ) = ( exp ` ( ( _i x. x ) - ( _i x. y ) ) ) )
72 mulcl 
 |-  ( ( _i e. CC /\ x e. CC ) -> ( _i x. x ) e. CC )
73 8 27 72 sylancr 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( _i x. x ) e. CC )
74 mulcl 
 |-  ( ( _i e. CC /\ y e. CC ) -> ( _i x. y ) e. CC )
75 8 30 74 sylancr 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( _i x. y ) e. CC )
76 efsub 
 |-  ( ( ( _i x. x ) e. CC /\ ( _i x. y ) e. CC ) -> ( exp ` ( ( _i x. x ) - ( _i x. y ) ) ) = ( ( exp ` ( _i x. x ) ) / ( exp ` ( _i x. y ) ) ) )
77 73 75 76 syl2anc 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( exp ` ( ( _i x. x ) - ( _i x. y ) ) ) = ( ( exp ` ( _i x. x ) ) / ( exp ` ( _i x. y ) ) ) )
78 efcl 
 |-  ( ( _i x. y ) e. CC -> ( exp ` ( _i x. y ) ) e. CC )
79 75 78 syl 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( exp ` ( _i x. y ) ) e. CC )
80 efne0 
 |-  ( ( _i x. y ) e. CC -> ( exp ` ( _i x. y ) ) =/= 0 )
81 75 80 syl 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( exp ` ( _i x. y ) ) =/= 0 )
82 simpr 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( F ` x ) = ( F ` y ) )
83 oveq2 
 |-  ( w = x -> ( _i x. w ) = ( _i x. x ) )
84 83 fveq2d 
 |-  ( w = x -> ( exp ` ( _i x. w ) ) = ( exp ` ( _i x. x ) ) )
85 fvex 
 |-  ( exp ` ( _i x. x ) ) e. _V
86 84 1 85 fvmpt 
 |-  ( x e. D -> ( F ` x ) = ( exp ` ( _i x. x ) ) )
87 25 86 syl 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( F ` x ) = ( exp ` ( _i x. x ) ) )
88 oveq2 
 |-  ( w = y -> ( _i x. w ) = ( _i x. y ) )
89 88 fveq2d 
 |-  ( w = y -> ( exp ` ( _i x. w ) ) = ( exp ` ( _i x. y ) ) )
90 fvex 
 |-  ( exp ` ( _i x. y ) ) e. _V
91 89 1 90 fvmpt 
 |-  ( y e. D -> ( F ` y ) = ( exp ` ( _i x. y ) ) )
92 28 91 syl 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( F ` y ) = ( exp ` ( _i x. y ) ) )
93 82 87 92 3eqtr3d 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( exp ` ( _i x. x ) ) = ( exp ` ( _i x. y ) ) )
94 79 81 93 diveq1bd 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( ( exp ` ( _i x. x ) ) / ( exp ` ( _i x. y ) ) ) = 1 )
95 71 77 94 3eqtrd 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( exp ` ( _i x. ( x - y ) ) ) = 1 )
96 mulcl 
 |-  ( ( _i e. CC /\ ( x - y ) e. CC ) -> ( _i x. ( x - y ) ) e. CC )
97 8 31 96 sylancr 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( _i x. ( x - y ) ) e. CC )
98 efeq1 
 |-  ( ( _i x. ( x - y ) ) e. CC -> ( ( exp ` ( _i x. ( x - y ) ) ) = 1 <-> ( ( _i x. ( x - y ) ) / ( _i x. ( 2 x. _pi ) ) ) e. ZZ ) )
99 97 98 syl 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( ( exp ` ( _i x. ( x - y ) ) ) = 1 <-> ( ( _i x. ( x - y ) ) / ( _i x. ( 2 x. _pi ) ) ) e. ZZ ) )
100 95 99 mpbid 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( ( _i x. ( x - y ) ) / ( _i x. ( 2 x. _pi ) ) ) e. ZZ )
101 68 100 eqeltrrd 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( ( x - y ) / ( 2 x. _pi ) ) e. ZZ )
102 nn0abscl 
 |-  ( ( ( x - y ) / ( 2 x. _pi ) ) e. ZZ -> ( abs ` ( ( x - y ) / ( 2 x. _pi ) ) ) e. NN0 )
103 101 102 syl 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( abs ` ( ( x - y ) / ( 2 x. _pi ) ) ) e. NN0 )
104 nn0lt10b 
 |-  ( ( abs ` ( ( x - y ) / ( 2 x. _pi ) ) ) e. NN0 -> ( ( abs ` ( ( x - y ) / ( 2 x. _pi ) ) ) < 1 <-> ( abs ` ( ( x - y ) / ( 2 x. _pi ) ) ) = 0 ) )
105 103 104 syl 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( ( abs ` ( ( x - y ) / ( 2 x. _pi ) ) ) < 1 <-> ( abs ` ( ( x - y ) / ( 2 x. _pi ) ) ) = 0 ) )
106 62 105 mpbid 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( abs ` ( ( x - y ) / ( 2 x. _pi ) ) ) = 0 )
107 42 106 abs00d 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( ( x - y ) / ( 2 x. _pi ) ) = 0 )
108 diveq0 
 |-  ( ( ( x - y ) e. CC /\ ( 2 x. _pi ) e. CC /\ ( 2 x. _pi ) =/= 0 ) -> ( ( ( x - y ) / ( 2 x. _pi ) ) = 0 <-> ( x - y ) = 0 ) )
109 35 39 108 mp3an23 
 |-  ( ( x - y ) e. CC -> ( ( ( x - y ) / ( 2 x. _pi ) ) = 0 <-> ( x - y ) = 0 ) )
110 31 109 syl 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( ( ( x - y ) / ( 2 x. _pi ) ) = 0 <-> ( x - y ) = 0 ) )
111 107 110 mpbid 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( x - y ) = 0 )
112 27 30 111 subeq0d 
 |-  ( ( ( ph /\ ( x e. D /\ y e. D ) ) /\ ( F ` x ) = ( F ` y ) ) -> x = y )
113 112 ex 
 |-  ( ( ph /\ ( x e. D /\ y e. D ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
114 113 ralrimivva 
 |-  ( ph -> A. x e. D A. y e. D ( ( F ` x ) = ( F ` y ) -> x = y ) )
115 dff13 
 |-  ( F : D -1-1-> C <-> ( F : D --> C /\ A. x e. D A. y e. D ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
116 23 114 115 sylanbrc 
 |-  ( ph -> F : D -1-1-> C )
117 oveq1 
 |-  ( z = ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) -> ( z - y ) = ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) )
118 117 oveq1d 
 |-  ( z = ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) -> ( ( z - y ) / ( 2 x. _pi ) ) = ( ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) / ( 2 x. _pi ) ) )
119 118 eleq1d 
 |-  ( z = ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) -> ( ( ( z - y ) / ( 2 x. _pi ) ) e. ZZ <-> ( ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) / ( 2 x. _pi ) ) e. ZZ ) )
120 119 rexbidv 
 |-  ( z = ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) -> ( E. y e. D ( ( z - y ) / ( 2 x. _pi ) ) e. ZZ <-> E. y e. D ( ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) / ( 2 x. _pi ) ) e. ZZ ) )
121 5 ralrimiva 
 |-  ( ph -> A. z e. RR E. y e. D ( ( z - y ) / ( 2 x. _pi ) ) e. ZZ )
122 121 adantr 
 |-  ( ( ph /\ x e. C ) -> A. z e. RR E. y e. D ( ( z - y ) / ( 2 x. _pi ) ) e. ZZ )
123 neghalfpire 
 |-  -u ( _pi / 2 ) e. RR
124 halfpire 
 |-  ( _pi / 2 ) e. RR
125 iccssre 
 |-  ( ( -u ( _pi / 2 ) e. RR /\ ( _pi / 2 ) e. RR ) -> ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) C_ RR )
126 123 124 125 mp2an 
 |-  ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) C_ RR
127 1 2 efif1olem3 
 |-  ( ( ph /\ x e. C ) -> ( Im ` ( sqrt ` x ) ) e. ( -u 1 [,] 1 ) )
128 resinf1o 
 |-  ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) : ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -1-1-onto-> ( -u 1 [,] 1 )
129 f1oeq1 
 |-  ( S = ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) -> ( S : ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -1-1-onto-> ( -u 1 [,] 1 ) <-> ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) : ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -1-1-onto-> ( -u 1 [,] 1 ) ) )
130 6 129 ax-mp 
 |-  ( S : ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -1-1-onto-> ( -u 1 [,] 1 ) <-> ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) : ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -1-1-onto-> ( -u 1 [,] 1 ) )
131 128 130 mpbir 
 |-  S : ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -1-1-onto-> ( -u 1 [,] 1 )
132 f1ocnv 
 |-  ( S : ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -1-1-onto-> ( -u 1 [,] 1 ) -> `' S : ( -u 1 [,] 1 ) -1-1-onto-> ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
133 f1of 
 |-  ( `' S : ( -u 1 [,] 1 ) -1-1-onto-> ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> `' S : ( -u 1 [,] 1 ) --> ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
134 131 132 133 mp2b 
 |-  `' S : ( -u 1 [,] 1 ) --> ( -u ( _pi / 2 ) [,] ( _pi / 2 ) )
135 134 ffvelcdmi 
 |-  ( ( Im ` ( sqrt ` x ) ) e. ( -u 1 [,] 1 ) -> ( `' S ` ( Im ` ( sqrt ` x ) ) ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
136 127 135 syl 
 |-  ( ( ph /\ x e. C ) -> ( `' S ` ( Im ` ( sqrt ` x ) ) ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
137 126 136 sselid 
 |-  ( ( ph /\ x e. C ) -> ( `' S ` ( Im ` ( sqrt ` x ) ) ) e. RR )
138 remulcl 
 |-  ( ( 2 e. RR /\ ( `' S ` ( Im ` ( sqrt ` x ) ) ) e. RR ) -> ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) e. RR )
139 32 137 138 sylancr 
 |-  ( ( ph /\ x e. C ) -> ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) e. RR )
140 120 122 139 rspcdva 
 |-  ( ( ph /\ x e. C ) -> E. y e. D ( ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) / ( 2 x. _pi ) ) e. ZZ )
141 oveq1 
 |-  ( ( exp ` ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) ) = 1 -> ( ( exp ` ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) ) x. ( exp ` ( _i x. y ) ) ) = ( 1 x. ( exp ` ( _i x. y ) ) ) )
142 8 a1i 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> _i e. CC )
143 139 adantr 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) e. RR )
144 143 recnd 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) e. CC )
145 3 ad2antrr 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> D C_ RR )
146 simpr 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> y e. D )
147 145 146 sseldd 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> y e. RR )
148 147 recnd 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> y e. CC )
149 142 144 148 subdid 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) = ( ( _i x. ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) - ( _i x. y ) ) )
150 149 oveq1d 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) + ( _i x. y ) ) = ( ( ( _i x. ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) - ( _i x. y ) ) + ( _i x. y ) ) )
151 mulcl 
 |-  ( ( _i e. CC /\ ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) e. CC ) -> ( _i x. ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) e. CC )
152 8 144 151 sylancr 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( _i x. ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) e. CC )
153 8 148 74 sylancr 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( _i x. y ) e. CC )
154 152 153 npcand 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( ( ( _i x. ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) - ( _i x. y ) ) + ( _i x. y ) ) = ( _i x. ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) )
155 150 154 eqtrd 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) + ( _i x. y ) ) = ( _i x. ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) )
156 155 fveq2d 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( exp ` ( ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) + ( _i x. y ) ) ) = ( exp ` ( _i x. ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) ) )
157 144 148 subcld 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) e. CC )
158 mulcl 
 |-  ( ( _i e. CC /\ ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) e. CC ) -> ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) e. CC )
159 8 157 158 sylancr 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) e. CC )
160 efadd 
 |-  ( ( ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) e. CC /\ ( _i x. y ) e. CC ) -> ( exp ` ( ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) + ( _i x. y ) ) ) = ( ( exp ` ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) ) x. ( exp ` ( _i x. y ) ) ) )
161 159 153 160 syl2anc 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( exp ` ( ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) + ( _i x. y ) ) ) = ( ( exp ` ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) ) x. ( exp ` ( _i x. y ) ) ) )
162 2cn 
 |-  2 e. CC
163 137 recnd 
 |-  ( ( ph /\ x e. C ) -> ( `' S ` ( Im ` ( sqrt ` x ) ) ) e. CC )
164 mul12 
 |-  ( ( _i e. CC /\ 2 e. CC /\ ( `' S ` ( Im ` ( sqrt ` x ) ) ) e. CC ) -> ( _i x. ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) = ( 2 x. ( _i x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) )
165 8 162 163 164 mp3an12i 
 |-  ( ( ph /\ x e. C ) -> ( _i x. ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) = ( 2 x. ( _i x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) )
166 165 fveq2d 
 |-  ( ( ph /\ x e. C ) -> ( exp ` ( _i x. ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) ) = ( exp ` ( 2 x. ( _i x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) ) )
167 mulcl 
 |-  ( ( _i e. CC /\ ( `' S ` ( Im ` ( sqrt ` x ) ) ) e. CC ) -> ( _i x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) e. CC )
168 8 163 167 sylancr 
 |-  ( ( ph /\ x e. C ) -> ( _i x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) e. CC )
169 2z 
 |-  2 e. ZZ
170 efexp 
 |-  ( ( ( _i x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) e. CC /\ 2 e. ZZ ) -> ( exp ` ( 2 x. ( _i x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) ) = ( ( exp ` ( _i x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) ^ 2 ) )
171 168 169 170 sylancl 
 |-  ( ( ph /\ x e. C ) -> ( exp ` ( 2 x. ( _i x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) ) = ( ( exp ` ( _i x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) ^ 2 ) )
172 166 171 eqtrd 
 |-  ( ( ph /\ x e. C ) -> ( exp ` ( _i x. ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) ) = ( ( exp ` ( _i x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) ^ 2 ) )
173 137 recoscld 
 |-  ( ( ph /\ x e. C ) -> ( cos ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) e. RR )
174 simpr 
 |-  ( ( ph /\ x e. C ) -> x e. C )
175 174 2 eleqtrdi 
 |-  ( ( ph /\ x e. C ) -> x e. ( `' abs " { 1 } ) )
176 fniniseg 
 |-  ( abs Fn CC -> ( x e. ( `' abs " { 1 } ) <-> ( x e. CC /\ ( abs ` x ) = 1 ) ) )
177 17 176 ax-mp 
 |-  ( x e. ( `' abs " { 1 } ) <-> ( x e. CC /\ ( abs ` x ) = 1 ) )
178 175 177 sylib 
 |-  ( ( ph /\ x e. C ) -> ( x e. CC /\ ( abs ` x ) = 1 ) )
179 178 simpld 
 |-  ( ( ph /\ x e. C ) -> x e. CC )
180 179 sqrtcld 
 |-  ( ( ph /\ x e. C ) -> ( sqrt ` x ) e. CC )
181 180 recld 
 |-  ( ( ph /\ x e. C ) -> ( Re ` ( sqrt ` x ) ) e. RR )
182 cosq14ge0 
 |-  ( ( `' S ` ( Im ` ( sqrt ` x ) ) ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> 0 <_ ( cos ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) )
183 136 182 syl 
 |-  ( ( ph /\ x e. C ) -> 0 <_ ( cos ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) )
184 179 sqrtrege0d 
 |-  ( ( ph /\ x e. C ) -> 0 <_ ( Re ` ( sqrt ` x ) ) )
185 sincossq 
 |-  ( ( `' S ` ( Im ` ( sqrt ` x ) ) ) e. CC -> ( ( ( sin ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ^ 2 ) + ( ( cos ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ^ 2 ) ) = 1 )
186 163 185 syl 
 |-  ( ( ph /\ x e. C ) -> ( ( ( sin ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ^ 2 ) + ( ( cos ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ^ 2 ) ) = 1 )
187 179 sqsqrtd 
 |-  ( ( ph /\ x e. C ) -> ( ( sqrt ` x ) ^ 2 ) = x )
188 187 fveq2d 
 |-  ( ( ph /\ x e. C ) -> ( abs ` ( ( sqrt ` x ) ^ 2 ) ) = ( abs ` x ) )
189 2nn0 
 |-  2 e. NN0
190 absexp 
 |-  ( ( ( sqrt ` x ) e. CC /\ 2 e. NN0 ) -> ( abs ` ( ( sqrt ` x ) ^ 2 ) ) = ( ( abs ` ( sqrt ` x ) ) ^ 2 ) )
191 180 189 190 sylancl 
 |-  ( ( ph /\ x e. C ) -> ( abs ` ( ( sqrt ` x ) ^ 2 ) ) = ( ( abs ` ( sqrt ` x ) ) ^ 2 ) )
192 178 simprd 
 |-  ( ( ph /\ x e. C ) -> ( abs ` x ) = 1 )
193 188 191 192 3eqtr3d 
 |-  ( ( ph /\ x e. C ) -> ( ( abs ` ( sqrt ` x ) ) ^ 2 ) = 1 )
194 180 absvalsq2d 
 |-  ( ( ph /\ x e. C ) -> ( ( abs ` ( sqrt ` x ) ) ^ 2 ) = ( ( ( Re ` ( sqrt ` x ) ) ^ 2 ) + ( ( Im ` ( sqrt ` x ) ) ^ 2 ) ) )
195 186 193 194 3eqtr2d 
 |-  ( ( ph /\ x e. C ) -> ( ( ( sin ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ^ 2 ) + ( ( cos ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ^ 2 ) ) = ( ( ( Re ` ( sqrt ` x ) ) ^ 2 ) + ( ( Im ` ( sqrt ` x ) ) ^ 2 ) ) )
196 6 fveq1i 
 |-  ( S ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) = ( ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) )
197 136 fvresd 
 |-  ( ( ph /\ x e. C ) -> ( ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) = ( sin ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) )
198 196 197 eqtrid 
 |-  ( ( ph /\ x e. C ) -> ( S ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) = ( sin ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) )
199 f1ocnvfv2 
 |-  ( ( S : ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -1-1-onto-> ( -u 1 [,] 1 ) /\ ( Im ` ( sqrt ` x ) ) e. ( -u 1 [,] 1 ) ) -> ( S ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) = ( Im ` ( sqrt ` x ) ) )
200 131 127 199 sylancr 
 |-  ( ( ph /\ x e. C ) -> ( S ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) = ( Im ` ( sqrt ` x ) ) )
201 198 200 eqtr3d 
 |-  ( ( ph /\ x e. C ) -> ( sin ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) = ( Im ` ( sqrt ` x ) ) )
202 201 oveq1d 
 |-  ( ( ph /\ x e. C ) -> ( ( sin ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ^ 2 ) = ( ( Im ` ( sqrt ` x ) ) ^ 2 ) )
203 195 202 oveq12d 
 |-  ( ( ph /\ x e. C ) -> ( ( ( ( sin ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ^ 2 ) + ( ( cos ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ^ 2 ) ) - ( ( sin ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ^ 2 ) ) = ( ( ( ( Re ` ( sqrt ` x ) ) ^ 2 ) + ( ( Im ` ( sqrt ` x ) ) ^ 2 ) ) - ( ( Im ` ( sqrt ` x ) ) ^ 2 ) ) )
204 163 sincld 
 |-  ( ( ph /\ x e. C ) -> ( sin ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) e. CC )
205 204 sqcld 
 |-  ( ( ph /\ x e. C ) -> ( ( sin ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ^ 2 ) e. CC )
206 163 coscld 
 |-  ( ( ph /\ x e. C ) -> ( cos ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) e. CC )
207 206 sqcld 
 |-  ( ( ph /\ x e. C ) -> ( ( cos ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ^ 2 ) e. CC )
208 205 207 pncan2d 
 |-  ( ( ph /\ x e. C ) -> ( ( ( ( sin ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ^ 2 ) + ( ( cos ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ^ 2 ) ) - ( ( sin ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ^ 2 ) ) = ( ( cos ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ^ 2 ) )
209 181 recnd 
 |-  ( ( ph /\ x e. C ) -> ( Re ` ( sqrt ` x ) ) e. CC )
210 209 sqcld 
 |-  ( ( ph /\ x e. C ) -> ( ( Re ` ( sqrt ` x ) ) ^ 2 ) e. CC )
211 202 205 eqeltrrd 
 |-  ( ( ph /\ x e. C ) -> ( ( Im ` ( sqrt ` x ) ) ^ 2 ) e. CC )
212 210 211 pncand 
 |-  ( ( ph /\ x e. C ) -> ( ( ( ( Re ` ( sqrt ` x ) ) ^ 2 ) + ( ( Im ` ( sqrt ` x ) ) ^ 2 ) ) - ( ( Im ` ( sqrt ` x ) ) ^ 2 ) ) = ( ( Re ` ( sqrt ` x ) ) ^ 2 ) )
213 203 208 212 3eqtr3d 
 |-  ( ( ph /\ x e. C ) -> ( ( cos ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ^ 2 ) = ( ( Re ` ( sqrt ` x ) ) ^ 2 ) )
214 173 181 183 184 213 sq11d 
 |-  ( ( ph /\ x e. C ) -> ( cos ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) = ( Re ` ( sqrt ` x ) ) )
215 201 oveq2d 
 |-  ( ( ph /\ x e. C ) -> ( _i x. ( sin ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) = ( _i x. ( Im ` ( sqrt ` x ) ) ) )
216 214 215 oveq12d 
 |-  ( ( ph /\ x e. C ) -> ( ( cos ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) + ( _i x. ( sin ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) ) = ( ( Re ` ( sqrt ` x ) ) + ( _i x. ( Im ` ( sqrt ` x ) ) ) ) )
217 efival 
 |-  ( ( `' S ` ( Im ` ( sqrt ` x ) ) ) e. CC -> ( exp ` ( _i x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) = ( ( cos ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) + ( _i x. ( sin ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) ) )
218 163 217 syl 
 |-  ( ( ph /\ x e. C ) -> ( exp ` ( _i x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) = ( ( cos ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) + ( _i x. ( sin ` ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) ) )
219 180 replimd 
 |-  ( ( ph /\ x e. C ) -> ( sqrt ` x ) = ( ( Re ` ( sqrt ` x ) ) + ( _i x. ( Im ` ( sqrt ` x ) ) ) ) )
220 216 218 219 3eqtr4d 
 |-  ( ( ph /\ x e. C ) -> ( exp ` ( _i x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) = ( sqrt ` x ) )
221 220 oveq1d 
 |-  ( ( ph /\ x e. C ) -> ( ( exp ` ( _i x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) ^ 2 ) = ( ( sqrt ` x ) ^ 2 ) )
222 172 221 187 3eqtrd 
 |-  ( ( ph /\ x e. C ) -> ( exp ` ( _i x. ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) ) = x )
223 222 adantr 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( exp ` ( _i x. ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) ) ) = x )
224 156 161 223 3eqtr3d 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( ( exp ` ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) ) x. ( exp ` ( _i x. y ) ) ) = x )
225 153 78 syl 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( exp ` ( _i x. y ) ) e. CC )
226 225 mullidd 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( 1 x. ( exp ` ( _i x. y ) ) ) = ( exp ` ( _i x. y ) ) )
227 224 226 eqeq12d 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( ( ( exp ` ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) ) x. ( exp ` ( _i x. y ) ) ) = ( 1 x. ( exp ` ( _i x. y ) ) ) <-> x = ( exp ` ( _i x. y ) ) ) )
228 141 227 imbitrid 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( ( exp ` ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) ) = 1 -> x = ( exp ` ( _i x. y ) ) ) )
229 efeq1 
 |-  ( ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) e. CC -> ( ( exp ` ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) ) = 1 <-> ( ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) / ( _i x. ( 2 x. _pi ) ) ) e. ZZ ) )
230 159 229 syl 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( ( exp ` ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) ) = 1 <-> ( ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) / ( _i x. ( 2 x. _pi ) ) ) e. ZZ ) )
231 divcan5 
 |-  ( ( ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) e. CC /\ ( ( 2 x. _pi ) e. CC /\ ( 2 x. _pi ) =/= 0 ) /\ ( _i e. CC /\ _i =/= 0 ) ) -> ( ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) / ( _i x. ( 2 x. _pi ) ) ) = ( ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) / ( 2 x. _pi ) ) )
232 63 65 231 mp3an23 
 |-  ( ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) e. CC -> ( ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) / ( _i x. ( 2 x. _pi ) ) ) = ( ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) / ( 2 x. _pi ) ) )
233 157 232 syl 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) / ( _i x. ( 2 x. _pi ) ) ) = ( ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) / ( 2 x. _pi ) ) )
234 233 eleq1d 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( ( ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) / ( _i x. ( 2 x. _pi ) ) ) e. ZZ <-> ( ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) / ( 2 x. _pi ) ) e. ZZ ) )
235 230 234 bitr2d 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( ( ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) / ( 2 x. _pi ) ) e. ZZ <-> ( exp ` ( _i x. ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) ) ) = 1 ) )
236 91 adantl 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( F ` y ) = ( exp ` ( _i x. y ) ) )
237 236 eqeq2d 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( x = ( F ` y ) <-> x = ( exp ` ( _i x. y ) ) ) )
238 228 235 237 3imtr4d 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( ( ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) / ( 2 x. _pi ) ) e. ZZ -> x = ( F ` y ) ) )
239 238 reximdva 
 |-  ( ( ph /\ x e. C ) -> ( E. y e. D ( ( ( 2 x. ( `' S ` ( Im ` ( sqrt ` x ) ) ) ) - y ) / ( 2 x. _pi ) ) e. ZZ -> E. y e. D x = ( F ` y ) ) )
240 140 239 mpd 
 |-  ( ( ph /\ x e. C ) -> E. y e. D x = ( F ` y ) )
241 240 ralrimiva 
 |-  ( ph -> A. x e. C E. y e. D x = ( F ` y ) )
242 dffo3 
 |-  ( F : D -onto-> C <-> ( F : D --> C /\ A. x e. C E. y e. D x = ( F ` y ) ) )
243 23 241 242 sylanbrc 
 |-  ( ph -> F : D -onto-> C )
244 df-f1o 
 |-  ( F : D -1-1-onto-> C <-> ( F : D -1-1-> C /\ F : D -onto-> C ) )
245 116 243 244 sylanbrc 
 |-  ( ph -> F : D -1-1-onto-> C )