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

Metamath Proof Explorer

Theorem efifo

Description: The exponential function of an imaginary number maps the reals onto the unit circle. (Contributed by Mario Carneiro, 13-May-2014)

Ref Expression
Hypotheses efifo.1 ⊢ 𝐹 = ( 𝑧 ∈ ℝ ↦ ( exp ‘ ( i · 𝑧 ) ) )
efifo.2 ⊢ 𝐶 = ( ◡ abs “ { 1 } )
Assertion efifo 𝐹 : ℝ –onto→ 𝐶

Proof

Step Hyp Ref Expression
1 efifo.1 ⊢ 𝐹 = ( 𝑧 ∈ ℝ ↦ ( exp ‘ ( i · 𝑧 ) ) )
2 efifo.2 ⊢ 𝐶 = ( ◡ abs “ { 1 } )
3 ax-icn ⊢ i ∈ ℂ
4 recn ⊢ ( 𝑧 ∈ ℝ → 𝑧 ∈ ℂ )
5 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( i · 𝑧 ) ∈ ℂ )
6 3 4 5 sylancr ⊢ ( 𝑧 ∈ ℝ → ( i · 𝑧 ) ∈ ℂ )
7 efcl ⊢ ( ( i · 𝑧 ) ∈ ℂ → ( exp ‘ ( i · 𝑧 ) ) ∈ ℂ )
8 6 7 syl ⊢ ( 𝑧 ∈ ℝ → ( exp ‘ ( i · 𝑧 ) ) ∈ ℂ )
9 absefi ⊢ ( 𝑧 ∈ ℝ → ( abs ‘ ( exp ‘ ( i · 𝑧 ) ) ) = 1 )
10 absf ⊢ abs : ℂ ⟶ ℝ
11 ffn ⊢ ( abs : ℂ ⟶ ℝ → abs Fn ℂ )
12 fniniseg ⊢ ( abs Fn ℂ → ( ( exp ‘ ( i · 𝑧 ) ) ∈ ( ◡ abs “ { 1 } ) ↔ ( ( exp ‘ ( i · 𝑧 ) ) ∈ ℂ ∧ ( abs ‘ ( exp ‘ ( i · 𝑧 ) ) ) = 1 ) ) )
13 10 11 12 mp2b ⊢ ( ( exp ‘ ( i · 𝑧 ) ) ∈ ( ◡ abs “ { 1 } ) ↔ ( ( exp ‘ ( i · 𝑧 ) ) ∈ ℂ ∧ ( abs ‘ ( exp ‘ ( i · 𝑧 ) ) ) = 1 ) )
14 8 9 13 sylanbrc ⊢ ( 𝑧 ∈ ℝ → ( exp ‘ ( i · 𝑧 ) ) ∈ ( ◡ abs “ { 1 } ) )
15 14 2 eleqtrrdi ⊢ ( 𝑧 ∈ ℝ → ( exp ‘ ( i · 𝑧 ) ) ∈ 𝐶 )
16 1 15 fmpti ⊢ 𝐹 : ℝ ⟶ 𝐶
17 ffn ⊢ ( 𝐹 : ℝ ⟶ 𝐶 → 𝐹 Fn ℝ )
18 16 17 ax-mp ⊢ 𝐹 Fn ℝ
19 frn ⊢ ( 𝐹 : ℝ ⟶ 𝐶 → ran 𝐹 ⊆ 𝐶 )
20 16 19 ax-mp ⊢ ran 𝐹 ⊆ 𝐶
21 df-ima ⊢ ( 𝐹 “ ( 0 (,] ( 2 · π ) ) ) = ran ( 𝐹 ↾ ( 0 (,] ( 2 · π ) ) )
22 1 reseq1i ⊢ ( 𝐹 ↾ ( 0 (,] ( 2 · π ) ) ) = ( ( 𝑧 ∈ ℝ ↦ ( exp ‘ ( i · 𝑧 ) ) ) ↾ ( 0 (,] ( 2 · π ) ) )
23 0xr ⊢ 0 ∈ ℝ*
24 2re ⊢ 2 ∈ ℝ
25 pire ⊢ π ∈ ℝ
26 24 25 remulcli ⊢ ( 2 · π ) ∈ ℝ
27 elioc2 ⊢ ( ( 0 ∈ ℝ* ∧ ( 2 · π ) ∈ ℝ ) → ( 𝑧 ∈ ( 0 (,] ( 2 · π ) ) ↔ ( 𝑧 ∈ ℝ ∧ 0 < 𝑧 ∧ 𝑧 ≤ ( 2 · π ) ) ) )
28 23 26 27 mp2an ⊢ ( 𝑧 ∈ ( 0 (,] ( 2 · π ) ) ↔ ( 𝑧 ∈ ℝ ∧ 0 < 𝑧 ∧ 𝑧 ≤ ( 2 · π ) ) )
29 28 simp1bi ⊢ ( 𝑧 ∈ ( 0 (,] ( 2 · π ) ) → 𝑧 ∈ ℝ )
30 29 ssriv ⊢ ( 0 (,] ( 2 · π ) ) ⊆ ℝ
31 resmpt ⊢ ( ( 0 (,] ( 2 · π ) ) ⊆ ℝ → ( ( 𝑧 ∈ ℝ ↦ ( exp ‘ ( i · 𝑧 ) ) ) ↾ ( 0 (,] ( 2 · π ) ) ) = ( 𝑧 ∈ ( 0 (,] ( 2 · π ) ) ↦ ( exp ‘ ( i · 𝑧 ) ) ) )
32 30 31 ax-mp ⊢ ( ( 𝑧 ∈ ℝ ↦ ( exp ‘ ( i · 𝑧 ) ) ) ↾ ( 0 (,] ( 2 · π ) ) ) = ( 𝑧 ∈ ( 0 (,] ( 2 · π ) ) ↦ ( exp ‘ ( i · 𝑧 ) ) )
33 22 32 eqtri ⊢ ( 𝐹 ↾ ( 0 (,] ( 2 · π ) ) ) = ( 𝑧 ∈ ( 0 (,] ( 2 · π ) ) ↦ ( exp ‘ ( i · 𝑧 ) ) )
34 33 rneqi ⊢ ran ( 𝐹 ↾ ( 0 (,] ( 2 · π ) ) ) = ran ( 𝑧 ∈ ( 0 (,] ( 2 · π ) ) ↦ ( exp ‘ ( i · 𝑧 ) ) )
35 0re ⊢ 0 ∈ ℝ
36 eqid ⊢ ( 𝑧 ∈ ( 0 (,] ( 2 · π ) ) ↦ ( exp ‘ ( i · 𝑧 ) ) ) = ( 𝑧 ∈ ( 0 (,] ( 2 · π ) ) ↦ ( exp ‘ ( i · 𝑧 ) ) )
37 26 recni ⊢ ( 2 · π ) ∈ ℂ
38 37 addlidi ⊢ ( 0 + ( 2 · π ) ) = ( 2 · π )
39 38 oveq2i ⊢ ( 0 (,] ( 0 + ( 2 · π ) ) ) = ( 0 (,] ( 2 · π ) )
40 39 eqcomi ⊢ ( 0 (,] ( 2 · π ) ) = ( 0 (,] ( 0 + ( 2 · π ) ) )
41 36 2 40 efif1o ⊢ ( 0 ∈ ℝ → ( 𝑧 ∈ ( 0 (,] ( 2 · π ) ) ↦ ( exp ‘ ( i · 𝑧 ) ) ) : ( 0 (,] ( 2 · π ) ) –1-1-onto→ 𝐶 )
42 35 41 ax-mp ⊢ ( 𝑧 ∈ ( 0 (,] ( 2 · π ) ) ↦ ( exp ‘ ( i · 𝑧 ) ) ) : ( 0 (,] ( 2 · π ) ) –1-1-onto→ 𝐶
43 f1ofo ⊢ ( ( 𝑧 ∈ ( 0 (,] ( 2 · π ) ) ↦ ( exp ‘ ( i · 𝑧 ) ) ) : ( 0 (,] ( 2 · π ) ) –1-1-onto→ 𝐶 → ( 𝑧 ∈ ( 0 (,] ( 2 · π ) ) ↦ ( exp ‘ ( i · 𝑧 ) ) ) : ( 0 (,] ( 2 · π ) ) –onto→ 𝐶 )
44 forn ⊢ ( ( 𝑧 ∈ ( 0 (,] ( 2 · π ) ) ↦ ( exp ‘ ( i · 𝑧 ) ) ) : ( 0 (,] ( 2 · π ) ) –onto→ 𝐶 → ran ( 𝑧 ∈ ( 0 (,] ( 2 · π ) ) ↦ ( exp ‘ ( i · 𝑧 ) ) ) = 𝐶 )
45 42 43 44 mp2b ⊢ ran ( 𝑧 ∈ ( 0 (,] ( 2 · π ) ) ↦ ( exp ‘ ( i · 𝑧 ) ) ) = 𝐶
46 34 45 eqtri ⊢ ran ( 𝐹 ↾ ( 0 (,] ( 2 · π ) ) ) = 𝐶
47 21 46 eqtri ⊢ ( 𝐹 “ ( 0 (,] ( 2 · π ) ) ) = 𝐶
48 imassrn ⊢ ( 𝐹 “ ( 0 (,] ( 2 · π ) ) ) ⊆ ran 𝐹
49 47 48 eqsstrri ⊢ 𝐶 ⊆ ran 𝐹
50 20 49 eqssi ⊢ ran 𝐹 = 𝐶
51 df-fo ⊢ ( 𝐹 : ℝ –onto→ 𝐶 ↔ ( 𝐹 Fn ℝ ∧ ran 𝐹 = 𝐶 ) )
52 18 50 51 mpbir2an ⊢ 𝐹 : ℝ –onto→ 𝐶