Step |
Hyp |
Ref |
Expression |
1 |
|
eff1o.1 |
|- S = ( `' Im " ( -u _pi (,] _pi ) ) |
2 |
|
pire |
|- _pi e. RR |
3 |
2
|
renegcli |
|- -u _pi e. RR |
4 |
|
eqid |
|- ( w e. ( -u _pi (,] _pi ) |-> ( exp ` ( _i x. w ) ) ) = ( w e. ( -u _pi (,] _pi ) |-> ( exp ` ( _i x. w ) ) ) |
5 |
|
rexr |
|- ( -u _pi e. RR -> -u _pi e. RR* ) |
6 |
|
iocssre |
|- ( ( -u _pi e. RR* /\ _pi e. RR ) -> ( -u _pi (,] _pi ) C_ RR ) |
7 |
5 2 6
|
sylancl |
|- ( -u _pi e. RR -> ( -u _pi (,] _pi ) C_ RR ) |
8 |
|
picn |
|- _pi e. CC |
9 |
8
|
2timesi |
|- ( 2 x. _pi ) = ( _pi + _pi ) |
10 |
9
|
oveq2i |
|- ( -u _pi + ( 2 x. _pi ) ) = ( -u _pi + ( _pi + _pi ) ) |
11 |
|
negpicn |
|- -u _pi e. CC |
12 |
8 8
|
addcli |
|- ( _pi + _pi ) e. CC |
13 |
11 12
|
addcomi |
|- ( -u _pi + ( _pi + _pi ) ) = ( ( _pi + _pi ) + -u _pi ) |
14 |
12 8
|
negsubi |
|- ( ( _pi + _pi ) + -u _pi ) = ( ( _pi + _pi ) - _pi ) |
15 |
8 8
|
pncan3oi |
|- ( ( _pi + _pi ) - _pi ) = _pi |
16 |
14 15
|
eqtri |
|- ( ( _pi + _pi ) + -u _pi ) = _pi |
17 |
10 13 16
|
3eqtrri |
|- _pi = ( -u _pi + ( 2 x. _pi ) ) |
18 |
17
|
oveq2i |
|- ( -u _pi (,] _pi ) = ( -u _pi (,] ( -u _pi + ( 2 x. _pi ) ) ) |
19 |
18
|
efif1olem1 |
|- ( ( -u _pi e. RR /\ ( x e. ( -u _pi (,] _pi ) /\ y e. ( -u _pi (,] _pi ) ) ) -> ( abs ` ( x - y ) ) < ( 2 x. _pi ) ) |
20 |
18
|
efif1olem2 |
|- ( ( -u _pi e. RR /\ z e. RR ) -> E. y e. ( -u _pi (,] _pi ) ( ( z - y ) / ( 2 x. _pi ) ) e. ZZ ) |
21 |
4 1 7 19 20
|
eff1olem |
|- ( -u _pi e. RR -> ( exp |` S ) : S -1-1-onto-> ( CC \ { 0 } ) ) |
22 |
3 21
|
ax-mp |
|- ( exp |` S ) : S -1-1-onto-> ( CC \ { 0 } ) |