This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrdi ⊢ ( 𝐴 ∈ ℝ → ( 𝑥 ∈ ( 𝐴 (,] ( 𝐴 + ( 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→ 𝐶 )