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	⊢ 𝑆 = ( ◡ ℑ “ ( - π (,] π ) )
Assertion	eff1o	⊢ ( exp ↾ 𝑆 ) : 𝑆 –1-1-onto→ ( ℂ ∖ { 0 } )

Proof

Step	Hyp	Ref	Expression
1		eff1o.1	⊢ 𝑆 = ( ◡ ℑ “ ( - π (,] π ) )
2		pire	⊢ π ∈ ℝ
3	2	renegcli	⊢ - π ∈ ℝ
4		eqid	⊢ ( 𝑤 ∈ ( - π (,] π ) ↦ ( exp ‘ ( i · 𝑤 ) ) ) = ( 𝑤 ∈ ( - π (,] π ) ↦ ( exp ‘ ( i · 𝑤 ) ) )
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	⊢ ( ( - π ∈ ℝ ∧ ( 𝑥 ∈ ( - π (,] π ) ∧ 𝑦 ∈ ( - π (,] π ) ) ) → ( abs ‘ ( 𝑥 − 𝑦 ) ) < ( 2 · π ) )
20	18	efif1olem2	⊢ ( ( - π ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ∃ 𝑦 ∈ ( - π (,] π ) ( ( 𝑧 − 𝑦 ) / ( 2 · π ) ) ∈ ℤ )
21	4 1 7 19 20	eff1olem	⊢ ( - π ∈ ℝ → ( exp ↾ 𝑆 ) : 𝑆 –1-1-onto→ ( ℂ ∖ { 0 } ) )
22	3 21	ax-mp	⊢ ( exp ↾ 𝑆 ) : 𝑆 –1-1-onto→ ( ℂ ∖ { 0 } )