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