effoi - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem effoi 8666

Description: The exponential function maps the set S, of complex numbers with imaginary part in a closed-below, open-above real interval of length 2 · π starting at A, onto the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.)

**Hypotheses**
Ref	Expression
eff1i.1	⊢ A ∈ ℝ
eff1i.2	⊢ D = (A[,)(A + (2 · π)))
eff1i.3	⊢ S = {v ∈ ℂ∣(ℑ ‘v) ∈ D}
eff1i.4	⊢ F = {⟨z, w⟩∣(z ∈ D ⋀ w = (exp ‘(i · z)))}
eff1i.5	⊢ C = {v ∈ ℂ∣(abs ‘v) = 1}

**Assertion**
Ref	Expression
effoi	⊢ (exp ↾ S):S–onto→(ℂ ∖ {0})

Distinct variable groups: v,A,w,z v,D,w,z w,C,z v,F

**Proof of Theorem effoi**
Step	Hyp	Ref	Expression
1		dffo3 3804	. 2 ⊢ ((exp ↾ S):S–onto→(ℂ ∖ {0}) ↔ ((exp ↾ S):S–→(ℂ ∖ {0}) ⋀ ∀y ∈ (ℂ ∖ {0})∃x ∈ S y = ((exp ↾ S) ‘x)))
2		eff2 7312	. . 3 ⊢ exp:ℂ–→(ℂ ∖ {0})
3		fveq2 3709	. . . . . . 7 ⊢ (v = x → (ℑ ‘v) = (ℑ ‘x))
4	3	eleq1d 1532	. . . . . 6 ⊢ (v = x → ((ℑ ‘v) ∈ D ↔ (ℑ ‘x) ∈ D))
5		eff1i.3	. . . . . 6 ⊢ S = {v ∈ ℂ∣(ℑ ‘v) ∈ D}
6	4, 5	elrab2 1898	. . . . 5 ⊢ (x ∈ S ↔ (x ∈ ℂ ⋀ (ℑ ‘x) ∈ D))
7	6	pm3.26bi 322	. . . 4 ⊢ (x ∈ S → x ∈ ℂ)
8	7	ssriv 2059	. . 3 ⊢ S ⊆ ℂ
9		fssres 3628	. . 3 ⊢ ((exp:ℂ–→(ℂ ∖ {0}) ⋀ S ⊆ ℂ) → (exp ↾ S):S–→(ℂ ∖ {0}))
10	2, 8, 9	mp2an 695	. 2 ⊢ (exp ↾ S):S–→(ℂ ∖ {0})
11		fveq2 3709	. . . . . 6 ⊢ (x = ((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y))))) → ((exp ↾ S) ‘x) = ((exp ↾ S) ‘((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y)))))))
12	11	eqeq2d 1478	. . . . 5 ⊢ (x = ((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y))))) → (y = ((exp ↾ S) ‘x) ↔ y = ((exp ↾ S) ‘((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y))))))))
13	12	rcla4ev 1868	. . . 4 ⊢ ((((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y))))) ∈ S ⋀ y = ((exp ↾ S) ‘((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y))))))) → ∃x ∈ S y = ((exp ↾ S) ‘x))
14		fveq2 3709	. . . . . . . 8 ⊢ (v = ((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y))))) → (ℑ ‘v) = (ℑ ‘((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y)))))))
15	14	eleq1d 1532	. . . . . . 7 ⊢ (v = ((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y))))) → ((ℑ ‘v) ∈ D ↔ (ℑ ‘((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y)))))) ∈ D))
16	15, 5	elrab2 1898	. . . . . 6 ⊢ (((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y))))) ∈ S ↔ (((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y))))) ∈ ℂ ⋀ (ℑ ‘((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y)))))) ∈ D))
17	16	biimpr 152	. . . . 5 ⊢ ((((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y))))) ∈ ℂ ⋀ (ℑ ‘((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y)))))) ∈ D) → ((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y))))) ∈ S)
18		axaddcl 5243	. . . . . 6 ⊢ (((^◡(exp ↾ ℝ) ‘(abs ‘y)) ∈ ℂ ⋀ (i · (^◡F ‘(y / (abs ‘y)))) ∈ ℂ) → ((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y))))) ∈ ℂ)
19		elrp 6220	. . . . . . . . . 10 ⊢ ((abs ‘y) ∈ ℝ⁺ ↔ ((abs ‘y) ∈ ℝ ⋀ 0 < (abs ‘y)))
20	19	biimpr 152	. . . . . . . . 9 ⊢ (((abs ‘y) ∈ ℝ ⋀ 0 < (abs ‘y)) → (abs ‘y) ∈ ℝ⁺)
21		eldifi 2152	. . . . . . . . . 10 ⊢ (y ∈ (ℂ ∖ {0}) → y ∈ ℂ)
22		absclt 6768	. . . . . . . . . 10 ⊢ (y ∈ ℂ → (abs ‘y) ∈ ℝ)
23	21, 22	syl 10	. . . . . . . . 9 ⊢ (y ∈ (ℂ ∖ {0}) → (abs ‘y) ∈ ℝ)
24		eldifsn 2453	. . . . . . . . . 10 ⊢ (y ∈ (ℂ ∖ {0}) ↔ (y ∈ ℂ ⋀ y ≠ 0))
25		absgt0t 6831	. . . . . . . . . . 11 ⊢ (y ∈ ℂ → (y ≠ 0 ↔ 0 < (abs ‘y)))
26	25	biimpa 416	. . . . . . . . . 10 ⊢ ((y ∈ ℂ ⋀ y ≠ 0) → 0 < (abs ‘y))
27	24, 26	sylbi 199	. . . . . . . . 9 ⊢ (y ∈ (ℂ ∖ {0}) → 0 < (abs ‘y))
28	20, 23, 27	sylanc 471	. . . . . . . 8 ⊢ (y ∈ (ℂ ∖ {0}) → (abs ‘y) ∈ ℝ⁺)
29		reeff1o2 7369	. . . . . . . . . . 11 ⊢ (exp ↾ ℝ):ℝ–1-1-onto→ℝ⁺
30		f1ocnv 3686	. . . . . . . . . . 11 ⊢ ((exp ↾ ℝ):ℝ–1-1-onto→ℝ⁺ → ^◡(exp ↾ ℝ):ℝ⁺–1-1-onto→ℝ)
31	29, 30	ax-mp 7	. . . . . . . . . 10 ⊢ ^◡(exp ↾ ℝ):ℝ⁺–1-1-onto→ℝ
32		f1of 3674	. . . . . . . . . 10 ⊢ (^◡(exp ↾ ℝ):ℝ⁺–1-1-onto→ℝ → ^◡(exp ↾ ℝ):ℝ⁺–→ℝ)
33	31, 32	ax-mp 7	. . . . . . . . 9 ⊢ ^◡(exp ↾ ℝ):ℝ⁺–→ℝ
34	33	ffvelrni 3800	. . . . . . . 8 ⊢ ((abs ‘y) ∈ ℝ⁺ → (^◡(exp ↾ ℝ) ‘(abs ‘y)) ∈ ℝ)
35	28, 34	syl 10	. . . . . . 7 ⊢ (y ∈ (ℂ ∖ {0}) → (^◡(exp ↾ ℝ) ‘(abs ‘y)) ∈ ℝ)
36	35	recnd 5287	. . . . . 6 ⊢ (y ∈ (ℂ ∖ {0}) → (^◡(exp ↾ ℝ) ‘(abs ‘y)) ∈ ℂ)
37		fveq2 3709	. . . . . . . . . . . . 13 ⊢ (v = (y / (abs ‘y)) → (abs ‘v) = (abs ‘(y / (abs ‘y))))
38	37	eqeq1d 1475	. . . . . . . . . . . 12 ⊢ (v = (y / (abs ‘y)) → ((abs ‘v) = 1 ↔ (abs ‘(y / (abs ‘y))) = 1))
39		eff1i.5	. . . . . . . . . . . 12 ⊢ C = {v ∈ ℂ∣(abs ‘v) = 1}
40	38, 39	elrab2 1898	. . . . . . . . . . 11 ⊢ ((y / (abs ‘y)) ∈ C ↔ ((y / (abs ‘y)) ∈ ℂ ⋀ (abs ‘(y / (abs ‘y))) = 1))
41	40	biimpr 152	. . . . . . . . . 10 ⊢ (((y / (abs ‘y)) ∈ ℂ ⋀ (abs ‘(y / (abs ‘y))) = 1) → (y / (abs ‘y)) ∈ C)
42		divclt 5681	. . . . . . . . . . 11 ⊢ ((y ∈ ℂ ⋀ (abs ‘y) ∈ ℂ ⋀ (abs ‘y) ≠ 0) → (y / (abs ‘y)) ∈ ℂ)
43	23	recnd 5287	. . . . . . . . . . 11 ⊢ (y ∈ (ℂ ∖ {0}) → (abs ‘y) ∈ ℂ)
44		gt0ne0t 5592	. . . . . . . . . . . 12 ⊢ (((abs ‘y) ∈ ℝ ⋀ 0 < (abs ‘y)) → (abs ‘y) ≠ 0)
45	44, 23, 27	sylanc 471	. . . . . . . . . . 11 ⊢ (y ∈ (ℂ ∖ {0}) → (abs ‘y) ≠ 0)
46	42, 21, 43, 45	syl3anc 856	. . . . . . . . . 10 ⊢ (y ∈ (ℂ ∖ {0}) → (y / (abs ‘y)) ∈ ℂ)
47		absdivt 6795	. . . . . . . . . . . 12 ⊢ ((y ∈ ℂ ⋀ (abs ‘y) ∈ ℂ ⋀ (abs ‘y) ≠ 0) → (abs ‘(y / (abs ‘y))) = ((abs ‘y) / (abs ‘(abs ‘y))))
48	47, 21, 43, 45	syl3anc 856	. . . . . . . . . . 11 ⊢ (y ∈ (ℂ ∖ {0}) → (abs ‘(y / (abs ‘y))) = ((abs ‘y) / (abs ‘(abs ‘y))))
49		absidmt 6830	. . . . . . . . . . . . 13 ⊢ (y ∈ ℂ → (abs ‘(abs ‘y)) = (abs ‘y))
50	49	opreq2d 3961	. . . . . . . . . . . 12 ⊢ (y ∈ ℂ → ((abs ‘y) / (abs ‘(abs ‘y))) = ((abs ‘y) / (abs ‘y)))
51	21, 50	syl 10	. . . . . . . . . . 11 ⊢ (y ∈ (ℂ ∖ {0}) → ((abs ‘y) / (abs ‘(abs ‘y))) = ((abs ‘y) / (abs ‘y)))
52		dividt 5722	. . . . . . . . . . . 12 ⊢ (((abs ‘y) ∈ ℂ ⋀ (abs ‘y) ≠ 0) → ((abs ‘y) / (abs ‘y)) = 1)
53	52, 43, 45	sylanc 471	. . . . . . . . . . 11 ⊢ (y ∈ (ℂ ∖ {0}) → ((abs ‘y) / (abs ‘y)) = 1)
54	48, 51, 53	3eqtrd 1503	. . . . . . . . . 10 ⊢ (y ∈ (ℂ ∖ {0}) → (abs ‘(y / (abs ‘y))) = 1)
55	41, 46, 54	sylanc 471	. . . . . . . . 9 ⊢ (y ∈ (ℂ ∖ {0}) → (y / (abs ‘y)) ∈ C)
56		eff1i.1	. . . . . . . . . . . . 13 ⊢ A ∈ ℝ
57		eff1i.2	. . . . . . . . . . . . . 14 ⊢ D = (A[,)(A + (2 · π)))
58		eff1i.4	. . . . . . . . . . . . . 14 ⊢ F = {⟨z, w⟩∣(z ∈ D ⋀ w = (exp ‘(i · z)))}
59	57, 58, 39	shftefif1o 8663	. . . . . . . . . . . . 13 ⊢ (A ∈ ℝ → F:D–1-1-onto→C)
60	56, 59	ax-mp 7	. . . . . . . . . . . 12 ⊢ F:D–1-1-onto→C
61		f1ocnv 3686	. . . . . . . . . . . 12 ⊢ (F:D–1-1-onto→C → ^◡F:C–1-1-onto→D)
62	60, 61	ax-mp 7	. . . . . . . . . . 11 ⊢ ^◡F:C–1-1-onto→D
63		f1of 3674	. . . . . . . . . . 11 ⊢ (^◡F:C–1-1-onto→D → ^◡F:C–→D)
64	62, 63	ax-mp 7	. . . . . . . . . 10 ⊢ ^◡F:C–→D
65	64	ffvelrni 3800	. . . . . . . . 9 ⊢ ((y / (abs ‘y)) ∈ C → (^◡F ‘(y / (abs ‘y))) ∈ D)
66	57	eleq2i 1530	. . . . . . . . . . . 12 ⊢ ((^◡F ‘(y / (abs ‘y))) ∈ D ↔ (^◡F ‘(y / (abs ‘y))) ∈ (A[,)(A + (2 · π))))
67		2re 5926	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
68		pire 8596	. . . . . . . . . . . . . . 15 ⊢ π ∈ ℝ
69	67, 68	remulcl 5307	. . . . . . . . . . . . . 14 ⊢ (2 · π) ∈ ℝ
70	56, 69	readdcl 5306	. . . . . . . . . . . . 13 ⊢ (A + (2 · π)) ∈ ℝ
71		elico2t 6323	. . . . . . . . . . . . 13 ⊢ ((A ∈ ℝ ⋀ (A + (2 · π)) ∈ ℝ) → ((^◡F ‘(y / (abs ‘y))) ∈ (A[,)(A + (2 · π))) ↔ ((^◡F ‘(y / (abs ‘y))) ∈ ℝ ⋀ A ≤ (^◡F ‘(y / (abs ‘y))) ⋀ (^◡F ‘(y / (abs ‘y))) < (A + (2 · π)))))
72	56, 70, 71	mp2an 695	. . . . . . . . . . . 12 ⊢ ((^◡F ‘(y / (abs ‘y))) ∈ (A[,)(A + (2 · π))) ↔ ((^◡F ‘(y / (abs ‘y))) ∈ ℝ ⋀ A ≤ (^◡F ‘(y / (abs ‘y))) ⋀ (^◡F ‘(y / (abs ‘y))) < (A + (2 · π))))
73	66, 72	bitr 173	. . . . . . . . . . 11 ⊢ ((^◡F ‘(y / (abs ‘y))) ∈ D ↔ ((^◡F ‘(y / (abs ‘y))) ∈ ℝ ⋀ A ≤ (^◡F ‘(y / (abs ‘y))) ⋀ (^◡F ‘(y / (abs ‘y))) < (A + (2 · π))))
74	73	biimp 151	. . . . . . . . . 10 ⊢ ((^◡F ‘(y / (abs ‘y))) ∈ D → ((^◡F ‘(y / (abs ‘y))) ∈ ℝ ⋀ A ≤ (^◡F ‘(y / (abs ‘y))) ⋀ (^◡F ‘(y / (abs ‘y))) < (A + (2 · π))))
75	74	3simp1d 792	. . . . . . . . 9 ⊢ ((^◡F ‘(y / (abs ‘y))) ∈ D → (^◡F ‘(y / (abs ‘y))) ∈ ℝ)
76	55, 65, 75	3syl 20	. . . . . . . 8 ⊢ (y ∈ (ℂ ∖ {0}) → (^◡F ‘(y / (abs ‘y))) ∈ ℝ)
77	76	recnd 5287	. . . . . . 7 ⊢ (y ∈ (ℂ ∖ {0}) → (^◡F ‘(y / (abs ‘y))) ∈ ℂ)
78		axicn 5242	. . . . . . . 8 ⊢ i ∈ ℂ
79		axmulcl 5245	. . . . . . . 8 ⊢ ((i ∈ ℂ ⋀ (^◡F ‘(y / (abs ‘y))) ∈ ℂ) → (i · (^◡F ‘(y / (abs ‘y)))) ∈ ℂ)
80	78, 79	mpan 693	. . . . . . 7 ⊢ ((^◡F ‘(y / (abs ‘y))) ∈ ℂ → (i · (^◡F ‘(y / (abs ‘y)))) ∈ ℂ)
81	77, 80	syl 10	. . . . . 6 ⊢ (y ∈ (ℂ ∖ {0}) → (i · (^◡F ‘(y / (abs ‘y)))) ∈ ℂ)
82	18, 36, 81	sylanc 471	. . . . 5 ⊢ (y ∈ (ℂ ∖ {0}) → ((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y))))) ∈ ℂ)
83		crimt 6704	. . . . . . 7 ⊢ (((^◡(exp ↾ ℝ) ‘(abs ‘y)) ∈ ℝ ⋀ (^◡F ‘(y / (abs ‘y))) ∈ ℝ) → (ℑ ‘((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y)))))) = (^◡F ‘(y / (abs ‘y))))
84	83, 35, 76	sylanc 471	. . . . . 6 ⊢ (y ∈ (ℂ ∖ {0}) → (ℑ ‘((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y)))))) = (^◡F ‘(y / (abs ‘y))))
85	55, 65	syl 10	. . . . . 6 ⊢ (y ∈ (ℂ ∖ {0}) → (^◡F ‘(y / (abs ‘y))) ∈ D)
86	84, 85	eqeltrd 1540	. . . . 5 ⊢ (y ∈ (ℂ ∖ {0}) → (ℑ ‘((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y)))))) ∈ D)
87	17, 82, 86	sylanc 471	. . . 4 ⊢ (y ∈ (ℂ ∖ {0}) → ((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y))))) ∈ S)
88		fvres 3719	. . . . . 6 ⊢ (((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y))))) ∈ S → ((exp ↾ S) ‘((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y)))))) = (exp ‘((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y)))))))
89	87, 88	syl 10	. . . . 5 ⊢ (y ∈ (ℂ ∖ {0}) → ((exp ↾ S) ‘((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y)))))) = (exp ‘((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y)))))))
90		efaddt 7309	. . . . . . 7 ⊢ (((^◡(exp ↾ ℝ) ‘(abs ‘y)) ∈ ℂ ⋀ (i · (^◡F ‘(y / (abs ‘y)))) ∈ ℂ) → (exp ‘((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y)))))) = ((exp ‘(^◡(exp ↾ ℝ) ‘(abs ‘y))) · (exp ‘(i · (^◡F ‘(y / (abs ‘y)))))))
91	90, 36, 81	sylanc 471	. . . . . 6 ⊢ (y ∈ (ℂ ∖ {0}) → (exp ‘((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y)))))) = ((exp ‘(^◡(exp ↾ ℝ) ‘(abs ‘y))) · (exp ‘(i · (^◡F ‘(y / (abs ‘y)))))))
92		fvres 3719	. . . . . . . . 9 ⊢ ((^◡(exp ↾ ℝ) ‘(abs ‘y)) ∈ ℝ → ((exp ↾ ℝ) ‘(^◡(exp ↾ ℝ) ‘(abs ‘y))) = (exp ‘(^◡(exp ↾ ℝ) ‘(abs ‘y))))
93	35, 92	syl 10	. . . . . . . 8 ⊢ (y ∈ (ℂ ∖ {0}) → ((exp ↾ ℝ) ‘(^◡(exp ↾ ℝ) ‘(abs ‘y))) = (exp ‘(^◡(exp ↾ ℝ) ‘(abs ‘y))))
94		f1ocnvfv2 3864	. . . . . . . . . 10 ⊢ (((exp ↾ ℝ):ℝ–1-1-onto→ℝ⁺ ⋀ (abs ‘y) ∈ ℝ⁺) → ((exp ↾ ℝ) ‘(^◡(exp ↾ ℝ) ‘(abs ‘y))) = (abs ‘y))
95	29, 94	mpan 693	. . . . . . . . 9 ⊢ ((abs ‘y) ∈ ℝ⁺ → ((exp ↾ ℝ) ‘(^◡(exp ↾ ℝ) ‘(abs ‘y))) = (abs ‘y))
96	28, 95	syl 10	. . . . . . . 8 ⊢ (y ∈ (ℂ ∖ {0}) → ((exp ↾ ℝ) ‘(^◡(exp ↾ ℝ) ‘(abs ‘y))) = (abs ‘y))
97	93, 96	eqtr3d 1501	. . . . . . 7 ⊢ (y ∈ (ℂ ∖ {0}) → (exp ‘(^◡(exp ↾ ℝ) ‘(abs ‘y))) = (abs ‘y))
98		opreq2 3954	. . . . . . . . . . 11 ⊢ (a = (^◡F ‘(y / (abs ‘y))) → (i · a) = (i · (^◡F ‘(y / (abs ‘y)))))
99	98	fveq2d 3713	. . . . . . . . . 10 ⊢ (a = (^◡F ‘(y / (abs ‘y))) → (exp ‘(i · a)) = (exp ‘(i · (^◡F ‘(y / (abs ‘y))))))
100		eleq1 1526	. . . . . . . . . . . . . 14 ⊢ (z = a → (z ∈ D ↔ a ∈ D))
101	100	adantr 389	. . . . . . . . . . . . 13 ⊢ ((z = a ⋀ w = b) → (z ∈ D ↔ a ∈ D))
102		id 59	. . . . . . . . . . . . . 14 ⊢ (w = b → w = b)
103		opreq2 3954	. . . . . . . . . . . . . . 15 ⊢ (z = a → (i · z) = (i · a))
104	103	fveq2d 3713	. . . . . . . . . . . . . 14 ⊢ (z = a → (exp ‘(i · z)) = (exp ‘(i · a)))
105	102, 104	eqeqan12rd 1483	. . . . . . . . . . . . 13 ⊢ ((z = a ⋀ w = b) → (w = (exp ‘(i · z)) ↔ b = (exp ‘(i · a))))
106	101, 105	anbi12d 626	. . . . . . . . . . . 12 ⊢ ((z = a ⋀ w = b) → ((z ∈ D ⋀ w = (exp ‘(i · z))) ↔ (a ∈ D ⋀ b = (exp ‘(i · a)))))
107	106	cbvopabv 2663	. . . . . . . . . . 11 ⊢ {⟨z, w⟩∣(z ∈ D ⋀ w = (exp ‘(i · z)))} = {⟨a, b⟩∣(a ∈ D ⋀ b = (exp ‘(i · a)))}
108	58, 107	eqtr 1487	. . . . . . . . . 10 ⊢ F = {⟨a, b⟩∣(a ∈ D ⋀ b = (exp ‘(i · a)))}
109		fvex 3717	. . . . . . . . . 10 ⊢ (exp ‘(i · (^◡F ‘(y / (abs ‘y))))) ∈ V
110	99, 108, 109	fvopab4 3765	. . . . . . . . 9 ⊢ ((^◡F ‘(y / (abs ‘y))) ∈ D → (F ‘(^◡F ‘(y / (abs ‘y)))) = (exp ‘(i · (^◡F ‘(y / (abs ‘y))))))
111	55, 65, 110	3syl 20	. . . . . . . 8 ⊢ (y ∈ (ℂ ∖ {0}) → (F ‘(^◡F ‘(y / (abs ‘y)))) = (exp ‘(i · (^◡F ‘(y / (abs ‘y))))))
112		f1ocnvfv2 3864	. . . . . . . . . 10 ⊢ ((F:D–1-1-onto→C ⋀ (y / (abs ‘y)) ∈ C) → (F ‘(^◡F ‘(y / (abs ‘y)))) = (y / (abs ‘y)))
113	60, 112	mpan 693	. . . . . . . . 9 ⊢ ((y / (abs ‘y)) ∈ C → (F ‘(^◡F ‘(y / (abs ‘y)))) = (y / (abs ‘y)))
114	55, 113	syl 10	. . . . . . . 8 ⊢ (y ∈ (ℂ ∖ {0}) → (F ‘(^◡F ‘(y / (abs ‘y)))) = (y / (abs ‘y)))
115	111, 114	eqtr3d 1501	. . . . . . 7 ⊢ (y ∈ (ℂ ∖ {0}) → (exp ‘(i · (^◡F ‘(y / (abs ‘y))))) = (y / (abs ‘y)))
116	97, 115	opreq12d 3963	. . . . . 6 ⊢ (y ∈ (ℂ ∖ {0}) → ((exp ‘(^◡(exp ↾ ℝ) ‘(abs ‘y))) · (exp ‘(i · (^◡F ‘(y / (abs ‘y)))))) = ((abs ‘y) · (y / (abs ‘y))))
117		divcan2t 5690	. . . . . . 7 ⊢ (((abs ‘y) ∈ ℂ ⋀ y ∈ ℂ ⋀ (abs ‘y) ≠ 0) → ((abs ‘y) · (y / (abs ‘y))) = y)
118	117, 43, 21, 45	syl3anc 856	. . . . . 6 ⊢ (y ∈ (ℂ ∖ {0}) → ((abs ‘y) · (y / (abs ‘y))) = y)
119	91, 116, 118	3eqtrd 1503	. . . . 5 ⊢ (y ∈ (ℂ ∖ {0}) → (exp ‘((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y)))))) = y)
120	89, 119	eqtr2d 1500	. . . 4 ⊢ (y ∈ (ℂ ∖ {0}) → y = ((exp ↾ S) ‘((^◡(exp ↾ ℝ) ‘(abs ‘y)) + (i · (^◡F ‘(y / (abs ‘y)))))))
121	13, 87, 120	sylanc 471	. . 3 ⊢ (y ∈ (ℂ ∖ {0}) → ∃x ∈ S y = ((exp ↾ S) ‘x))
122	121	rgen 1690	. 2 ⊢ ∀y ∈ (ℂ ∖ {0})∃x ∈ S y = ((exp ↾ S) ‘x)
123	1, 10, 122	mpbir2an 728	1 ⊢ (exp ↾ S):S–onto→(ℂ ∖ {0})

