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 ⊢ exp ↾ S : S ⟶ 1-1 onto ℂ ∖ 0

Proof

Step Hyp Ref Expression
1 eff1o.1 ⊢ S = ℑ -1 − π π
2 pire ⊢ π ∈ ℝ
3 2 renegcli ⊢ − π ∈ ℝ
4 eqid ⊢ w ∈ − π π ⟼ e i ⁢ w = w ∈ − π π ⟼ e i ⁢ w
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 ∈ − π π → x − y < 2 ⁢ π
20 18 efif1olem2 ⊢ − π ∈ ℝ ∧ z ∈ ℝ → ∃ y ∈ − π π z − y 2 ⁢ π ∈ ℤ
21 4 1 7 19 20 eff1olem ⊢ − π ∈ ℝ → exp ↾ S : S ⟶ 1-1 onto ℂ ∖ 0
22 3 21 ax-mp ⊢ exp ↾ S : S ⟶ 1-1 onto ℂ ∖ 0