MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  efif1olem4 Structured version   Unicode version

Theorem efif1olem4 20485
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.)
Hypotheses
Ref Expression
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
Ref Expression
efif1olem4  |-  ( ph  ->  F : D -1-1-onto-> C )
Distinct variable groups:    x, w, y, z    w, C, x, y    x, F, y    ph, w, x, y, z   
y, S, z    w, D, x, y, z
Allowed substitution hints:    C( z)    S( x, w)    F( z, w)

Proof of Theorem efif1olem4
StepHypRef Expression
1 efif1olem4.3 . . . . . 6  |-  ( ph  ->  D  C_  RR )
21sselda 3337 . . . . 5  |-  ( (
ph  /\  w  e.  D )  ->  w  e.  RR )
3 ax-icn 9087 . . . . . . . . 9  |-  _i  e.  CC
4 recn 9118 . . . . . . . . 9  |-  ( w  e.  RR  ->  w  e.  CC )
5 mulcl 9112 . . . . . . . . 9  |-  ( ( _i  e.  CC  /\  w  e.  CC )  ->  ( _i  x.  w
)  e.  CC )
63, 4, 5sylancr 646 . . . . . . . 8  |-  ( w  e.  RR  ->  (
_i  x.  w )  e.  CC )
7 efcl 12723 . . . . . . . 8  |-  ( ( _i  x.  w )  e.  CC  ->  ( exp `  ( _i  x.  w ) )  e.  CC )
86, 7syl 16 . . . . . . 7  |-  ( w  e.  RR  ->  ( exp `  ( _i  x.  w ) )  e.  CC )
9 absefi 12835 . . . . . . 7  |-  ( w  e.  RR  ->  ( abs `  ( exp `  (
_i  x.  w )
) )  =  1 )
10 absf 12179 . . . . . . . . 9  |-  abs : CC
--> RR
11 ffn 5626 . . . . . . . . 9  |-  ( abs
: CC --> RR  ->  abs 
Fn  CC )
1210, 11ax-mp 5 . . . . . . . 8  |-  abs  Fn  CC
13 fniniseg 5887 . . . . . . . 8  |-  ( abs 
Fn  CC  ->  ( ( exp `  ( _i  x.  w ) )  e.  ( `' abs " { 1 } )  <-> 
( ( exp `  (
_i  x.  w )
)  e.  CC  /\  ( abs `  ( exp `  ( _i  x.  w
) ) )  =  1 ) ) )
1412, 13ax-mp 5 . . . . . . 7  |-  ( ( exp `  ( _i  x.  w ) )  e.  ( `' abs " { 1 } )  <-> 
( ( exp `  (
_i  x.  w )
)  e.  CC  /\  ( abs `  ( exp `  ( _i  x.  w
) ) )  =  1 ) )
158, 9, 14sylanbrc 647 . . . . . 6  |-  ( w  e.  RR  ->  ( exp `  ( _i  x.  w ) )  e.  ( `' abs " {
1 } ) )
16 efif1o.2 . . . . . 6  |-  C  =  ( `' abs " {
1 } )
1715, 16syl6eleqr 2534 . . . . 5  |-  ( w  e.  RR  ->  ( exp `  ( _i  x.  w ) )  e.  C )
182, 17syl 16 . . . 4  |-  ( (
ph  /\  w  e.  D )  ->  ( exp `  ( _i  x.  w ) )  e.  C )
19 efif1o.1 . . . 4  |-  F  =  ( w  e.  D  |->  ( exp `  (
_i  x.  w )
) )
2018, 19fmptd 5929 . . 3  |-  ( ph  ->  F : D --> C )
211ad2antrr 708 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  D  C_  RR )
22 simplrl 738 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  x  e.  D )
2321, 22sseldd 3338 . . . . . . 7  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  x  e.  RR )
2423recnd 9152 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  x  e.  CC )
25 simplrr 739 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  y  e.  D )
2621, 25sseldd 3338 . . . . . . 7  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  y  e.  RR )
2726recnd 9152 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  y  e.  CC )
2824, 27subcld 9449 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( x  -  y )  e.  CC )
29 2re 10107 . . . . . . . . . . . 12  |-  2  e.  RR
30 pire 20410 . . . . . . . . . . . 12  |-  pi  e.  RR
3129, 30remulcli 9142 . . . . . . . . . . 11  |-  ( 2  x.  pi )  e.  RR
3231recni 9140 . . . . . . . . . 10  |-  ( 2  x.  pi )  e.  CC
33 2pos 10120 . . . . . . . . . . . 12  |-  0  <  2
34 pipos 20411 . . . . . . . . . . . 12  |-  0  <  pi
3529, 30, 33, 34mulgt0ii 9244 . . . . . . . . . . 11  |-  0  <  ( 2  x.  pi )
3631, 35gt0ne0ii 9601 . . . . . . . . . 10  |-  ( 2  x.  pi )  =/=  0
37 divcl 9722 . . . . . . . . . 10  |-  ( ( ( x  -  y
)  e.  CC  /\  ( 2  x.  pi )  e.  CC  /\  (
2  x.  pi )  =/=  0 )  -> 
( ( x  -  y )  /  (
2  x.  pi ) )  e.  CC )
3832, 36, 37mp3an23 1272 . . . . . . . . 9  |-  ( ( x  -  y )  e.  CC  ->  (
( x  -  y
)  /  ( 2  x.  pi ) )  e.  CC )
3928, 38syl 16 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( (
x  -  y )  /  ( 2  x.  pi ) )  e.  CC )
40 absdiv 12138 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) ) ) )
4132, 36, 40mp3an23 1272 . . . . . . . . . . . 12  |-  ( ( x  -  y )  e.  CC  ->  ( abs `  ( ( x  -  y )  / 
( 2  x.  pi ) ) )  =  ( ( abs `  (
x  -  y ) )  /  ( abs `  ( 2  x.  pi ) ) ) )
4228, 41syl 16 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( abs `  ( ( x  -  y )  /  (
2  x.  pi ) ) )  =  ( ( abs `  (
x  -  y ) )  /  ( abs `  ( 2  x.  pi ) ) ) )
43 0re 9129 . . . . . . . . . . . . . 14  |-  0  e.  RR
4443, 31, 35ltleii 9234 . . . . . . . . . . . . 13  |-  0  <_  ( 2  x.  pi )
45 absid 12139 . . . . . . . . . . . . 13  |-  ( ( ( 2  x.  pi )  e.  RR  /\  0  <_  ( 2  x.  pi ) )  ->  ( abs `  ( 2  x.  pi ) )  =  ( 2  x.  pi ) )
4631, 44, 45mp2an 655 . . . . . . . . . . . 12  |-  ( abs `  ( 2  x.  pi ) )  =  ( 2  x.  pi )
4746oveq2i 6128 . . . . . . . . . . 11  |-  ( ( abs `  ( x  -  y ) )  /  ( abs `  (
2  x.  pi ) ) )  =  ( ( abs `  (
x  -  y ) )  /  ( 2  x.  pi ) )
4842, 47syl6eq 2491 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( abs `  ( ( x  -  y )  /  (
2  x.  pi ) ) )  =  ( ( abs `  (
x  -  y ) )  /  ( 2  x.  pi ) ) )
49 efif1olem4.4 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  D  /\  y  e.  D ) )  -> 
( abs `  (
x  -  y ) )  <  ( 2  x.  pi ) )
5049adantr 453 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( abs `  ( x  -  y
) )  <  (
2  x.  pi ) )
5132mulid1i 9130 . . . . . . . . . . . 12  |-  ( ( 2  x.  pi )  x.  1 )  =  ( 2  x.  pi )
5250, 51syl6breqr 4283 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( abs `  ( x  -  y
) )  <  (
( 2  x.  pi )  x.  1 ) )
5328abscld 12276 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( abs `  ( x  -  y
) )  e.  RR )
54 1re 9128 . . . . . . . . . . . . 13  |-  1  e.  RR
5531, 35pm3.2i 443 . . . . . . . . . . . . 13  |-  ( ( 2  x.  pi )  e.  RR  /\  0  <  ( 2  x.  pi ) )
56 ltdivmul 9920 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) ) )
5754, 55, 56mp3an23 1272 . . . . . . . . . . . 12  |-  ( ( abs `  ( x  -  y ) )  e.  RR  ->  (
( ( abs `  (
x  -  y ) )  /  ( 2  x.  pi ) )  <  1  <->  ( abs `  ( x  -  y
) )  <  (
( 2  x.  pi )  x.  1 ) ) )
5853, 57syl 16 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) )
5952, 58mpbird 225 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( ( abs `  ( x  -  y ) )  / 
( 2  x.  pi ) )  <  1
)
6048, 59eqbrtrd 4263 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( abs `  ( ( x  -  y )  /  (
2  x.  pi ) ) )  <  1
)
6132, 36pm3.2i 443 . . . . . . . . . . . . . 14  |-  ( ( 2  x.  pi )  e.  CC  /\  (
2  x.  pi )  =/=  0 )
62 ine0 9507 . . . . . . . . . . . . . . 15  |-  _i  =/=  0
633, 62pm3.2i 443 . . . . . . . . . . . . . 14  |-  ( _i  e.  CC  /\  _i  =/=  0 )
64 divcan5 9754 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) ) )
6561, 63, 64mp3an23 1272 . . . . . . . . . . . . 13  |-  ( ( x  -  y )  e.  CC  ->  (
( _i  x.  (
x  -  y ) )  /  ( _i  x.  ( 2  x.  pi ) ) )  =  ( ( x  -  y )  / 
( 2  x.  pi ) ) )
6628, 65syl 16 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) )
673a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  _i  e.  CC )
6867, 24, 27subdid 9527 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( _i  x.  ( x  -  y
) )  =  ( ( _i  x.  x
)  -  ( _i  x.  y ) ) )
6968fveq2d 5767 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( exp `  ( _i  x.  (
x  -  y ) ) )  =  ( exp `  ( ( _i  x.  x )  -  ( _i  x.  y ) ) ) )
70 mulcl 9112 . . . . . . . . . . . . . . . 16  |-  ( ( _i  e.  CC  /\  x  e.  CC )  ->  ( _i  x.  x
)  e.  CC )
713, 24, 70sylancr 646 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( _i  x.  x )  e.  CC )
72 mulcl 9112 . . . . . . . . . . . . . . . 16  |-  ( ( _i  e.  CC  /\  y  e.  CC )  ->  ( _i  x.  y
)  e.  CC )
733, 27, 72sylancr 646 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( _i  x.  y )  e.  CC )
74 efsub 12739 . . . . . . . . . . . . . . 15  |-  ( ( ( _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 )
) ) )
7571, 73, 74syl2anc 644 . . . . . . . . . . . . . 14  |-  ( ( ( 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
) ) ) )
76 efcl 12723 . . . . . . . . . . . . . . . 16  |-  ( ( _i  x.  y )  e.  CC  ->  ( exp `  ( _i  x.  y ) )  e.  CC )
7773, 76syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( exp `  ( _i  x.  y
) )  e.  CC )
78 efne0 12736 . . . . . . . . . . . . . . . 16  |-  ( ( _i  x.  y )  e.  CC  ->  ( exp `  ( _i  x.  y ) )  =/=  0 )
7973, 78syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( exp `  ( _i  x.  y
) )  =/=  0
)
80 simpr 449 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( F `  x )  =  ( F `  y ) )
81 oveq2 6125 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  x  ->  (
_i  x.  w )  =  ( _i  x.  x ) )
8281fveq2d 5767 . . . . . . . . . . . . . . . . . 18  |-  ( w  =  x  ->  ( exp `  ( _i  x.  w ) )  =  ( exp `  (
_i  x.  x )
) )
83 fvex 5773 . . . . . . . . . . . . . . . . . 18  |-  ( exp `  ( _i  x.  x
) )  e.  _V
8482, 19, 83fvmpt 5842 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  D  ->  ( F `  x )  =  ( exp `  (
_i  x.  x )
) )
8522, 84syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( F `  x )  =  ( exp `  ( _i  x.  x ) ) )
86 oveq2 6125 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  y  ->  (
_i  x.  w )  =  ( _i  x.  y ) )
8786fveq2d 5767 . . . . . . . . . . . . . . . . . 18  |-  ( w  =  y  ->  ( exp `  ( _i  x.  w ) )  =  ( exp `  (
_i  x.  y )
) )
88 fvex 5773 . . . . . . . . . . . . . . . . . 18  |-  ( exp `  ( _i  x.  y
) )  e.  _V
8987, 19, 88fvmpt 5842 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  D  ->  ( F `  y )  =  ( exp `  (
_i  x.  y )
) )
9025, 89syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( F `  y )  =  ( exp `  ( _i  x.  y ) ) )
9180, 85, 903eqtr3d 2483 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( exp `  ( _i  x.  x
) )  =  ( exp `  ( _i  x.  y ) ) )
9277, 79, 91diveq1bd 9876 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( ( exp `  ( _i  x.  x ) )  / 
( exp `  (
_i  x.  y )
) )  =  1 )
9369, 75, 923eqtrd 2479 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( exp `  ( _i  x.  (
x  -  y ) ) )  =  1 )
94 mulcl 9112 . . . . . . . . . . . . . . 15  |-  ( ( _i  e.  CC  /\  ( x  -  y
)  e.  CC )  ->  ( _i  x.  ( x  -  y
) )  e.  CC )
953, 28, 94sylancr 646 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( _i  x.  ( x  -  y
) )  e.  CC )
96 efeq1 20469 . . . . . . . . . . . . . 14  |-  ( ( _i  x.  ( x  -  y ) )  e.  CC  ->  (
( exp `  (
_i  x.  ( x  -  y ) ) )  =  1  <->  (
( _i  x.  (
x  -  y ) )  /  ( _i  x.  ( 2  x.  pi ) ) )  e.  ZZ ) )
9795, 96syl 16 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) )
9893, 97mpbid 203 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( (
_i  x.  ( x  -  y ) )  /  ( _i  x.  ( 2  x.  pi ) ) )  e.  ZZ )
9966, 98eqeltrrd 2518 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( (
x  -  y )  /  ( 2  x.  pi ) )  e.  ZZ )
100 nn0abscl 12155 . . . . . . . . . . 11  |-  ( ( ( x  -  y
)  /  ( 2  x.  pi ) )  e.  ZZ  ->  ( abs `  ( ( x  -  y )  / 
( 2  x.  pi ) ) )  e. 
NN0 )
10199, 100syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( abs `  ( ( x  -  y )  /  (
2  x.  pi ) ) )  e.  NN0 )
102 nn0lt10b 10374 . . . . . . . . . 10  |-  ( ( abs `  ( ( x  -  y )  /  ( 2  x.  pi ) ) )  e.  NN0  ->  ( ( abs `  ( ( x  -  y )  /  ( 2  x.  pi ) ) )  <  1  <->  ( abs `  ( ( x  -  y )  /  (
2  x.  pi ) ) )  =  0 ) )
103101, 102syl 16 . . . . . . . . 9  |-  ( ( ( 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 ) )
10460, 103mpbid 203 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( abs `  ( ( x  -  y )  /  (
2  x.  pi ) ) )  =  0 )
10539, 104abs00d 12286 . . . . . . 7  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( (
x  -  y )  /  ( 2  x.  pi ) )  =  0 )
106 diveq0 9726 . . . . . . . . 9  |-  ( ( ( x  -  y
)  e.  CC  /\  ( 2  x.  pi )  e.  CC  /\  (
2  x.  pi )  =/=  0 )  -> 
( ( ( x  -  y )  / 
( 2  x.  pi ) )  =  0  <-> 
( x  -  y
)  =  0 ) )
10732, 36, 106mp3an23 1272 . . . . . . . 8  |-  ( ( x  -  y )  e.  CC  ->  (
( ( x  -  y )  /  (
2  x.  pi ) )  =  0  <->  (
x  -  y )  =  0 ) )
10828, 107syl 16 . . . . . . 7  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( (
( x  -  y
)  /  ( 2  x.  pi ) )  =  0  <->  ( x  -  y )  =  0 ) )
109105, 108mpbid 203 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  ( x  -  y )  =  0 )
11024, 27, 109subeq0d 9457 . . . . 5  |-  ( ( ( ph  /\  (
x  e.  D  /\  y  e.  D )
)  /\  ( F `  x )  =  ( F `  y ) )  ->  x  =  y )
111110ex 425 . . . 4  |-  ( (
ph  /\  ( x  e.  D  /\  y  e.  D ) )  -> 
( ( F `  x )  =  ( F `  y )  ->  x  =  y ) )
112111ralrimivva 2805 . . 3  |-  ( ph  ->  A. x  e.  D  A. y  e.  D  ( ( F `  x )  =  ( F `  y )  ->  x  =  y ) )
113 dff13 6040 . . 3  |-  ( F : D -1-1-> C  <->  ( F : D --> C  /\  A. x  e.  D  A. y  e.  D  (
( F `  x
)  =  ( F `
 y )  ->  x  =  y )
) )
11420, 112, 113sylanbrc 647 . 2  |-  ( ph  ->  F : D -1-1-> C
)
115 halfpire 20413 . . . . . . . . . 10  |-  ( pi 
/  2 )  e.  RR
116115renegcli 9400 . . . . . . . . 9  |-  -u (
pi  /  2 )  e.  RR
117 iccssre 11030 . . . . . . . . 9  |-  ( (
-u ( pi  / 
2 )  e.  RR  /\  ( pi  /  2
)  e.  RR )  ->  ( -u (
pi  /  2 ) [,] ( pi  / 
2 ) )  C_  RR )
118116, 115, 117mp2an 655 . . . . . . . 8  |-  ( -u ( pi  /  2
) [,] ( pi 
/  2 ) ) 
C_  RR
11919, 16efif1olem3 20484 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  C )  ->  (
Im `  ( sqr `  x ) )  e.  ( -u 1 [,] 1 ) )
120 resinf1o 20476 . . . . . . . . . . . 12  |-  ( sin  |`  ( -u ( pi 
/  2 ) [,] ( pi  /  2
) ) ) : ( -u ( pi 
/  2 ) [,] ( pi  /  2
) ) -1-1-onto-> ( -u 1 [,] 1 )
121 efif1olem4.6 . . . . . . . . . . . . 13  |-  S  =  ( sin  |`  ( -u ( pi  /  2
) [,] ( pi 
/  2 ) ) )
122 f1oeq1 5700 . . . . . . . . . . . . 13  |-  ( 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
) ) )
123121, 122ax-mp 5 . . . . . . . . . . . 12  |-  ( 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
) )
124120, 123mpbir 202 . . . . . . . . . . 11  |-  S :
( -u ( pi  / 
2 ) [,] (
pi  /  2 ) ) -1-1-onto-> ( -u 1 [,] 1 )
125 f1ocnv 5722 . . . . . . . . . . 11  |-  ( S : ( -u (
pi  /  2 ) [,] ( pi  / 
2 ) ) -1-1-onto-> ( -u
1 [,] 1 )  ->  `' S :
( -u 1 [,] 1
)
-1-1-onto-> ( -u ( pi  / 
2 ) [,] (
pi  /  2 ) ) )
126 f1of 5709 . . . . . . . . . . 11  |-  ( `' S : ( -u
1 [,] 1 ) -1-1-onto-> (
-u ( pi  / 
2 ) [,] (
pi  /  2 ) )  ->  `' S : ( -u 1 [,] 1 ) --> ( -u ( pi  /  2
) [,] ( pi 
/  2 ) ) )
127124, 125, 126mp2b 10 . . . . . . . . . 10  |-  `' S : ( -u 1 [,] 1 ) --> ( -u ( pi  /  2
) [,] ( pi 
/  2 ) )
128127ffvelrni 5905 . . . . . . . . 9  |-  ( ( Im `  ( sqr `  x ) )  e.  ( -u 1 [,] 1 )  ->  ( `' S `  ( Im
`  ( sqr `  x
) ) )  e.  ( -u ( pi 
/  2 ) [,] ( pi  /  2
) ) )
129119, 128syl 16 . . . . . . . 8  |-  ( (
ph  /\  x  e.  C )  ->  ( `' S `  ( Im
`  ( sqr `  x
) ) )  e.  ( -u ( pi 
/  2 ) [,] ( pi  /  2
) ) )
130118, 129sseldi 3335 . . . . . . 7  |-  ( (
ph  /\  x  e.  C )  ->  ( `' S `  ( Im
`  ( sqr `  x
) ) )  e.  RR )
131 remulcl 9113 . . . . . . 7  |-  ( ( 2  e.  RR  /\  ( `' S `  ( Im
`  ( sqr `  x
) ) )  e.  RR )  ->  (
2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  e.  RR )
13229, 130, 131sylancr 646 . . . . . 6  |-  ( (
ph  /\  x  e.  C )  ->  (
2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  e.  RR )
133 efif1olem4.5 . . . . . . . 8  |-  ( (
ph  /\  z  e.  RR )  ->  E. y  e.  D  ( (
z  -  y )  /  ( 2  x.  pi ) )  e.  ZZ )
134133ralrimiva 2796 . . . . . . 7  |-  ( ph  ->  A. z  e.  RR  E. y  e.  D  ( ( z  -  y
)  /  ( 2  x.  pi ) )  e.  ZZ )
135134adantr 453 . . . . . 6  |-  ( (
ph  /\  x  e.  C )  ->  A. z  e.  RR  E. y  e.  D  ( ( z  -  y )  / 
( 2  x.  pi ) )  e.  ZZ )
136 oveq1 6124 . . . . . . . . . 10  |-  ( z  =  ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) )  ->  ( z  -  y )  =  ( ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) )  -  y ) )
137136oveq1d 6132 . . . . . . . . 9  |-  ( z  =  ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) )  ->  ( (
z  -  y )  /  ( 2  x.  pi ) )  =  ( ( ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) )  -  y
)  /  ( 2  x.  pi ) ) )
138137eleq1d 2509 . . . . . . . 8  |-  ( z  =  ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) )  ->  ( (
( z  -  y
)  /  ( 2  x.  pi ) )  e.  ZZ  <->  ( (
( 2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y )  / 
( 2  x.  pi ) )  e.  ZZ ) )
139138rexbidv 2733 . . . . . . 7  |-  ( z  =  ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) )  ->  ( E. y  e.  D  (
( z  -  y
)  /  ( 2  x.  pi ) )  e.  ZZ  <->  E. y  e.  D  ( (
( 2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y )  / 
( 2  x.  pi ) )  e.  ZZ ) )
140139rspcv 3057 . . . . . 6  |-  ( ( 2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  e.  RR  ->  ( A. z  e.  RR  E. y  e.  D  ( ( z  -  y
)  /  ( 2  x.  pi ) )  e.  ZZ  ->  E. y  e.  D  ( (
( 2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y )  / 
( 2  x.  pi ) )  e.  ZZ ) )
141132, 135, 140sylc 59 . . . . 5  |-  ( (
ph  /\  x  e.  C )  ->  E. y  e.  D  ( (
( 2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y )  / 
( 2  x.  pi ) )  e.  ZZ )
142 oveq1 6124 . . . . . . . 8  |-  ( ( exp `  ( _i  x.  ( ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) )  -  y
) ) )  =  1  ->  ( ( exp `  ( _i  x.  ( ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) )  -  y ) ) )  x.  ( exp `  ( _i  x.  y ) ) )  =  ( 1  x.  ( exp `  (
_i  x.  y )
) ) )
1433a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  _i  e.  CC )
144132adantr 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  (
2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  e.  RR )
145144recnd 9152 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  (
2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  e.  CC )
1461ad2antrr 708 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  D  C_  RR )
147 simpr 449 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  y  e.  D )
148146, 147sseldd 3338 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  y  e.  RR )
149148recnd 9152 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  y  e.  CC )
150143, 145, 149subdid 9527 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  (
_i  x.  ( (
2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y ) )  =  ( ( _i  x.  ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) ) )  -  (
_i  x.  y )
) )
151150oveq1d 6132 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  (
( _i  x.  (
( 2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y ) )  +  ( _i  x.  y ) )  =  ( ( ( _i  x.  ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) ) )  -  (
_i  x.  y )
)  +  ( _i  x.  y ) ) )
152 mulcl 9112 . . . . . . . . . . . . . 14  |-  ( ( _i  e.  CC  /\  ( 2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  e.  CC )  -> 
( _i  x.  (
2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) )  e.  CC )
1533, 145, 152sylancr 646 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  (
_i  x.  ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) ) )  e.  CC )
1543, 149, 72sylancr 646 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  (
_i  x.  y )  e.  CC )
155153, 154npcand 9453 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  (
( ( _i  x.  ( 2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) )  -  ( _i  x.  y ) )  +  ( _i  x.  y ) )  =  ( _i  x.  (
2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) ) )
156151, 155eqtrd 2475 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  (
( _i  x.  (
( 2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y ) )  +  ( _i  x.  y ) )  =  ( _i  x.  (
2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) ) )
157156fveq2d 5767 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  ( exp `  ( ( _i  x.  ( ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) )  -  y
) )  +  ( _i  x.  y ) ) )  =  ( exp `  ( _i  x.  ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) ) ) ) )
158145, 149subcld 9449 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  (
( 2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y )  e.  CC )
159 mulcl 9112 . . . . . . . . . . . 12  |-  ( ( _i  e.  CC  /\  ( ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) )  -  y )  e.  CC )  -> 
( _i  x.  (
( 2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y ) )  e.  CC )
1603, 158, 159sylancr 646 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  (
_i  x.  ( (
2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y ) )  e.  CC )
161 efadd 12734 . . . . . . . . . . 11  |-  ( ( ( _i  x.  (
( 2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y ) )  e.  CC  /\  (
_i  x.  y )  e.  CC )  ->  ( exp `  ( ( _i  x.  ( ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) )  -  y
) )  +  ( _i  x.  y ) ) )  =  ( ( exp `  (
_i  x.  ( (
2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y ) ) )  x.  ( exp `  ( _i  x.  y
) ) ) )
162160, 154, 161syl2anc 644 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  ( exp `  ( ( _i  x.  ( ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) )  -  y
) )  +  ( _i  x.  y ) ) )  =  ( ( exp `  (
_i  x.  ( (
2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y ) ) )  x.  ( exp `  ( _i  x.  y
) ) ) )
163130recnd 9152 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  C )  ->  ( `' S `  ( Im
`  ( sqr `  x
) ) )  e.  CC )
164 2cn 10108 . . . . . . . . . . . . . . . 16  |-  2  e.  CC
165 mul12 9270 . . . . . . . . . . . . . . . 16  |-  ( ( _i  e.  CC  /\  2  e.  CC  /\  ( `' S `  ( Im
`  ( sqr `  x
) ) )  e.  CC )  ->  (
_i  x.  ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) ) )  =  ( 2  x.  (
_i  x.  ( `' S `  ( Im `  ( sqr `  x
) ) ) ) ) )
1663, 164, 165mp3an12 1270 . . . . . . . . . . . . . . 15  |-  ( ( `' S `  ( Im
`  ( sqr `  x
) ) )  e.  CC  ->  ( _i  x.  ( 2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) )  =  ( 2  x.  ( _i  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) ) )
167163, 166syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  C )  ->  (
_i  x.  ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) ) )  =  ( 2  x.  (
_i  x.  ( `' S `  ( Im `  ( sqr `  x
) ) ) ) ) )
168167fveq2d 5767 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  C )  ->  ( exp `  ( _i  x.  ( 2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) ) )  =  ( exp `  ( 2  x.  ( _i  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) ) ) )
169 mulcl 9112 . . . . . . . . . . . . . . 15  |-  ( ( _i  e.  CC  /\  ( `' S `  ( Im
`  ( sqr `  x
) ) )  e.  CC )  ->  (
_i  x.  ( `' S `  ( Im `  ( sqr `  x
) ) ) )  e.  CC )
1703, 163, 169sylancr 646 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  C )  ->  (
_i  x.  ( `' S `  ( Im `  ( sqr `  x
) ) ) )  e.  CC )
171 2z 10350 . . . . . . . . . . . . . 14  |-  2  e.  ZZ
172 efexp 12740 . . . . . . . . . . . . . 14  |-  ( ( ( _i  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  e.  CC  /\  2  e.  ZZ )  ->  ( exp `  ( 2  x.  ( _i  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) ) )  =  ( ( exp `  (
_i  x.  ( `' S `  ( Im `  ( sqr `  x
) ) ) ) ) ^ 2 ) )
173170, 171, 172sylancl 645 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  C )  ->  ( exp `  ( 2  x.  ( _i  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) ) )  =  ( ( exp `  (
_i  x.  ( `' S `  ( Im `  ( sqr `  x
) ) ) ) ) ^ 2 ) )
174168, 173eqtrd 2475 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  C )  ->  ( exp `  ( _i  x.  ( 2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) ) )  =  ( ( exp `  (
_i  x.  ( `' S `  ( Im `  ( sqr `  x
) ) ) ) ) ^ 2 ) )
175130recoscld 12783 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  C )  ->  ( cos `  ( `' S `  ( Im `  ( sqr `  x ) ) ) )  e.  RR )
176 simpr 449 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  C )  ->  x  e.  C )
177176, 16syl6eleq 2533 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  C )  ->  x  e.  ( `' abs " {
1 } ) )
178 fniniseg 5887 . . . . . . . . . . . . . . . . . . . . 21  |-  ( abs 
Fn  CC  ->  ( x  e.  ( `' abs " { 1 } )  <-> 
( x  e.  CC  /\  ( abs `  x
)  =  1 ) ) )
17912, 178ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( `' abs " { 1 } )  <-> 
( x  e.  CC  /\  ( abs `  x
)  =  1 ) )
180177, 179sylib 190 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  C )  ->  (
x  e.  CC  /\  ( abs `  x )  =  1 ) )
181180simpld 447 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  C )  ->  x  e.  CC )
182181sqrcld 12277 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  C )  ->  ( sqr `  x )  e.  CC )
183182recld 12037 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  C )  ->  (
Re `  ( sqr `  x ) )  e.  RR )
184 cosq14ge0 20457 . . . . . . . . . . . . . . . . 17  |-  ( ( `' S `  ( Im
`  ( sqr `  x
) ) )  e.  ( -u ( pi 
/  2 ) [,] ( pi  /  2
) )  ->  0  <_  ( cos `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) )
185129, 184syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  C )  ->  0  <_  ( cos `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) )
186181sqrrege0d 12278 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  C )  ->  0  <_  ( Re `  ( sqr `  x ) ) )
187 sincossq 12815 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( `' S `  ( Im
`  ( sqr `  x
) ) )  e.  CC  ->  ( (
( sin `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) ^ 2 )  +  ( ( cos `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) ^ 2 ) )  =  1 )
188163, 187syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  C )  ->  (
( ( sin `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) ^ 2 )  +  ( ( cos `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) ^ 2 ) )  =  1 )
189181sqsqrd 12279 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  C )  ->  (
( sqr `  x
) ^ 2 )  =  x )
190189fveq2d 5767 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  C )  ->  ( abs `  ( ( sqr `  x ) ^ 2 ) )  =  ( abs `  x ) )
191 2nn0 10276 . . . . . . . . . . . . . . . . . . . . 21  |-  2  e.  NN0
192 absexp 12147 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( sqr `  x
)  e.  CC  /\  2  e.  NN0 )  -> 
( abs `  (
( sqr `  x
) ^ 2 ) )  =  ( ( abs `  ( sqr `  x ) ) ^
2 ) )
193182, 191, 192sylancl 645 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  C )  ->  ( abs `  ( ( sqr `  x ) ^ 2 ) )  =  ( ( abs `  ( sqr `  x ) ) ^ 2 ) )
194180simprd 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  C )  ->  ( abs `  x )  =  1 )
195190, 193, 1943eqtr3d 2483 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  C )  ->  (
( abs `  ( sqr `  x ) ) ^ 2 )  =  1 )
196182absvalsq2d 12283 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  C )  ->  (
( abs `  ( sqr `  x ) ) ^ 2 )  =  ( ( ( Re
`  ( sqr `  x
) ) ^ 2 )  +  ( ( Im `  ( sqr `  x ) ) ^
2 ) ) )
197188, 195, 1963eqtr2d 2481 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  C )  ->  (
( ( sin `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) ^ 2 )  +  ( ( cos `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) ^ 2 ) )  =  ( ( ( Re `  ( sqr `  x ) ) ^
2 )  +  ( ( Im `  ( sqr `  x ) ) ^ 2 ) ) )
198121fveq1i 5764 . . . . . . . . . . . . . . . . . . . . 21  |-  ( S `
 ( `' S `  ( Im `  ( sqr `  x ) ) ) )  =  ( ( sin  |`  ( -u ( pi  /  2
) [,] ( pi 
/  2 ) ) ) `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )
199 fvres 5776 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( `' S `  ( Im
`  ( sqr `  x
) ) )  e.  ( -u ( pi 
/  2 ) [,] ( pi  /  2
) )  ->  (
( sin  |`  ( -u ( pi  /  2
) [,] ( pi 
/  2 ) ) ) `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  =  ( sin `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) )
200129, 199syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  C )  ->  (
( sin  |`  ( -u ( pi  /  2
) [,] ( pi 
/  2 ) ) ) `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  =  ( sin `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) )
201198, 200syl5eq 2487 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  C )  ->  ( S `  ( `' S `  ( Im `  ( sqr `  x
) ) ) )  =  ( sin `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) )
202 f1ocnvfv2 6051 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( S : ( -u ( pi  /  2
) [,] ( pi 
/  2 ) ) -1-1-onto-> (
-u 1 [,] 1
)  /\  ( Im `  ( sqr `  x
) )  e.  (
-u 1 [,] 1
) )  ->  ( S `  ( `' S `  ( Im `  ( sqr `  x
) ) ) )  =  ( Im `  ( sqr `  x ) ) )
203124, 119, 202sylancr 646 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  C )  ->  ( S `  ( `' S `  ( Im `  ( sqr `  x
) ) ) )  =  ( Im `  ( sqr `  x ) ) )
204201, 203eqtr3d 2477 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  C )  ->  ( sin `  ( `' S `  ( Im `  ( sqr `  x ) ) ) )  =  ( Im `  ( sqr `  x ) ) )
205204oveq1d 6132 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  C )  ->  (
( sin `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) ^ 2 )  =  ( ( Im `  ( sqr `  x ) ) ^ 2 ) )
206197, 205oveq12d 6135 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  C )  ->  (
( ( ( sin `  ( `' S `  ( Im `  ( sqr `  x ) ) ) ) ^ 2 )  +  ( ( cos `  ( `' S `  ( Im `  ( sqr `  x ) ) ) ) ^ 2 ) )  -  ( ( sin `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) ^ 2 ) )  =  ( ( ( ( Re `  ( sqr `  x ) ) ^ 2 )  +  ( ( Im `  ( sqr `  x ) ) ^ 2 ) )  -  ( ( Im `  ( sqr `  x ) ) ^
2 ) ) )
207163sincld 12769 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  C )  ->  ( sin `  ( `' S `  ( Im `  ( sqr `  x ) ) ) )  e.  CC )
208207sqcld 11559 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  C )  ->  (
( sin `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) ^ 2 )  e.  CC )
209163coscld 12770 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  C )  ->  ( cos `  ( `' S `  ( Im `  ( sqr `  x ) ) ) )  e.  CC )
210209sqcld 11559 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  C )  ->  (
( cos `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) ^ 2 )  e.  CC )
211208, 210pncan2d 9451 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  C )  ->  (
( ( ( sin `  ( `' S `  ( Im `  ( sqr `  x ) ) ) ) ^ 2 )  +  ( ( cos `  ( `' S `  ( Im `  ( sqr `  x ) ) ) ) ^ 2 ) )  -  ( ( sin `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) ^ 2 ) )  =  ( ( cos `  ( `' S `  ( Im `  ( sqr `  x ) ) ) ) ^ 2 ) )
212183recnd 9152 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  C )  ->  (
Re `  ( sqr `  x ) )  e.  CC )
213212sqcld 11559 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  C )  ->  (
( Re `  ( sqr `  x ) ) ^ 2 )  e.  CC )
214205, 208eqeltrrd 2518 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  C )  ->  (
( Im `  ( sqr `  x ) ) ^ 2 )  e.  CC )
215213, 214pncand 9450 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  C )  ->  (
( ( ( Re
`  ( sqr `  x
) ) ^ 2 )  +  ( ( Im `  ( sqr `  x ) ) ^
2 ) )  -  ( ( Im `  ( sqr `  x ) ) ^ 2 ) )  =  ( ( Re `  ( sqr `  x ) ) ^
2 ) )
216206, 211, 2153eqtr3d 2483 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  C )  ->  (
( cos `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) ^ 2 )  =  ( ( Re `  ( sqr `  x ) ) ^ 2 ) )
217175, 183, 185, 186, 216sq11d 11597 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  C )  ->  ( cos `  ( `' S `  ( Im `  ( sqr `  x ) ) ) )  =  ( Re `  ( sqr `  x ) ) )
218204oveq2d 6133 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  C )  ->  (
_i  x.  ( sin `  ( `' S `  ( Im `  ( sqr `  x ) ) ) ) )  =  ( _i  x.  ( Im
`  ( sqr `  x
) ) ) )
219217, 218oveq12d 6135 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  C )  ->  (
( cos `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  +  ( _i  x.  ( sin `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) ) )  =  ( ( Re `  ( sqr `  x ) )  +  ( _i  x.  ( Im `  ( sqr `  x ) ) ) ) )
220 efival 12791 . . . . . . . . . . . . . . 15  |-  ( ( `' S `  ( Im
`  ( sqr `  x
) ) )  e.  CC  ->  ( exp `  ( _i  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) )  =  ( ( cos `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  +  ( _i  x.  ( sin `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) ) ) )
221163, 220syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  C )  ->  ( exp `  ( _i  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) )  =  ( ( cos `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  +  ( _i  x.  ( sin `  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) ) ) )
222182replimd 12040 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  C )  ->  ( sqr `  x )  =  ( ( Re `  ( sqr `  x ) )  +  ( _i  x.  ( Im `  ( sqr `  x ) ) ) ) )
223219, 221, 2223eqtr4d 2485 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  C )  ->  ( exp `  ( _i  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) )  =  ( sqr `  x ) )
224223oveq1d 6132 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  C )  ->  (
( exp `  (
_i  x.  ( `' S `  ( Im `  ( sqr `  x
) ) ) ) ) ^ 2 )  =  ( ( sqr `  x ) ^ 2 ) )
225174, 224, 1893eqtrd 2479 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  C )  ->  ( exp `  ( _i  x.  ( 2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) ) )  =  x )
226225adantr 453 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  ( exp `  ( _i  x.  ( 2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) ) ) )  =  x )
227157, 162, 2263eqtr3d 2483 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  (
( exp `  (
_i  x.  ( (
2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y ) ) )  x.  ( exp `  ( _i  x.  y
) ) )  =  x )
228154, 76syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  ( exp `  ( _i  x.  y ) )  e.  CC )
229228mulid2d 9144 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  (
1  x.  ( exp `  ( _i  x.  y
) ) )  =  ( exp `  (
_i  x.  y )
) )
230227, 229eqeq12d 2457 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  (
( ( exp `  (
_i  x.  ( (
2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y ) ) )  x.  ( exp `  ( _i  x.  y
) ) )  =  ( 1  x.  ( exp `  ( _i  x.  y ) ) )  <-> 
x  =  ( exp `  ( _i  x.  y
) ) ) )
231142, 230syl5ib 212 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  (
( exp `  (
_i  x.  ( (
2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y ) ) )  =  1  ->  x  =  ( exp `  ( _i  x.  y
) ) ) )
232 efeq1 20469 . . . . . . . . 9  |-  ( ( _i  x.  ( ( 2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y ) )  e.  CC  ->  (
( exp `  (
_i  x.  ( (
2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y ) ) )  =  1  <->  (
( _i  x.  (
( 2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y ) )  /  ( _i  x.  ( 2  x.  pi ) ) )  e.  ZZ ) )
233160, 232syl 16 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  (
( exp `  (
_i  x.  ( (
2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y ) ) )  =  1  <->  (
( _i  x.  (
( 2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y ) )  /  ( _i  x.  ( 2  x.  pi ) ) )  e.  ZZ ) )
234 divcan5 9754 . . . . . . . . . . 11  |-  ( ( ( ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) )  -  y )  e.  CC  /\  (
( 2  x.  pi )  e.  CC  /\  (
2  x.  pi )  =/=  0 )  /\  ( _i  e.  CC  /\  _i  =/=  0 ) )  ->  ( (
_i  x.  ( (
2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y ) )  /  ( _i  x.  ( 2  x.  pi ) ) )  =  ( ( ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) )  -  y
)  /  ( 2  x.  pi ) ) )
23561, 63, 234mp3an23 1272 . . . . . . . . . 10  |-  ( ( ( 2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y )  e.  CC  ->  ( (
_i  x.  ( (
2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y ) )  /  ( _i  x.  ( 2  x.  pi ) ) )  =  ( ( ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) )  -  y
)  /  ( 2  x.  pi ) ) )
236158, 235syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  (
( _i  x.  (
( 2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y ) )  /  ( _i  x.  ( 2  x.  pi ) ) )  =  ( ( ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) )  -  y
)  /  ( 2  x.  pi ) ) )
237236eleq1d 2509 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  (
( ( _i  x.  ( ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) )  -  y ) )  /  ( _i  x.  ( 2  x.  pi ) ) )  e.  ZZ  <->  ( (
( 2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y )  / 
( 2  x.  pi ) )  e.  ZZ ) )
238233, 237bitr2d 247 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  (
( ( ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) )  -  y
)  /  ( 2  x.  pi ) )  e.  ZZ  <->  ( exp `  ( _i  x.  (
( 2  x.  ( `' S `  ( Im
`  ( sqr `  x
) ) ) )  -  y ) ) )  =  1 ) )
23989adantl 454 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  ( F `  y )  =  ( exp `  (
_i  x.  y )
) )
240239eqeq2d 2454 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  (
x  =  ( F `
 y )  <->  x  =  ( exp `  ( _i  x.  y ) ) ) )