Colors of variables: wff set class

Syntax hints: ↔ wb 146 ⋀ wa 223 ⋀ w3a 773 = wceq 953 ∈ wcel 955 ≠ wne 1577 ∀wral 1637 ∃wrex 1638 {crab 1640 ∖ cdif 2034 ⊆ wss 2037 {csn 2399 class class class wbr 2609 {copab 2656 ^◡ccnv 3159 ↾ cres 3162 –→wf 3168 –onto→wfo 3170 –1-1-onto→wf1o 3171 ‘cfv 3172 (class class class)co 3948 ℂcc 5204 ℝcr 5205 0cc0 5206 1c1 5207 ici 5208 + caddc 5209 · cmul 5211 / cdiv 5266 ≤ cle 5267 ℝ⁺crp 5272 < clt 5458 2c2 5908 [,)cico 6296 ℑcim 6679 abscabs 6681 expce 7235 πcpi 7239

This theorem is referenced by: eff1oi 8668

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 959 ax-gen 960 ax-8 961 ax-9 962 ax-10 963 ax-11 964 ax-12 965 ax-13 966 ax-14 967 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-10o 1136 ax-16 1206 ax-11o 1213 ax-ext 1452 ax-rep 2683 ax-sep 2693 ax-nul 2700 ax-pow 2732 ax-pr 2769 ax-un 2857 ax-reg 4565 ax-inf2 4597 ax-ac 4716

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 774 df-3an 775 df-ex 978 df-sb 1168 df-eu 1375 df-mo 1376 df-clab 1457 df-cleq 1462 df-clel 1465 df-ne 1579 df-nel 1580 df-ral 1641 df-rex 1642 df-reu 1643 df-rab 1644 df-v 1803 df-sbc 1932 df-csb 1992 df-dif 2039 df-un 2040 df-in 2041 df-ss 2043 df-pss 2045 df-nul 2271 df-if 2352 df-pw 2392 df-sn 2402 df-pr 2403 df-tp 2405 df-op 2406 df-uni 2494 df-int 2524 df-iun 2558 df-iin 2559 df-br 2610 df-opab 2657 df-tr 2671 df-eprel 2821 df-id 2824 df-po 2831 df-so 2841 df-fr 2907 df-we 2924 df-ord 2941 df-on 2942 df-lim 2943 df-suc 2944 df-om 3122 df-xp 3174 df-rel 3175 df-cnv 3176 df-co 3177 df-dm 3178 df-rn 3179 df-res 3180 df-ima 3181 df-fun 3182 df-fn 3183 df-f 3184 df-f1 3185 df-fo 3186 df-f1o 3187 df-fv 3188 df-rdg 3917 df-opr 3950 df-oprab 3951 df-1st 4063 df-2nd 4064 df-1o 4117 df-oadd 4119 df-omul 4120 df-er 4245 df-ec 4247 df-qs 4250 df-map 4308 df-en 4351 df-dom 4352 df-sdom 4353 df-sup 4548 df-r1 4615 df-rank 4616 df-ni 4972 df-pli 4973 df-mi 4974 df-lti 4975 df-plpq 5007 df-mpq 5008 df-enq 5009 df-nq 5010 df-plq 5011 df-mq 5012 df-rq 5013 df-ltq 5014 df-1q 5015 df-np 5058 df-1p 5059 df-plp 5060 df-mp 5061 df-ltp 5062 df-plpr 5136 df-mpr 5137 df-enr 5138 df-nr 5139 df-plr 5140 df-mr 5141 df-ltr 5142 df-0r 5143 df-1r 5144 df-m1r 5145 df-c 5212 df-0 5213 df-1 5214 df-i 5215 df-r 5216 df-plus 5217 df-mul 5218 df-lt 5219 df-sub 5328 df-neg 5330 df-pnf 5459 df-mnf 5460 df-xr 5461 df-ltxr 5462 df-le 5463 df-div 5672 df-n 5873 df-2 5917 df-3 5918 df-4 5919 df-5 5920 df-6 5921 df-7 5922 df-8 5923 df-9 5924 df-n0 6047 df-z 6083 df-fl 6172 df-q 6194 df-rp 6219 df-seq1 6245 df-shft 6278 df-ioo 6298 df-ioc 6299 df-ico 6300 df-icc 6301 df-uz 6350 df-fz 6400 df-seqz 6465 df-seq0 6466 df-exp 6501 df-sqr 6600 df-re 6682 df-im 6683 df-cj 6684 df-abs 6685 df-fac 6869 df-bc 6894 df-clim 6913 df-sum 6918 df-cncf 7198 df-ef 7240 df-sin 7242 df-cos 7243 df-pi 7244 df-top 7534 df-cn 7694 df-cnp 7695 df-met 7732 df-bl 7734 df-opn 7735 df-lm 7860 df-grp 7971 df-gid 7972 df-ginv 7973 df-gdiv 7974 df-abl 8036 df-subg 8052