efif1olem4

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

	Ref	Expression
Hypotheses	efif1o.1	$⊢ F = (w \in D ⟼ e^{i w})$
	efif1o.2	$⊢ C = {abs}^{-1} [\{1\}]$
	efif1olem4.3	$⊢ φ \to D \subseteq ℝ$
	efif1olem4.4	$⊢ (φ \land (x \in D \land y \in D)) \to \|x - y\| < 2 π$
	efif1olem4.5	$⊢ (φ \land z \in ℝ) \to \exists y \in D \frac{z - y}{2 π} \in ℤ$
	efif1olem4.6	$⊢ S = {\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]}$
Assertion	efif1olem4	$⊢ φ \to F : D \underset{1-1 onto}{⟶} C$

Proof

Step	Hyp	Ref	Expression
1		efif1o.1	$⊢ F = (w \in D ⟼ e^{i w})$
2		efif1o.2	$⊢ C = {abs}^{-1} [\{1\}]$
3		efif1olem4.3	$⊢ φ \to D \subseteq ℝ$
4		efif1olem4.4	$⊢ (φ \land (x \in D \land y \in D)) \to \|x - y\| < 2 π$
5		efif1olem4.5	$⊢ (φ \land z \in ℝ) \to \exists y \in D \frac{z - y}{2 π} \in ℤ$
6		efif1olem4.6	$⊢ S = {\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]}$
7	3	sselda	$⊢ (φ \land w \in D) \to w \in ℝ$
8		ax-icn	$⊢ i \in ℂ$
9		recn	$⊢ w \in ℝ \to w \in ℂ$
10		mulcl	$⊢ (i \in ℂ \land w \in ℂ) \to i w \in ℂ$
11	8 9 10	sylancr	$⊢ w \in ℝ \to i w \in ℂ$
12	11	efcld	$⊢ w \in ℝ \to e^{i w} \in ℂ$
13		absefi	$⊢ w \in ℝ \to \|e^{i w}\| = 1$
14		absf	$⊢ abs : ℂ ⟶ ℝ$
15		ffn	$⊢ abs : ℂ ⟶ ℝ \to abs Fn ℂ$
16	14 15	ax-mp	$⊢ abs Fn ℂ$
17		fniniseg	$⊢ abs Fn ℂ \to (e^{i w} \in {abs}^{-1} [\{1\}] \leftrightarrow (e^{i w} \in ℂ \land \|e^{i w}\| = 1))$
18	16 17	ax-mp	$⊢ e^{i w} \in {abs}^{-1} [\{1\}] \leftrightarrow (e^{i w} \in ℂ \land \|e^{i w}\| = 1)$
19	12 13 18	sylanbrc	$⊢ w \in ℝ \to e^{i w} \in {abs}^{-1} [\{1\}]$
20	19 2	eleqtrrdi	$⊢ w \in ℝ \to e^{i w} \in C$
21	7 20	syl	$⊢ (φ \land w \in D) \to e^{i w} \in C$
22	21 1	fmptd	$⊢ φ \to F : D ⟶ C$
23	3	ad2antrr	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to D \subseteq ℝ$
24		simplrl	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to x \in D$
25	23 24	sseldd	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to x \in ℝ$
26	25	recnd	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to x \in ℂ$
27		simplrr	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to y \in D$
28	23 27	sseldd	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to y \in ℝ$
29	28	recnd	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to y \in ℂ$
30	26 29	subcld	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to x - y \in ℂ$
31		2picn	$⊢ 2 π \in ℂ$
32		2pire	$⊢ 2 π \in ℝ$
33		2re	$⊢ 2 \in ℝ$
34		pire	$⊢ π \in ℝ$
35		2pos	$⊢ 0 < 2$
36		pipos	$⊢ 0 < π$
37	33 34 35 36	mulgt0ii	$⊢ 0 < 2 π$
38	32 37	gt0ne0ii	$⊢ 2 π \neq 0$
39		divcl	$⊢ (x - y \in ℂ \land 2 π \in ℂ \land 2 π \neq 0) \to \frac{x - y}{2 π} \in ℂ$
40	31 38 39	mp3an23	$⊢ x - y \in ℂ \to \frac{x - y}{2 π} \in ℂ$
41	30 40	syl	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to \frac{x - y}{2 π} \in ℂ$
42		absdiv	$⊢ (x - y \in ℂ \land 2 π \in ℂ \land 2 π \neq 0) \to \|\frac{x - y}{2 π}\| = \frac{\|x - y\|}{\|2 π\|}$
43	31 38 42	mp3an23	$⊢ x - y \in ℂ \to \|\frac{x - y}{2 π}\| = \frac{\|x - y\|}{\|2 π\|}$
44	30 43	syl	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to \|\frac{x - y}{2 π}\| = \frac{\|x - y\|}{\|2 π\|}$
45		0re	$⊢ 0 \in ℝ$
46	45 32 37	ltleii	$⊢ 0 \leq 2 π$
47		absid	$⊢ (2 π \in ℝ \land 0 \leq 2 π) \to \|2 π\| = 2 π$
48	32 46 47	mp2an	$⊢ \|2 π\| = 2 π$
49	48	oveq2i	$⊢ \frac{\|x - y\|}{\|2 π\|} = \frac{\|x - y\|}{2 π}$
50	44 49	eqtrdi	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to \|\frac{x - y}{2 π}\| = \frac{\|x - y\|}{2 π}$
51	4	adantr	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to \|x - y\| < 2 π$
52	31	mulridi	$⊢ 2 π \cdot 1 = 2 π$
53	51 52	breqtrrdi	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to \|x - y\| < 2 π \cdot 1$
54	30	abscld	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to \|x - y\| \in ℝ$
55		1re	$⊢ 1 \in ℝ$
56	32 37	pm3.2i	$⊢ (2 π \in ℝ \land 0 < 2 π)$
57		ltdivmul	$⊢ (\|x - y\| \in ℝ \land 1 \in ℝ \land (2 π \in ℝ \land 0 < 2 π)) \to (\frac{\|x - y\|}{2 π} < 1 \leftrightarrow \|x - y\| < 2 π \cdot 1)$
58	55 56 57	mp3an23	$⊢ \|x - y\| \in ℝ \to (\frac{\|x - y\|}{2 π} < 1 \leftrightarrow \|x - y\| < 2 π \cdot 1)$
59	54 58	syl	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to (\frac{\|x - y\|}{2 π} < 1 \leftrightarrow \|x - y\| < 2 π \cdot 1)$
60	53 59	mpbird	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to \frac{\|x - y\|}{2 π} < 1$
61	50 60	eqbrtrd	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to \|\frac{x - y}{2 π}\| < 1$
62	31 38	pm3.2i	$⊢ (2 π \in ℂ \land 2 π \neq 0)$
63		ine0	$⊢ i \neq 0$
64	8 63	pm3.2i	$⊢ (i \in ℂ \land i \neq 0)$
65		divcan5	$⊢ (x - y \in ℂ \land (2 π \in ℂ \land 2 π \neq 0) \land (i \in ℂ \land i \neq 0)) \to \frac{i (x - y)}{i 2 π} = \frac{x - y}{2 π}$
66	62 64 65	mp3an23	$⊢ x - y \in ℂ \to \frac{i (x - y)}{i 2 π} = \frac{x - y}{2 π}$
67	30 66	syl	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to \frac{i (x - y)}{i 2 π} = \frac{x - y}{2 π}$
68	8	a1i	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to i \in ℂ$
69	68 26 29	subdid	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to i (x - y) = i x - i y$
70	69	fveq2d	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to e^{i (x - y)} = e^{i x - i y}$
71		mulcl	$⊢ (i \in ℂ \land x \in ℂ) \to i x \in ℂ$
72	8 26 71	sylancr	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to i x \in ℂ$
73		mulcl	$⊢ (i \in ℂ \land y \in ℂ) \to i y \in ℂ$
74	8 29 73	sylancr	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to i y \in ℂ$
75		efsub	$⊢ (i x \in ℂ \land i y \in ℂ) \to e^{i x - i y} = \frac{e^{i x}}{e^{i y}}$
76	72 74 75	syl2anc	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to e^{i x - i y} = \frac{e^{i x}}{e^{i y}}$
77	74	efcld	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to e^{i y} \in ℂ$
78	74	efne0d	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to e^{i y} \neq 0$
79		simpr	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to F (x) = F (y)$
80		oveq2	$⊢ w = x \to i w = i x$
81	80	fveq2d	$⊢ w = x \to e^{i w} = e^{i x}$
82		fvex	$⊢ e^{i x} \in V$
83	81 1 82	fvmpt	$⊢ x \in D \to F (x) = e^{i x}$
84	24 83	syl	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to F (x) = e^{i x}$
85		oveq2	$⊢ w = y \to i w = i y$
86	85	fveq2d	$⊢ w = y \to e^{i w} = e^{i y}$
87		fvex	$⊢ e^{i y} \in V$
88	86 1 87	fvmpt	$⊢ y \in D \to F (y) = e^{i y}$
89	27 88	syl	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to F (y) = e^{i y}$
90	79 84 89	3eqtr3d	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to e^{i x} = e^{i y}$
91	77 78 90	diveq1bd	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to \frac{e^{i x}}{e^{i y}} = 1$
92	70 76 91	3eqtrd	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to e^{i (x - y)} = 1$
93		mulcl	$⊢ (i \in ℂ \land x - y \in ℂ) \to i (x - y) \in ℂ$
94	8 30 93	sylancr	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to i (x - y) \in ℂ$
95		efeq1	$⊢ i (x - y) \in ℂ \to (e^{i (x - y)} = 1 \leftrightarrow \frac{i (x - y)}{i 2 π} \in ℤ)$
96	94 95	syl	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to (e^{i (x - y)} = 1 \leftrightarrow \frac{i (x - y)}{i 2 π} \in ℤ)$
97	92 96	mpbid	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to \frac{i (x - y)}{i 2 π} \in ℤ$
98	67 97	eqeltrrd	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to \frac{x - y}{2 π} \in ℤ$
99		nn0abscl	$⊢ \frac{x - y}{2 π} \in ℤ \to \|\frac{x - y}{2 π}\| \in ℕ_{0}$
100	98 99	syl	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to \|\frac{x - y}{2 π}\| \in ℕ_{0}$
101		nn0lt10b	$⊢ \|\frac{x - y}{2 π}\| \in ℕ_{0} \to (\|\frac{x - y}{2 π}\| < 1 \leftrightarrow \|\frac{x - y}{2 π}\| = 0)$
102	100 101	syl	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to (\|\frac{x - y}{2 π}\| < 1 \leftrightarrow \|\frac{x - y}{2 π}\| = 0)$
103	61 102	mpbid	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to \|\frac{x - y}{2 π}\| = 0$
104	41 103	abs00d	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to \frac{x - y}{2 π} = 0$
105		diveq0	$⊢ (x - y \in ℂ \land 2 π \in ℂ \land 2 π \neq 0) \to (\frac{x - y}{2 π} = 0 \leftrightarrow x - y = 0)$
106	31 38 105	mp3an23	$⊢ x - y \in ℂ \to (\frac{x - y}{2 π} = 0 \leftrightarrow x - y = 0)$
107	30 106	syl	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to (\frac{x - y}{2 π} = 0 \leftrightarrow x - y = 0)$
108	104 107	mpbid	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to x - y = 0$
109	26 29 108	subeq0d	$⊢ ((φ \land (x \in D \land y \in D)) \land F (x) = F (y)) \to x = y$
110	109	ex	$⊢ (φ \land (x \in D \land y \in D)) \to (F (x) = F (y) \to x = y)$
111	110	ralrimivva	$⊢ φ \to \forall x \in D \forall y \in D (F (x) = F (y) \to x = y)$
112		dff13	$⊢ F : D \underset{1-1}{⟶} C \leftrightarrow (F : D ⟶ C \land \forall x \in D \forall y \in D (F (x) = F (y) \to x = y))$
113	22 111 112	sylanbrc	$⊢ φ \to F : D \underset{1-1}{⟶} C$
114		oveq1	$⊢ z = 2 S^{-1} (ℑ (\sqrt{x})) \to z - y = 2 S^{-1} (ℑ (\sqrt{x})) - y$
115	114	oveq1d	$⊢ z = 2 S^{-1} (ℑ (\sqrt{x})) \to \frac{z - y}{2 π} = \frac{2 S^{-1} (ℑ (\sqrt{x})) - y}{2 π}$
116	115	eleq1d	$⊢ z = 2 S^{-1} (ℑ (\sqrt{x})) \to (\frac{z - y}{2 π} \in ℤ \leftrightarrow \frac{2 S^{-1} (ℑ (\sqrt{x})) - y}{2 π} \in ℤ)$
117	116	rexbidv	$⊢ z = 2 S^{-1} (ℑ (\sqrt{x})) \to (\exists y \in D \frac{z - y}{2 π} \in ℤ \leftrightarrow \exists y \in D \frac{2 S^{-1} (ℑ (\sqrt{x})) - y}{2 π} \in ℤ)$
118	5	ralrimiva	$⊢ φ \to \forall z \in ℝ \exists y \in D \frac{z - y}{2 π} \in ℤ$
119	118	adantr	$⊢ (φ \land x \in C) \to \forall z \in ℝ \exists y \in D \frac{z - y}{2 π} \in ℤ$
120		neghalfpire	$⊢ - \frac{π}{2} \in ℝ$
121		halfpire	$⊢ \frac{π}{2} \in ℝ$
122		iccssre	$⊢ (- \frac{π}{2} \in ℝ \land \frac{π}{2} \in ℝ) \to [- \frac{π}{2}, \frac{π}{2}] \subseteq ℝ$
123	120 121 122	mp2an	$⊢ [- \frac{π}{2}, \frac{π}{2}] \subseteq ℝ$
124	1 2	efif1olem3	$⊢ (φ \land x \in C) \to ℑ (\sqrt{x}) \in [- 1, 1]$
125		resinf1o	$⊢ ({\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]}) : [- \frac{π}{2}, \frac{π}{2}] \underset{1-1 onto}{⟶} [- 1, 1]$
126		f1oeq1	$⊢ S = {\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]} \to (S : [- \frac{π}{2}, \frac{π}{2}] \underset{1-1 onto}{⟶} [- 1, 1] \leftrightarrow ({\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]}) : [- \frac{π}{2}, \frac{π}{2}] \underset{1-1 onto}{⟶} [- 1, 1])$
127	6 126	ax-mp	$⊢ S : [- \frac{π}{2}, \frac{π}{2}] \underset{1-1 onto}{⟶} [- 1, 1] \leftrightarrow ({\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]}) : [- \frac{π}{2}, \frac{π}{2}] \underset{1-1 onto}{⟶} [- 1, 1]$
128	125 127	mpbir	$⊢ S : [- \frac{π}{2}, \frac{π}{2}] \underset{1-1 onto}{⟶} [- 1, 1]$
129		f1ocnv	$⊢ S : [- \frac{π}{2}, \frac{π}{2}] \underset{1-1 onto}{⟶} [- 1, 1] \to S^{-1} : [- 1, 1] \underset{1-1 onto}{⟶} [- \frac{π}{2}, \frac{π}{2}]$
130		f1of	$⊢ S^{-1} : [- 1, 1] \underset{1-1 onto}{⟶} [- \frac{π}{2}, \frac{π}{2}] \to S^{-1} : [- 1, 1] ⟶ [- \frac{π}{2}, \frac{π}{2}]$
131	128 129 130	mp2b	$⊢ S^{-1} : [- 1, 1] ⟶ [- \frac{π}{2}, \frac{π}{2}]$
132	131	ffvelcdmi	$⊢ ℑ (\sqrt{x}) \in [- 1, 1] \to S^{-1} (ℑ (\sqrt{x})) \in [- \frac{π}{2}, \frac{π}{2}]$
133	124 132	syl	$⊢ (φ \land x \in C) \to S^{-1} (ℑ (\sqrt{x})) \in [- \frac{π}{2}, \frac{π}{2}]$
134	123 133	sselid	$⊢ (φ \land x \in C) \to S^{-1} (ℑ (\sqrt{x})) \in ℝ$
135		remulcl	$⊢ (2 \in ℝ \land S^{-1} (ℑ (\sqrt{x})) \in ℝ) \to 2 S^{-1} (ℑ (\sqrt{x})) \in ℝ$
136	33 134 135	sylancr	$⊢ (φ \land x \in C) \to 2 S^{-1} (ℑ (\sqrt{x})) \in ℝ$
137	117 119 136	rspcdva	$⊢ (φ \land x \in C) \to \exists y \in D \frac{2 S^{-1} (ℑ (\sqrt{x})) - y}{2 π} \in ℤ$
138		oveq1	$⊢ e^{i (2 S^{-1} (ℑ (\sqrt{x})) - y)} = 1 \to e^{i (2 S^{-1} (ℑ (\sqrt{x})) - y)} e^{i y} = 1 e^{i y}$
139	136	adantr	$⊢ ((φ \land x \in C) \land y \in D) \to 2 S^{-1} (ℑ (\sqrt{x})) \in ℝ$
140	139	recnd	$⊢ ((φ \land x \in C) \land y \in D) \to 2 S^{-1} (ℑ (\sqrt{x})) \in ℂ$
141		mulcl	$⊢ (i \in ℂ \land 2 S^{-1} (ℑ (\sqrt{x})) \in ℂ) \to i 2 S^{-1} (ℑ (\sqrt{x})) \in ℂ$
142	8 140 141	sylancr	$⊢ ((φ \land x \in C) \land y \in D) \to i 2 S^{-1} (ℑ (\sqrt{x})) \in ℂ$
143	3	ad2antrr	$⊢ ((φ \land x \in C) \land y \in D) \to D \subseteq ℝ$
144		simpr	$⊢ ((φ \land x \in C) \land y \in D) \to y \in D$
145	143 144	sseldd	$⊢ ((φ \land x \in C) \land y \in D) \to y \in ℝ$
146	145	recnd	$⊢ ((φ \land x \in C) \land y \in D) \to y \in ℂ$
147	8 146 73	sylancr	$⊢ ((φ \land x \in C) \land y \in D) \to i y \in ℂ$
148	8	a1i	$⊢ ((φ \land x \in C) \land y \in D) \to i \in ℂ$
149	148 140 146	subdid	$⊢ ((φ \land x \in C) \land y \in D) \to i (2 S^{-1} (ℑ (\sqrt{x})) - y) = i 2 S^{-1} (ℑ (\sqrt{x})) - i y$
150	142 147 149	mvrrsubd	$⊢ ((φ \land x \in C) \land y \in D) \to i (2 S^{-1} (ℑ (\sqrt{x})) - y) + i y = i 2 S^{-1} (ℑ (\sqrt{x}))$
151	150	fveq2d	$⊢ ((φ \land x \in C) \land y \in D) \to e^{i (2 S^{-1} (ℑ (\sqrt{x})) - y) + i y} = e^{i 2 S^{-1} (ℑ (\sqrt{x}))}$
152	140 146	subcld	$⊢ ((φ \land x \in C) \land y \in D) \to 2 S^{-1} (ℑ (\sqrt{x})) - y \in ℂ$
153		mulcl	$⊢ (i \in ℂ \land 2 S^{-1} (ℑ (\sqrt{x})) - y \in ℂ) \to i (2 S^{-1} (ℑ (\sqrt{x})) - y) \in ℂ$
154	8 152 153	sylancr	$⊢ ((φ \land x \in C) \land y \in D) \to i (2 S^{-1} (ℑ (\sqrt{x})) - y) \in ℂ$
155		efadd	$⊢ (i (2 S^{-1} (ℑ (\sqrt{x})) - y) \in ℂ \land i y \in ℂ) \to e^{i (2 S^{-1} (ℑ (\sqrt{x})) - y) + i y} = e^{i (2 S^{-1} (ℑ (\sqrt{x})) - y)} e^{i y}$
156	154 147 155	syl2anc	$⊢ ((φ \land x \in C) \land y \in D) \to e^{i (2 S^{-1} (ℑ (\sqrt{x})) - y) + i y} = e^{i (2 S^{-1} (ℑ (\sqrt{x})) - y)} e^{i y}$
157		2cn	$⊢ 2 \in ℂ$
158	134	recnd	$⊢ (φ \land x \in C) \to S^{-1} (ℑ (\sqrt{x})) \in ℂ$
159		mul12	$⊢ (i \in ℂ \land 2 \in ℂ \land S^{-1} (ℑ (\sqrt{x})) \in ℂ) \to i 2 S^{-1} (ℑ (\sqrt{x})) = 2 i S^{-1} (ℑ (\sqrt{x}))$
160	8 157 158 159	mp3an12i	$⊢ (φ \land x \in C) \to i 2 S^{-1} (ℑ (\sqrt{x})) = 2 i S^{-1} (ℑ (\sqrt{x}))$
161	160	fveq2d	$⊢ (φ \land x \in C) \to e^{i 2 S^{-1} (ℑ (\sqrt{x}))} = e^{2 i S^{-1} (ℑ (\sqrt{x}))}$
162		mulcl	$⊢ (i \in ℂ \land S^{-1} (ℑ (\sqrt{x})) \in ℂ) \to i S^{-1} (ℑ (\sqrt{x})) \in ℂ$
163	8 158 162	sylancr	$⊢ (φ \land x \in C) \to i S^{-1} (ℑ (\sqrt{x})) \in ℂ$
164		2z	$⊢ 2 \in ℤ$
165		efexp	$⊢ (i S^{-1} (ℑ (\sqrt{x})) \in ℂ \land 2 \in ℤ) \to e^{2 i S^{-1} (ℑ (\sqrt{x}))} = {e^{i S^{-1} (ℑ (\sqrt{x}))}}^{2}$
166	163 164 165	sylancl	$⊢ (φ \land x \in C) \to e^{2 i S^{-1} (ℑ (\sqrt{x}))} = {e^{i S^{-1} (ℑ (\sqrt{x}))}}^{2}$
167	161 166	eqtrd	$⊢ (φ \land x \in C) \to e^{i 2 S^{-1} (ℑ (\sqrt{x}))} = {e^{i S^{-1} (ℑ (\sqrt{x}))}}^{2}$
168	134	recoscld	$⊢ (φ \land x \in C) \to \cos S^{-1} (ℑ (\sqrt{x})) \in ℝ$
169		simpr	$⊢ (φ \land x \in C) \to x \in C$
170	169 2	eleqtrdi	$⊢ (φ \land x \in C) \to x \in {abs}^{-1} [\{1\}]$
171		fniniseg	$⊢ abs Fn ℂ \to (x \in {abs}^{-1} [\{1\}] \leftrightarrow (x \in ℂ \land \|x\| = 1))$
172	16 171	ax-mp	$⊢ x \in {abs}^{-1} [\{1\}] \leftrightarrow (x \in ℂ \land \|x\| = 1)$
173	170 172	sylib	$⊢ (φ \land x \in C) \to (x \in ℂ \land \|x\| = 1)$
174	173	simpld	$⊢ (φ \land x \in C) \to x \in ℂ$
175	174	sqrtcld	$⊢ (φ \land x \in C) \to \sqrt{x} \in ℂ$
176	175	recld	$⊢ (φ \land x \in C) \to ℜ (\sqrt{x}) \in ℝ$
177		cosq14ge0	$⊢ S^{-1} (ℑ (\sqrt{x})) \in [- \frac{π}{2}, \frac{π}{2}] \to 0 \leq \cos S^{-1} (ℑ (\sqrt{x}))$
178	133 177	syl	$⊢ (φ \land x \in C) \to 0 \leq \cos S^{-1} (ℑ (\sqrt{x}))$
179	174	sqrtrege0d	$⊢ (φ \land x \in C) \to 0 \leq ℜ (\sqrt{x})$
180		sincossq	$⊢ S^{-1} (ℑ (\sqrt{x})) \in ℂ \to {\sin S^{-1} (ℑ (\sqrt{x}))}^{2} + {\cos S^{-1} (ℑ (\sqrt{x}))}^{2} = 1$
181	158 180	syl	$⊢ (φ \land x \in C) \to {\sin S^{-1} (ℑ (\sqrt{x}))}^{2} + {\cos S^{-1} (ℑ (\sqrt{x}))}^{2} = 1$
182	174	sqsqrtd	$⊢ (φ \land x \in C) \to {\sqrt{x}}^{2} = x$
183	182	fveq2d	$⊢ (φ \land x \in C) \to \|{\sqrt{x}}^{2}\| = \|x\|$
184		2nn0	$⊢ 2 \in ℕ_{0}$
185		absexp	$⊢ (\sqrt{x} \in ℂ \land 2 \in ℕ_{0}) \to \|{\sqrt{x}}^{2}\| = {\|\sqrt{x}\|}^{2}$
186	175 184 185	sylancl	$⊢ (φ \land x \in C) \to \|{\sqrt{x}}^{2}\| = {\|\sqrt{x}\|}^{2}$
187	173	simprd	$⊢ (φ \land x \in C) \to \|x\| = 1$
188	183 186 187	3eqtr3d	$⊢ (φ \land x \in C) \to {\|\sqrt{x}\|}^{2} = 1$
189	175	absvalsq2d	$⊢ (φ \land x \in C) \to {\|\sqrt{x}\|}^{2} = {ℜ (\sqrt{x})}^{2} + {ℑ (\sqrt{x})}^{2}$
190	181 188 189	3eqtr2d	$⊢ (φ \land x \in C) \to {\sin S^{-1} (ℑ (\sqrt{x}))}^{2} + {\cos S^{-1} (ℑ (\sqrt{x}))}^{2} = {ℜ (\sqrt{x})}^{2} + {ℑ (\sqrt{x})}^{2}$
191	6	fveq1i	$⊢ S (S^{-1} (ℑ (\sqrt{x}))) = ({\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]}) (S^{-1} (ℑ (\sqrt{x})))$
192	133	fvresd	$⊢ (φ \land x \in C) \to ({\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]}) (S^{-1} (ℑ (\sqrt{x}))) = \sin S^{-1} (ℑ (\sqrt{x}))$
193	191 192	eqtrid	$⊢ (φ \land x \in C) \to S (S^{-1} (ℑ (\sqrt{x}))) = \sin S^{-1} (ℑ (\sqrt{x}))$
194		f1ocnvfv2	$⊢ (S : [- \frac{π}{2}, \frac{π}{2}] \underset{1-1 onto}{⟶} [- 1, 1] \land ℑ (\sqrt{x}) \in [- 1, 1]) \to S (S^{-1} (ℑ (\sqrt{x}))) = ℑ (\sqrt{x})$
195	128 124 194	sylancr	$⊢ (φ \land x \in C) \to S (S^{-1} (ℑ (\sqrt{x}))) = ℑ (\sqrt{x})$
196	193 195	eqtr3d	$⊢ (φ \land x \in C) \to \sin S^{-1} (ℑ (\sqrt{x})) = ℑ (\sqrt{x})$
197	196	oveq1d	$⊢ (φ \land x \in C) \to {\sin S^{-1} (ℑ (\sqrt{x}))}^{2} = {ℑ (\sqrt{x})}^{2}$
198	190 197	oveq12d	$⊢ (φ \land x \in C) \to {\sin S^{-1} (ℑ (\sqrt{x}))}^{2} + {\cos S^{-1} (ℑ (\sqrt{x}))}^{2} - {\sin S^{-1} (ℑ (\sqrt{x}))}^{2} = {ℜ (\sqrt{x})}^{2} + {ℑ (\sqrt{x})}^{2} - {ℑ (\sqrt{x})}^{2}$
199	158	sincld	$⊢ (φ \land x \in C) \to \sin S^{-1} (ℑ (\sqrt{x})) \in ℂ$
200	199	sqcld	$⊢ (φ \land x \in C) \to {\sin S^{-1} (ℑ (\sqrt{x}))}^{2} \in ℂ$
201	158	coscld	$⊢ (φ \land x \in C) \to \cos S^{-1} (ℑ (\sqrt{x})) \in ℂ$
202	201	sqcld	$⊢ (φ \land x \in C) \to {\cos S^{-1} (ℑ (\sqrt{x}))}^{2} \in ℂ$
203	200 202	pncan2d	$⊢ (φ \land x \in C) \to {\sin S^{-1} (ℑ (\sqrt{x}))}^{2} + {\cos S^{-1} (ℑ (\sqrt{x}))}^{2} - {\sin S^{-1} (ℑ (\sqrt{x}))}^{2} = {\cos S^{-1} (ℑ (\sqrt{x}))}^{2}$
204	176	recnd	$⊢ (φ \land x \in C) \to ℜ (\sqrt{x}) \in ℂ$
205	204	sqcld	$⊢ (φ \land x \in C) \to {ℜ (\sqrt{x})}^{2} \in ℂ$
206	197 200	eqeltrrd	$⊢ (φ \land x \in C) \to {ℑ (\sqrt{x})}^{2} \in ℂ$
207	205 206	pncand	$⊢ (φ \land x \in C) \to {ℜ (\sqrt{x})}^{2} + {ℑ (\sqrt{x})}^{2} - {ℑ (\sqrt{x})}^{2} = {ℜ (\sqrt{x})}^{2}$
208	198 203 207	3eqtr3d	$⊢ (φ \land x \in C) \to {\cos S^{-1} (ℑ (\sqrt{x}))}^{2} = {ℜ (\sqrt{x})}^{2}$
209	168 176 178 179 208	sq11d	$⊢ (φ \land x \in C) \to \cos S^{-1} (ℑ (\sqrt{x})) = ℜ (\sqrt{x})$
210	196	oveq2d	$⊢ (φ \land x \in C) \to i \sin S^{-1} (ℑ (\sqrt{x})) = i ℑ (\sqrt{x})$
211	209 210	oveq12d	$⊢ (φ \land x \in C) \to \cos S^{-1} (ℑ (\sqrt{x})) + i \sin S^{-1} (ℑ (\sqrt{x})) = ℜ (\sqrt{x}) + i ℑ (\sqrt{x})$
212		efival	$⊢ S^{-1} (ℑ (\sqrt{x})) \in ℂ \to e^{i S^{-1} (ℑ (\sqrt{x}))} = \cos S^{-1} (ℑ (\sqrt{x})) + i \sin S^{-1} (ℑ (\sqrt{x}))$
213	158 212	syl	$⊢ (φ \land x \in C) \to e^{i S^{-1} (ℑ (\sqrt{x}))} = \cos S^{-1} (ℑ (\sqrt{x})) + i \sin S^{-1} (ℑ (\sqrt{x}))$
214	175	replimd	$⊢ (φ \land x \in C) \to \sqrt{x} = ℜ (\sqrt{x}) + i ℑ (\sqrt{x})$
215	211 213 214	3eqtr4d	$⊢ (φ \land x \in C) \to e^{i S^{-1} (ℑ (\sqrt{x}))} = \sqrt{x}$
216	215	oveq1d	$⊢ (φ \land x \in C) \to {e^{i S^{-1} (ℑ (\sqrt{x}))}}^{2} = {\sqrt{x}}^{2}$
217	167 216 182	3eqtrd	$⊢ (φ \land x \in C) \to e^{i 2 S^{-1} (ℑ (\sqrt{x}))} = x$
218	217	adantr	$⊢ ((φ \land x \in C) \land y \in D) \to e^{i 2 S^{-1} (ℑ (\sqrt{x}))} = x$
219	151 156 218	3eqtr3d	$⊢ ((φ \land x \in C) \land y \in D) \to e^{i (2 S^{-1} (ℑ (\sqrt{x})) - y)} e^{i y} = x$
220	147	efcld	$⊢ ((φ \land x \in C) \land y \in D) \to e^{i y} \in ℂ$
221	220	mullidd	$⊢ ((φ \land x \in C) \land y \in D) \to 1 e^{i y} = e^{i y}$
222	219 221	eqeq12d	$⊢ ((φ \land x \in C) \land y \in D) \to (e^{i (2 S^{-1} (ℑ (\sqrt{x})) - y)} e^{i y} = 1 e^{i y} \leftrightarrow x = e^{i y})$
223	138 222	imbitrid	$⊢ ((φ \land x \in C) \land y \in D) \to (e^{i (2 S^{-1} (ℑ (\sqrt{x})) - y)} = 1 \to x = e^{i y})$
224		efeq1	$⊢ i (2 S^{-1} (ℑ (\sqrt{x})) - y) \in ℂ \to (e^{i (2 S^{-1} (ℑ (\sqrt{x})) - y)} = 1 \leftrightarrow \frac{i (2 S^{-1} (ℑ (\sqrt{x})) - y)}{i 2 π} \in ℤ)$
225	154 224	syl	$⊢ ((φ \land x \in C) \land y \in D) \to (e^{i (2 S^{-1} (ℑ (\sqrt{x})) - y)} = 1 \leftrightarrow \frac{i (2 S^{-1} (ℑ (\sqrt{x})) - y)}{i 2 π} \in ℤ)$
226		divcan5	$⊢ (2 S^{-1} (ℑ (\sqrt{x})) - y \in ℂ \land (2 π \in ℂ \land 2 π \neq 0) \land (i \in ℂ \land i \neq 0)) \to \frac{i (2 S^{-1} (ℑ (\sqrt{x})) - y)}{i 2 π} = \frac{2 S^{-1} (ℑ (\sqrt{x})) - y}{2 π}$
227	62 64 226	mp3an23	$⊢ 2 S^{-1} (ℑ (\sqrt{x})) - y \in ℂ \to \frac{i (2 S^{-1} (ℑ (\sqrt{x})) - y)}{i 2 π} = \frac{2 S^{-1} (ℑ (\sqrt{x})) - y}{2 π}$
228	152 227	syl	$⊢ ((φ \land x \in C) \land y \in D) \to \frac{i (2 S^{-1} (ℑ (\sqrt{x})) - y)}{i 2 π} = \frac{2 S^{-1} (ℑ (\sqrt{x})) - y}{2 π}$
229	228	eleq1d	$⊢ ((φ \land x \in C) \land y \in D) \to (\frac{i (2 S^{-1} (ℑ (\sqrt{x})) - y)}{i 2 π} \in ℤ \leftrightarrow \frac{2 S^{-1} (ℑ (\sqrt{x})) - y}{2 π} \in ℤ)$
230	225 229	bitr2d	$⊢ ((φ \land x \in C) \land y \in D) \to (\frac{2 S^{-1} (ℑ (\sqrt{x})) - y}{2 π} \in ℤ \leftrightarrow e^{i (2 S^{-1} (ℑ (\sqrt{x})) - y)} = 1)$
231	88	adantl	$⊢ ((φ \land x \in C) \land y \in D) \to F (y) = e^{i y}$
232	231	eqeq2d	$⊢ ((φ \land x \in C) \land y \in D) \to (x = F (y) \leftrightarrow x = e^{i y})$
233	223 230 232	3imtr4d	$⊢ ((φ \land x \in C) \land y \in D) \to (\frac{2 S^{-1} (ℑ (\sqrt{x})) - y}{2 π} \in ℤ \to x = F (y))$
234	233	reximdva	$⊢ (φ \land x \in C) \to (\exists y \in D \frac{2 S^{-1} (ℑ (\sqrt{x})) - y}{2 π} \in ℤ \to \exists y \in D x = F (y))$
235	137 234	mpd	$⊢ (φ \land x \in C) \to \exists y \in D x = F (y)$
236	235	ralrimiva	$⊢ φ \to \forall x \in C \exists y \in D x = F (y)$
237		dffo3	$⊢ F : D \underset{onto}{⟶} C \leftrightarrow (F : D ⟶ C \land \forall x \in C \exists y \in D x = F (y))$
238	22 236 237	sylanbrc	$⊢ φ \to F : D \underset{onto}{⟶} C$
239		df-f1o	$⊢ F : D \underset{1-1 onto}{⟶} C \leftrightarrow (F : D \underset{1-1}{⟶} C \land F : D \underset{onto}{⟶} C)$
240	113 238 239	sylanbrc	$⊢ φ \to F : D \underset{1-1 onto}{⟶} C$

Metamath Proof Explorer

Theorem efif1olem4

Proof