Metamath Proof Explorer


Theorem eff1o

Description: The exponential function maps the set S , of complex numbers with imaginary part in the closed-above, open-below interval from -upi to pi one-to-one onto the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008) (Revised by Mario Carneiro, 13-May-2014)

Ref Expression
Hypothesis eff1o.1 S=-1ππ
Assertion eff1o expS:S1-1 onto0

Proof

Step Hyp Ref Expression
1 eff1o.1 S=-1ππ
2 pire π
3 2 renegcli π
4 eqid wππeiw=wππeiw
5 rexr ππ*
6 iocssre π*πππ
7 5 2 6 sylancl πππ
8 picn π
9 8 2timesi 2π=π+π
10 9 oveq2i -π+2π=π+π+π
11 negpicn π
12 8 8 addcli π+π
13 11 12 addcomi π+π+π=π+π+π
14 12 8 negsubi π+π+π=π+π-π
15 8 8 pncan3oi π+π-π=π
16 14 15 eqtri π+π+π=π
17 10 13 16 3eqtrri π=-π+2π
18 17 oveq2i ππ=π-π+2π
19 18 efif1olem1 πxππyππxy<2π
20 18 efif1olem2 πzyππzy2π
21 4 1 7 19 20 eff1olem πexpS:S1-1 onto0
22 3 21 ax-mp expS:S1-1 onto0