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	addid2i	⊢ ( 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→ 𝐶