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 | |
|
Assertion | eff1o | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eff1o.1 | |
|
2 | pire | |
|
3 | 2 | renegcli | |
4 | eqid | |
|
5 | rexr | |
|
6 | iocssre | |
|
7 | 5 2 6 | sylancl | |
8 | picn | |
|
9 | 8 | 2timesi | |
10 | 9 | oveq2i | |
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 | |
18 | 17 | oveq2i | |
19 | 18 | efif1olem1 | |
20 | 18 | efif1olem2 | |
21 | 4 1 7 19 20 | eff1olem | |
22 | 3 21 | ax-mp | |