Theorem efif1o

Description: The exponential function of an imaginary number maps any open-below, closed-above interval of length 2 _pi one-to-one onto the unit circle. (Contributed by Paul Chapman, 16-Mar-2008) (Revised by Mario Carneiro, 13-May-2014)

	Ref	Expression
Hypotheses	efif1o.1	⊢ 𝐹 = ( 𝑤 ∈ 𝐷 ↦ ( exp ‘ ( i · 𝑤 ) ) )
	efif1o.2	⊢ 𝐶 = ( ◡ abs “ { 1 } )
	efif1o.3	⊢ 𝐷 = ( 𝐴 (,] ( 𝐴 + ( 2 · π ) ) )
Assertion	efif1o	⊢ ( 𝐴 ∈ ℝ → 𝐹 : 𝐷 –1-1-onto→ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		efif1o.1	⊢ 𝐹 = ( 𝑤 ∈ 𝐷 ↦ ( exp ‘ ( i · 𝑤 ) ) )
2		efif1o.2	⊢ 𝐶 = ( ◡ abs “ { 1 } )
3		efif1o.3	⊢ 𝐷 = ( 𝐴 (,] ( 𝐴 + ( 2 · π ) ) )
4		rexr	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
5		2re	⊢ 2 ∈ ℝ
6		pire	⊢ π ∈ ℝ
7	5 6	remulcli	⊢ ( 2 · π ) ∈ ℝ
8		readdcl	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 2 · π ) ∈ ℝ ) → ( 𝐴 + ( 2 · π ) ) ∈ ℝ )
9	7 8	mpan2	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + ( 2 · π ) ) ∈ ℝ )
10		elioc2	⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐴 + ( 2 · π ) ) ∈ ℝ ) → ( 𝑥 ∈ ( 𝐴 (,] ( 𝐴 + ( 2 · π ) ) ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ ( 𝐴 + ( 2 · π ) ) ) ) )
11	4 9 10	syl2anc	⊢ ( 𝐴 ∈ ℝ → ( 𝑥 ∈ ( 𝐴 (,] ( 𝐴 + ( 2 · π ) ) ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ ( 𝐴 + ( 2 · π ) ) ) ) )
12		simp1	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ ( 𝐴 + ( 2 · π ) ) ) → 𝑥 ∈ ℝ )
13	11 12	syl6bi	⊢ ( 𝐴 ∈ ℝ → ( 𝑥 ∈ ( 𝐴 (,] ( 𝐴 + ( 2 · π ) ) ) → 𝑥 ∈ ℝ ) )
14	13	ssrdv	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 (,] ( 𝐴 + ( 2 · π ) ) ) ⊆ ℝ )
15	3 14	eqsstrid	⊢ ( 𝐴 ∈ ℝ → 𝐷 ⊆ ℝ )
16	3	efif1olem1	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( abs ‘ ( 𝑥 − 𝑦 ) ) < ( 2 · π ) )
17	3	efif1olem2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐷 ( ( 𝑧 − 𝑦 ) / ( 2 · π ) ) ∈ ℤ )
18		eqid	⊢ ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) = ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) )
19	1 2 15 16 17 18	efif1olem4	⊢ ( 𝐴 ∈ ℝ → 𝐹 : 𝐷 –1-1-onto→ 𝐶 )