241231, 238, 2403imtr4d 261 . . . . . 6  |-  ( ( ( ph  /\  x  e.  C )  /\  y  e.  D )  ->  (
( ( ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) )  -  y
)  /  ( 2  x.  pi ) )  e.  ZZ  ->  x  =  ( F `  y ) ) )
242241reximdva 2825 . . . . 5  |-  ( (
ph  /\  x  e.  C )  ->  ( E. y  e.  D  ( ( ( 2  x.  ( `' S `  ( Im `  ( sqr `  x ) ) ) )  -  y
)  /  ( 2  x.  pi ) )  e.  ZZ  ->  E. y  e.  D  x  =  ( F `  y ) ) )
243141, 242mpd 15 . . . 4  |-  ( (
ph  /\  x  e.  C )  ->  E. y  e.  D  x  =  ( F `  y ) )
244243ralrimiva 2796 . . 3  |-  ( ph  ->  A. x  e.  C  E. y  e.  D  x  =  ( F `  y ) )
245 dffo3 5920 . . 3  |-  ( F : D -onto-> C  <->  ( F : D --> C  /\  A. x  e.  C  E. y  e.  D  x  =  ( F `  y ) ) )
24620, 244, 245sylanbrc 647 . 2  |-  ( ph  ->  F : D -onto-> C
)
247 df-f1o 5496 . 2  |-  ( F : D -1-1-onto-> C  <->  ( F : D -1-1-> C  /\  F : D -onto-> C ) )
248114, 246, 247sylanbrc 647 1  |-  ( ph  ->  F : D -1-1-onto-> C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1654    e. wcel 1728    =/= wne 2606   A.wral 2712   E.wrex 2713    C_ wss 3309   {csn 3843   class class class wbr 4243    e. cmpt 4297   `'ccnv 4912    |` cres 4915   "cima 4916    Fn wfn 5484   -->wf 5485   -1-1->wf1 5486   -onto->wfo 5487   -1-1-onto->wf1o 5488   ` cfv 5489  (class class class)co 6117   CCcc 9026   RRcr 9027   0cc0 9028   1c1 9029   _ici 9030    + caddc 9031    x. cmul 9033    < clt 9158    <_ cle 9159    - cmin 9329   -ucneg 9330    / cdiv 9715   2c2 10087   NN0cn0 10259   ZZcz 10320   [,]cicc 10957   ^cexp 11420   Recre 11940   Imcim 11941   sqrcsqr 12076   abscabs 12077   expce 12702   sincsin 12704   cosccos 12705   picpi 12707
This theorem is referenced by:  efif1o  20486  eff1olem  20488
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-rep 4351  ax-sep 4361  ax-nul 4369  ax-pow 4412  ax-pr 4438  ax-un 4736  ax-inf2 7632  ax-cnex 9084  ax-resscn 9085  ax-1cn 9086  ax-icn 9087  ax-addcl 9088  ax-addrcl 9089  ax-mulcl 9090  ax-mulrcl 9091  ax-mulcom 9092  ax-addass 9093  ax-mulass 9094  ax-distr 9095  ax-i2m1 9096  ax-1ne0 9097  ax-1rid 9098  ax-rnegex 9099  ax-rrecex 9100  ax-cnre 9101  ax-pre-lttri 9102  ax-pre-lttrn 9103  ax-pre-ltadd 9104  ax-pre-mulgt0 9105  ax-pre-sup 9106  ax-addf 9107  ax-mulf 9108
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-fal 1330  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2292  df-mo 2293  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-nel 2609  df-ral 2717  df-rex 2718  df-reu 2719  df-rmo 2720  df-rab 2721  df-v 2967  df-sbc 3171  df-csb 3271  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-pss 3325  df-nul 3617  df-if 3768  df-pw 3830  df-sn 3849  df-pr 3850  df-tp 3851  df-op 3852  df-uni 4045  df-int 4080  df-iun 4124  df-iin 4125  df-br 4244  df-opab 4298  df-mpt 4299  df-tr 4334  df-eprel 4529  df-id 4533  df-po 4538  df-so 4539  df-fr 4576  df-se 4577  df-we 4578  df-ord 4619  df-on 4620  df-lim 4621  df-suc 4622  df-om 4881  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5453  df-fun 5491  df-fn 5492  df-f 5493  df-f1 5494  df-fo 5495  df-f1o 5496  df-fv 5497  df-isom 5498  df-ov 6120  df-oprab 6121  df-mpt2 6122  df-of 6341  df-1st 6385  df-2nd 6386  df-riota 6585  df-recs 6669  df-rdg 6704  df-1o 6760  df-2o 6761  df-oadd 6764  df-er 6941  df-map 7056  df-pm 7057  df-ixp 7100  df-en 7146  df-dom 7147  df-sdom 7148  df-fin 7149  df-fi 7452  df-sup 7482  df-oi 7515  df-card 7864  df-cda 8086  df-pnf 9160  df-mnf 9161  df-xr 9162  df-ltxr 9163  df-le 9164  df-sub 9331  df-neg 9332  df-div 9716  df-nn 10039  df-2 10096  df-3 10097  df-4 10098  df-5 10099  df-6 10100  df-7 10101  df-8 10102  df-9 10103  df-10 10104  df-n0 10260  df-z 10321  df-dec 10421  df-uz 10527  df-q 10613  df-rp 10651  df-xneg 10748  df-xadd 10749  df-xmul 10750  df-ioo 10958  df-ioc 10959  df-ico 10960  df-icc 10961  df-fz 11082  df-fzo 11174  df-fl 11240  df-mod 11289  df-seq 11362  df-exp 11421  df-fac 11605  df-bc 11632  df-hash 11657  df-shft 11920  df-cj 11942  df-re 11943  df-im 11944  df-sqr 12078  df-abs 12079  df-limsup 12303  df-clim 12320  df-rlim 12321  df-sum 12518  df-ef 12708  df-sin 12710  df-cos 12711  df-pi 12713  df-struct 13509  df-ndx 13510  df-slot 13511  df-base 13512  df-sets 13513  df-ress 13514  df-plusg 13580  df-mulr 13581  df-starv 13582  df-sca 13583  df-vsca 13584  df-tset 13586  df-ple 13587  df-ds 13589  df-unif 13590  df-hom 13591  df-cco 13592  df-rest 13688  df-topn 13689  df-topgen 13705  df-pt 13706  df-prds 13709  df-xrs 13764  df-0g 13765  df-gsum 13766  df-qtop 13771  df-imas 13772  df-xps 13774  df-mre 13849  df-mrc 13850  df-acs 13852  df-mnd 14728  df-submnd 14777  df-mulg 14853  df-cntz 15154  df-cmn 15452  df-psmet 16732  df-xmet 16733  df-met 16734  df-bl 16735  df-mopn 16736  df-fbas 16737  df-fg 16738  df-cnfld 16742  df-top 17001  df-bases 17003  df-topon 17004  df-topsp 17005  df-cld 17121  df-ntr 17122  df-cls 17123  df-nei 17200  df-lp 17238  df-perf 17239  df-cn 17329  df-cnp 17330  df-haus 17417  df-tx 17632  df-hmeo 17825  df-fil 17916  df-fm 18008  df-flim 18009  df-flf 18010  df-xms 18388  df-ms 18389  df-tms 18390  df-cncf 18946  df-limc 19791  df-dv 19792
  Copyright terms: Public domain W3C validator