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

Metamath Proof Explorer

Theorem efif1olem4

Proof