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	$⊢ F = (z \in ℝ ⟼ e^{i z})$
	efifo.2	$⊢ C = {abs}^{-1} [\{1\}]$
Assertion	efifo	$⊢ F : ℝ \underset{onto}{⟶} C$

Proof

Step	Hyp	Ref	Expression
1		efifo.1	$⊢ F = (z \in ℝ ⟼ e^{i z})$
2		efifo.2	$⊢ C = {abs}^{-1} [\{1\}]$
3		ax-icn	$⊢ i \in ℂ$
4		recn	$⊢ z \in ℝ \to z \in ℂ$
5		mulcl	$⊢ (i \in ℂ \land z \in ℂ) \to i z \in ℂ$
6	3 4 5	sylancr	$⊢ z \in ℝ \to i z \in ℂ$
7		efcl	$⊢ i z \in ℂ \to e^{i z} \in ℂ$
8	6 7	syl	$⊢ z \in ℝ \to e^{i z} \in ℂ$
9		absefi	$⊢ z \in ℝ \to \|e^{i z}\| = 1$
10		absf	$⊢ abs : ℂ ⟶ ℝ$
11		ffn	$⊢ abs : ℂ ⟶ ℝ \to abs Fn ℂ$
12		fniniseg	$⊢ abs Fn ℂ \to (e^{i z} \in {abs}^{-1} [\{1\}] \leftrightarrow (e^{i z} \in ℂ \land \|e^{i z}\| = 1))$
13	10 11 12	mp2b	$⊢ e^{i z} \in {abs}^{-1} [\{1\}] \leftrightarrow (e^{i z} \in ℂ \land \|e^{i z}\| = 1)$
14	8 9 13	sylanbrc	$⊢ z \in ℝ \to e^{i z} \in {abs}^{-1} [\{1\}]$
15	14 2	eleqtrrdi	$⊢ z \in ℝ \to e^{i z} \in C$
16	1 15	fmpti	$⊢ F : ℝ ⟶ C$
17		ffn	$⊢ F : ℝ ⟶ C \to F Fn ℝ$
18	16 17	ax-mp	$⊢ F Fn ℝ$
19		frn	$⊢ F : ℝ ⟶ C \to ran F \subseteq C$
20	16 19	ax-mp	$⊢ ran F \subseteq C$
21		df-ima	$⊢ F [(0, 2 π]] = ran ({F ↾}_{(0, 2 π]})$
22	1	reseq1i	$⊢ {F ↾}_{(0, 2 π]} = {(z \in ℝ ⟼ e^{i z}) ↾}_{(0, 2 π]}$
23		0xr	$⊢ 0 \in ℝ^{*}$
24		2re	$⊢ 2 \in ℝ$
25		pire	$⊢ π \in ℝ$
26	24 25	remulcli	$⊢ 2 π \in ℝ$
27		elioc2	$⊢ (0 \in ℝ^{*} \land 2 π \in ℝ) \to (z \in (0, 2 π] \leftrightarrow (z \in ℝ \land 0 < z \land z \leq 2 π))$
28	23 26 27	mp2an	$⊢ z \in (0, 2 π] \leftrightarrow (z \in ℝ \land 0 < z \land z \leq 2 π)$
29	28	simp1bi	$⊢ z \in (0, 2 π] \to z \in ℝ$
30	29	ssriv	$⊢ (0, 2 π] \subseteq ℝ$
31		resmpt	$⊢ (0, 2 π] \subseteq ℝ \to {(z \in ℝ ⟼ e^{i z}) ↾}_{(0, 2 π]} = (z \in (0, 2 π] ⟼ e^{i z})$
32	30 31	ax-mp	$⊢ {(z \in ℝ ⟼ e^{i z}) ↾}_{(0, 2 π]} = (z \in (0, 2 π] ⟼ e^{i z})$
33	22 32	eqtri	$⊢ {F ↾}_{(0, 2 π]} = (z \in (0, 2 π] ⟼ e^{i z})$
34	33	rneqi	$⊢ ran ({F ↾}_{(0, 2 π]}) = ran (z \in (0, 2 π] ⟼ e^{i z})$
35		0re	$⊢ 0 \in ℝ$
36		eqid	$⊢ (z \in (0, 2 π] ⟼ e^{i z}) = (z \in (0, 2 π] ⟼ e^{i z})$
37	26	recni	$⊢ 2 π \in ℂ$
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 \in ℝ \to (z \in (0, 2 π] ⟼ e^{i z}) : (0, 2 π] \underset{1-1 onto}{⟶} C$
42	35 41	ax-mp	$⊢ (z \in (0, 2 π] ⟼ e^{i z}) : (0, 2 π] \underset{1-1 onto}{⟶} C$
43		f1ofo	$⊢ (z \in (0, 2 π] ⟼ e^{i z}) : (0, 2 π] \underset{1-1 onto}{⟶} C \to (z \in (0, 2 π] ⟼ e^{i z}) : (0, 2 π] \underset{onto}{⟶} C$
44		forn	$⊢ (z \in (0, 2 π] ⟼ e^{i z}) : (0, 2 π] \underset{onto}{⟶} C \to ran (z \in (0, 2 π] ⟼ e^{i z}) = C$
45	42 43 44	mp2b	$⊢ ran (z \in (0, 2 π] ⟼ e^{i z}) = C$
46	34 45	eqtri	$⊢ ran ({F ↾}_{(0, 2 π]}) = C$
47	21 46	eqtri	$⊢ F [(0, 2 π]] = C$
48		imassrn	$⊢ F [(0, 2 π]] \subseteq ran F$
49	47 48	eqsstrri	$⊢ C \subseteq ran F$
50	20 49	eqssi	$⊢ ran F = C$
51		df-fo	$⊢ F : ℝ \underset{onto}{⟶} C \leftrightarrow (F Fn ℝ \land ran F = C)$
52	18 50 51	mpbir2an	$⊢ F : ℝ \underset{onto}{⟶} C$

Metamath Proof Explorer

Theorem efifo

Proof