# 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}={\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]$
Assertion eff1o ${⊢}\left({\mathrm{exp}↾}_{{S}}\right):{S}\underset{1-1 onto}{⟶}ℂ\setminus \left\{0\right\}$

### Proof

Step Hyp Ref Expression
1 eff1o.1 ${⊢}{S}={\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]$
2 pire ${⊢}\mathrm{\pi }\in ℝ$
3 2 renegcli ${⊢}-\mathrm{\pi }\in ℝ$
4 eqid ${⊢}\left({w}\in \left(-\mathrm{\pi },\mathrm{\pi }\right]⟼{\mathrm{e}}^{\mathrm{i}{w}}\right)=\left({w}\in \left(-\mathrm{\pi },\mathrm{\pi }\right]⟼{\mathrm{e}}^{\mathrm{i}{w}}\right)$
5 rexr ${⊢}-\mathrm{\pi }\in ℝ\to -\mathrm{\pi }\in {ℝ}^{*}$
6 iocssre ${⊢}\left(-\mathrm{\pi }\in {ℝ}^{*}\wedge \mathrm{\pi }\in ℝ\right)\to \left(-\mathrm{\pi },\mathrm{\pi }\right]\subseteq ℝ$
7 5 2 6 sylancl ${⊢}-\mathrm{\pi }\in ℝ\to \left(-\mathrm{\pi },\mathrm{\pi }\right]\subseteq ℝ$
8 picn ${⊢}\mathrm{\pi }\in ℂ$
9 8 2timesi ${⊢}2\mathrm{\pi }=\mathrm{\pi }+\mathrm{\pi }$
10 9 oveq2i ${⊢}-\mathrm{\pi }+2\mathrm{\pi }=\left(-\mathrm{\pi }\right)+\mathrm{\pi }+\mathrm{\pi }$
11 negpicn ${⊢}-\mathrm{\pi }\in ℂ$
12 8 8 addcli ${⊢}\mathrm{\pi }+\mathrm{\pi }\in ℂ$
13 11 12 addcomi ${⊢}\left(-\mathrm{\pi }\right)+\mathrm{\pi }+\mathrm{\pi }=\mathrm{\pi }+\mathrm{\pi }+\left(-\mathrm{\pi }\right)$
14 12 8 negsubi ${⊢}\mathrm{\pi }+\mathrm{\pi }+\left(-\mathrm{\pi }\right)=\mathrm{\pi }+\mathrm{\pi }-\mathrm{\pi }$
15 8 8 pncan3oi ${⊢}\mathrm{\pi }+\mathrm{\pi }-\mathrm{\pi }=\mathrm{\pi }$
16 14 15 eqtri ${⊢}\mathrm{\pi }+\mathrm{\pi }+\left(-\mathrm{\pi }\right)=\mathrm{\pi }$
17 10 13 16 3eqtrri ${⊢}\mathrm{\pi }=-\mathrm{\pi }+2\mathrm{\pi }$
18 17 oveq2i ${⊢}\left(-\mathrm{\pi },\mathrm{\pi }\right]=\left(-\mathrm{\pi },-\mathrm{\pi }+2\mathrm{\pi }\right]$
19 18 efif1olem1 ${⊢}\left(-\mathrm{\pi }\in ℝ\wedge \left({x}\in \left(-\mathrm{\pi },\mathrm{\pi }\right]\wedge {y}\in \left(-\mathrm{\pi },\mathrm{\pi }\right]\right)\right)\to \left|{x}-{y}\right|<2\mathrm{\pi }$
20 18 efif1olem2 ${⊢}\left(-\mathrm{\pi }\in ℝ\wedge {z}\in ℝ\right)\to \exists {y}\in \left(-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\frac{{z}-{y}}{2\mathrm{\pi }}\in ℤ$
21 4 1 7 19 20 eff1olem ${⊢}-\mathrm{\pi }\in ℝ\to \left({\mathrm{exp}↾}_{{S}}\right):{S}\underset{1-1 onto}{⟶}ℂ\setminus \left\{0\right\}$
22 3 21 ax-mp ${⊢}\left({\mathrm{exp}↾}_{{S}}\right):{S}\underset{1-1 onto}{⟶}ℂ\setminus \left\{0\right\}$