Theorem eff1olem 26877

Description: The exponential function maps the set 𝑆, of complex numbers with imaginary part in a real interval of length 2 · π, one-to-one onto the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.) (Proof shortened by Mario Carneiro, 13-May-2014.)

Hypotheses

Ref	Expression
eff1olem.1	⊢ 𝐹 = (𝑤 ∈ 𝐷 ↦ (exp‘(i · 𝑤)))
eff1olem.2	⊢ 𝑆 = (◡ℑ “ 𝐷)
eff1olem.3	⊢ (𝜑 → 𝐷 ⊆ ℝ)
eff1olem.4	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → (abs‘(𝑥 − 𝑦)) < (2 · π))
eff1olem.5	⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → ∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈ ℤ)

Assertion

Ref	Expression
eff1olem	⊢ (𝜑 → (exp ↾ 𝑆):𝑆–1-1-onto→(ℂ ∖ {0}))

Distinct variable groups:   𝑥,𝑤,𝑦,𝑧,𝐷   𝑥,𝐹,𝑦,𝑧   𝜑,𝑤,𝑥,𝑦,𝑧   𝑥,𝑆,𝑦

Allowed substitution hints:   𝑆(𝑧, 𝑤)   𝐹(𝑤)

Proof of Theorem eff1olem

Step	Hyp	Ref	Expression
1		cnvimass 6199	. . . 4 ⊢ (◡ℑ “ 𝐷) ⊆ dom ℑ
2		eff1olem.2	. . . 4 ⊢ 𝑆 = (◡ℑ “ 𝐷)
3		imf 15281	. . . . . 6 ⊢ ℑ:ℂ⟶ℝ
4	3	fdmi 6722	. . . . 5 ⊢ dom ℑ = ℂ
5	4	eqcomi 2770	. . . 4 ⊢ ℂ = dom ℑ
6	1, 2, 5	3sstr4i 3980	. . 3 ⊢ 𝑆 ⊆ ℂ
7		eff2 16268	. . . . . . 7 ⊢ exp:ℂ⟶(ℂ ∖ {0})
8	7	a1i 11	. . . . . 6 ⊢ (𝑆 ⊆ ℂ → exp:ℂ⟶(ℂ ∖ {0}))
9	8	feqmptd 6954	. . . . 5 ⊢ (𝑆 ⊆ ℂ → exp = (𝑦 ∈ ℂ ↦ (exp‘𝑦)))
10	9	reseq1d 5969	. . . 4 ⊢ (𝑆 ⊆ ℂ → (exp ↾ 𝑆) = ((𝑦 ∈ ℂ ↦ (exp‘𝑦)) ↾ 𝑆))
11		resmpt 6029	. . . 4 ⊢ (𝑆 ⊆ ℂ → ((𝑦 ∈ ℂ ↦ (exp‘𝑦)) ↾ 𝑆) = (𝑦 ∈ 𝑆 ↦ (exp‘𝑦)))
12	10, 11	eqtrd 2796	. . 3 ⊢ (𝑆 ⊆ ℂ → (exp ↾ 𝑆) = (𝑦 ∈ 𝑆 ↦ (exp‘𝑦)))
13	6, 12	ax-mp 5	. 2 ⊢ (exp ↾ 𝑆) = (𝑦 ∈ 𝑆 ↦ (exp‘𝑦))
14	6	sseli 3925	. . . 4 ⊢ (𝑦 ∈ 𝑆 → 𝑦 ∈ ℂ)
15	7	ffvelcdmi 7084	. . . 4 ⊢ (𝑦 ∈ ℂ → (exp‘𝑦) ∈ (ℂ ∖ {0}))
16	14, 15	syl 18	. . 3 ⊢ (𝑦 ∈ 𝑆 → (exp‘𝑦) ∈ (ℂ ∖ {0}))
17	16	adantl 487	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (exp‘𝑦) ∈ (ℂ ∖ {0}))
18		eldifsn 4748	. . . . . . . . . 10 ⊢ (𝑥 ∈ (ℂ ∖ {0}) ↔ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
19	18	bilani 510	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
20	19	simpld 500	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑥 ∈ ℂ)
21	19	simprd 501	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑥 ≠ 0)
22	20, 21	absrpcld 15619	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (abs‘𝑥) ∈ ℝ+)
23		reeff1o 26775	. . . . . . . . 9 ⊢ (exp ↾ ℝ):ℝ–1-1-onto→ℝ+
24		f1ocnv 6838	. . . . . . . . 9 ⊢ ((exp ↾ ℝ):ℝ–1-1-onto→ℝ+ → ◡(exp ↾ ℝ):ℝ+–1-1-onto→ℝ)
25		f1of 6825	. . . . . . . . 9 ⊢ (◡(exp ↾ ℝ):ℝ+–1-1-onto→ℝ → ◡(exp ↾ ℝ):ℝ+⟶ℝ)
26	23, 24, 25	mp2b 10	. . . . . . . 8 ⊢ ◡(exp ↾ ℝ):ℝ+⟶ℝ
27	26	ffvelcdmi 7084	. . . . . . 7 ⊢ ((abs‘𝑥) ∈ ℝ+ → (◡(exp ↾ ℝ)‘(abs‘𝑥)) ∈ ℝ)
28	22, 27	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (◡(exp ↾ ℝ)‘(abs‘𝑥)) ∈ ℝ)
29	28	recnd 11338	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (◡(exp ↾ ℝ)‘(abs‘𝑥)) ∈ ℂ)
30		ax-icn 11260	. . . . . 6 ⊢ i ∈ ℂ
31		eff1olem.3	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ⊆ ℝ)
32	31	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝐷 ⊆ ℝ)
33		eff1olem.1	. . . . . . . . . . . 12 ⊢ 𝐹 = (𝑤 ∈ 𝐷 ↦ (exp‘(i · 𝑤)))
34		eqid 2761	. . . . . . . . . . . 12 ⊢ (◡abs “ {1}) = (◡abs “ {1})
35		eff1olem.4	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → (abs‘(𝑥 − 𝑦)) < (2 · π))
36		eff1olem.5	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → ∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈ ℤ)
37		eqid 2761	. . . . . . . . . . . 12 ⊢ (sin ↾ ( -(π / 2)[,](π / 2))) = (sin ↾ ( -(π / 2)[,](π / 2)))
38	33, 34, 31, 35, 36, 37	efif1olem4 26874	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝐷–1-1-onto→(◡abs “ {1}))
39		f1ocnv 6838	. . . . . . . . . . 11 ⊢ (𝐹:𝐷–1-1-onto→(◡abs “ {1}) → ◡𝐹:(◡abs “ {1})–1-1-onto→𝐷)
40		f1of 6825	. . . . . . . . . . 11 ⊢ (◡𝐹:(◡abs “ {1})–1-1-onto→𝐷 → ◡𝐹:(◡abs “ {1})⟶𝐷)
41	38, 39, 40	3syl 19	. . . . . . . . . 10 ⊢ (𝜑 → ◡𝐹:(◡abs “ {1})⟶𝐷)
42	41	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ◡𝐹:(◡abs “ {1})⟶𝐷)
43	20	abscld 15607	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (abs‘𝑥) ∈ ℝ)
44	43	recnd 11338	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (abs‘𝑥) ∈ ℂ)
45	20, 21	absne0d 15618	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (abs‘𝑥) ≠ 0)
46	20, 44, 45	divcld 12094	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑥 / (abs‘𝑥)) ∈ ℂ)
47	20, 44, 45	absdivd 15626	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (abs‘(𝑥 / (abs‘𝑥))) = ((abs‘𝑥) / (abs‘(abs‘𝑥))))
48		absidm 15492	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (abs‘(abs‘𝑥)) = (abs‘𝑥))
49	20, 48	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (abs‘(abs‘𝑥)) = (abs‘𝑥))
50	49	oveq2d 7437	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((abs‘𝑥) / (abs‘(abs‘𝑥))) = ((abs‘𝑥) / (abs‘𝑥)))
51	44, 45	dividd 12092	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((abs‘𝑥) / (abs‘𝑥)) = 1)
52	47, 50, 51	3eqtrd 2800	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (abs‘(𝑥 / (abs‘𝑥))) = 1)
53		absf 15506	. . . . . . . . . . 11 ⊢ abs:ℂ⟶ℝ
54		ffn 6710	. . . . . . . . . . 11 ⊢ (abs:ℂ⟶ℝ → abs Fn ℂ)
55		fniniseg 7060	. . . . . . . . . . 11 ⊢ (abs Fn ℂ → ((𝑥 / (abs‘𝑥)) ∈ (◡abs “ {1}) ↔ ((𝑥 / (abs‘𝑥)) ∈ ℂ ∧ (abs‘(𝑥 / (abs‘𝑥))) = 1)))
56	53, 54, 55	mp2b 10	. . . . . . . . . 10 ⊢ ((𝑥 / (abs‘𝑥)) ∈ (◡abs “ {1}) ↔ ((𝑥 / (abs‘𝑥)) ∈ ℂ ∧ (abs‘(𝑥 / (abs‘𝑥))) = 1))
57	46, 52, 56	sylanbrc 595	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑥 / (abs‘𝑥)) ∈ (◡abs “ {1}))
58	42, 57	ffvelcdmd 7086	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (◡𝐹‘(𝑥 / (abs‘𝑥))) ∈ 𝐷)
59	32, 58	sseldd 3930	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (◡𝐹‘(𝑥 / (abs‘𝑥))) ∈ ℝ)
60	59	recnd 11338	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (◡𝐹‘(𝑥 / (abs‘𝑥))) ∈ ℂ)
61		mulcl 11285	. . . . . 6 ⊢ ((i ∈ ℂ ∧ (◡𝐹‘(𝑥 / (abs‘𝑥))) ∈ ℂ) → (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))) ∈ ℂ)
62	30, 60, 61	sylancr 599	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))) ∈ ℂ)
63	29, 62	addcld 11329	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ∈ ℂ)
64	28, 59	crimd 15400	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (ℑ‘((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))) = (◡𝐹‘(𝑥 / (abs‘𝑥))))
65	64, 58	eqeltrd 2861	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (ℑ‘((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))) ∈ 𝐷)
66		ffn 6710	. . . . 5 ⊢ (ℑ:ℂ⟶ℝ → ℑ Fn ℂ)
67		elpreima 7058	. . . . 5 ⊢ (ℑ Fn ℂ → (((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ∈ (◡ℑ “ 𝐷) ↔ (((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ∈ ℂ ∧ (ℑ‘((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))) ∈ 𝐷)))
68	3, 66, 67	mp2b 10	. . . 4 ⊢ (((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ∈ (◡ℑ “ 𝐷) ↔ (((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ∈ ℂ ∧ (ℑ‘((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))) ∈ 𝐷))
69	63, 65, 68	sylanbrc 595	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ∈ (◡ℑ “ 𝐷))
70	69, 2	eleqtrrdi 2872	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ∈ 𝑆)
71		efadd 16261	. . . . . . 7 ⊢ (((◡(exp ↾ ℝ)‘(abs‘𝑥)) ∈ ℂ ∧ (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))) ∈ ℂ) → (exp‘((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))) = ((exp‘(◡(exp ↾ ℝ)‘(abs‘𝑥))) · (exp‘(i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))))
72	29, 62, 71	syl2anc 596	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (exp‘((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))) = ((exp‘(◡(exp ↾ ℝ)‘(abs‘𝑥))) · (exp‘(i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))))
73	28	fvresd 6906	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((exp ↾ ℝ)‘(◡(exp ↾ ℝ)‘(abs‘𝑥))) = (exp‘(◡(exp ↾ ℝ)‘(abs‘𝑥))))
74		f1ocnvfv2 7286	. . . . . . . . 9 ⊢ (((exp ↾ ℝ):ℝ–1-1-onto→ℝ+ ∧ (abs‘𝑥) ∈ ℝ+) → ((exp ↾ ℝ)‘(◡(exp ↾ ℝ)‘(abs‘𝑥))) = (abs‘𝑥))
75	23, 22, 74	sylancr 599	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((exp ↾ ℝ)‘(◡(exp ↾ ℝ)‘(abs‘𝑥))) = (abs‘𝑥))
76	73, 75	eqtr3d 2798	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (exp‘(◡(exp ↾ ℝ)‘(abs‘𝑥))) = (abs‘𝑥))
77		oveq2 7429	. . . . . . . . . . 11 ⊢ (𝑧 = (◡𝐹‘(𝑥 / (abs‘𝑥))) → (i · 𝑧) = (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))
78	77	fveq2d 6890	. . . . . . . . . 10 ⊢ (𝑧 = (◡𝐹‘(𝑥 / (abs‘𝑥))) → (exp‘(i · 𝑧)) = (exp‘(i · (◡𝐹‘(𝑥 / (abs‘𝑥))))))
79		oveq2 7429	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑧 → (i · 𝑤) = (i · 𝑧))
80	79	fveq2d 6890	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑧 → (exp‘(i · 𝑤)) = (exp‘(i · 𝑧)))
81	80	cbvmptv 5209	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝐷 ↦ (exp‘(i · 𝑤))) = (𝑧 ∈ 𝐷 ↦ (exp‘(i · 𝑧)))
82	33, 81	eqtri 2784	. . . . . . . . . 10 ⊢ 𝐹 = (𝑧 ∈ 𝐷 ↦ (exp‘(i · 𝑧)))
83		fvex 6899	. . . . . . . . . 10 ⊢ (exp‘(i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ∈ V
84	78, 82, 83	fvmpt 6994	. . . . . . . . 9 ⊢ ((◡𝐹‘(𝑥 / (abs‘𝑥))) ∈ 𝐷 → (𝐹‘(◡𝐹‘(𝑥 / (abs‘𝑥)))) = (exp‘(i · (◡𝐹‘(𝑥 / (abs‘𝑥))))))
85	58, 84	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝐹‘(◡𝐹‘(𝑥 / (abs‘𝑥)))) = (exp‘(i · (◡𝐹‘(𝑥 / (abs‘𝑥))))))
86	38	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝐹:𝐷–1-1-onto→(◡abs “ {1}))
87		f1ocnvfv2 7286	. . . . . . . . 9 ⊢ ((𝐹:𝐷–1-1-onto→(◡abs “ {1}) ∧ (𝑥 / (abs‘𝑥)) ∈ (◡abs “ {1})) → (𝐹‘(◡𝐹‘(𝑥 / (abs‘𝑥)))) = (𝑥 / (abs‘𝑥)))
88	86, 57, 87	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝐹‘(◡𝐹‘(𝑥 / (abs‘𝑥)))) = (𝑥 / (abs‘𝑥)))
89	85, 88	eqtr3d 2798	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (exp‘(i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) = (𝑥 / (abs‘𝑥)))
90	76, 89	oveq12d 7439	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((exp‘(◡(exp ↾ ℝ)‘(abs‘𝑥))) · (exp‘(i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))) = ((abs‘𝑥) · (𝑥 / (abs‘𝑥))))
91	20, 44, 45	divcan2d 12096	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((abs‘𝑥) · (𝑥 / (abs‘𝑥))) = 𝑥)
92	72, 90, 91	3eqtrrd 2801	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑥 = (exp‘((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))))
93	92	adantrl 729	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ (ℂ ∖ {0}))) → 𝑥 = (exp‘((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))))
94		fveq2 6886	. . . . 5 ⊢ (𝑦 = ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) → (exp‘𝑦) = (exp‘((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))))
95	94	eqeq2d 2772	. . . 4 ⊢ (𝑦 = ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) → (𝑥 = (exp‘𝑦) ↔ 𝑥 = (exp‘((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))))))
96	93, 95	syl5ibrcom 250	. . 3 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ (ℂ ∖ {0}))) → (𝑦 = ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) → 𝑥 = (exp‘𝑦)))
97	14	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ ℂ)
98	97	replimd 15365	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑦 = ((ℜ‘𝑦) + (i · (ℑ‘𝑦))))
99		absef 16366	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℂ → (abs‘(exp‘𝑦)) = (exp‘(ℜ‘𝑦)))
100	97, 99	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (abs‘(exp‘𝑦)) = (exp‘(ℜ‘𝑦)))
101	97	recld 15362	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (ℜ‘𝑦) ∈ ℝ)
102	101	fvresd 6906	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ((exp ↾ ℝ)‘(ℜ‘𝑦)) = (exp‘(ℜ‘𝑦)))
103	100, 102	eqtr4d 2799	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (abs‘(exp‘𝑦)) = ((exp ↾ ℝ)‘(ℜ‘𝑦)))
104	103	fveq2d 6890	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (◡(exp ↾ ℝ)‘(abs‘(exp‘𝑦))) = (◡(exp ↾ ℝ)‘((exp ↾ ℝ)‘(ℜ‘𝑦))))
105		f1ocnvfv1 7285	. . . . . . . . 9 ⊢ (((exp ↾ ℝ):ℝ–1-1-onto→ℝ+ ∧ (ℜ‘𝑦) ∈ ℝ) → (◡(exp ↾ ℝ)‘((exp ↾ ℝ)‘(ℜ‘𝑦))) = (ℜ‘𝑦))
106	23, 101, 105	sylancr 599	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (◡(exp ↾ ℝ)‘((exp ↾ ℝ)‘(ℜ‘𝑦))) = (ℜ‘𝑦))
107	104, 106	eqtrd 2796	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (◡(exp ↾ ℝ)‘(abs‘(exp‘𝑦))) = (ℜ‘𝑦))
108	97	imcld 15363	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (ℑ‘𝑦) ∈ ℝ)
109	108	recnd 11338	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (ℑ‘𝑦) ∈ ℂ)
110		mulcl 11285	. . . . . . . . . . . . . 14 ⊢ ((i ∈ ℂ ∧ (ℑ‘𝑦) ∈ ℂ) → (i · (ℑ‘𝑦)) ∈ ℂ)
111	30, 109, 110	sylancr 599	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (i · (ℑ‘𝑦)) ∈ ℂ)
112		efcl 16249	. . . . . . . . . . . . 13 ⊢ ((i · (ℑ‘𝑦)) ∈ ℂ → (exp‘(i · (ℑ‘𝑦))) ∈ ℂ)
113	111, 112	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (exp‘(i · (ℑ‘𝑦))) ∈ ℂ)
114	101	recnd 11338	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (ℜ‘𝑦) ∈ ℂ)
115		efcl 16249	. . . . . . . . . . . . 13 ⊢ ((ℜ‘𝑦) ∈ ℂ → (exp‘(ℜ‘𝑦)) ∈ ℂ)
116	114, 115	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (exp‘(ℜ‘𝑦)) ∈ ℂ)
117		efne0 16265	. . . . . . . . . . . . 13 ⊢ ((ℜ‘𝑦) ∈ ℂ → (exp‘(ℜ‘𝑦)) ≠ 0)
118	114, 117	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (exp‘(ℜ‘𝑦)) ≠ 0)
119	113, 116, 118	divcan3d 12099	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (((exp‘(ℜ‘𝑦)) · (exp‘(i · (ℑ‘𝑦)))) / (exp‘(ℜ‘𝑦))) = (exp‘(i · (ℑ‘𝑦))))
120	98	fveq2d 6890	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (exp‘𝑦) = (exp‘((ℜ‘𝑦) + (i · (ℑ‘𝑦)))))
121		efadd 16261	. . . . . . . . . . . . . 14 ⊢ (((ℜ‘𝑦) ∈ ℂ ∧ (i · (ℑ‘𝑦)) ∈ ℂ) → (exp‘((ℜ‘𝑦) + (i · (ℑ‘𝑦)))) = ((exp‘(ℜ‘𝑦)) · (exp‘(i · (ℑ‘𝑦)))))
122	114, 111, 121	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (exp‘((ℜ‘𝑦) + (i · (ℑ‘𝑦)))) = ((exp‘(ℜ‘𝑦)) · (exp‘(i · (ℑ‘𝑦)))))
123	120, 122	eqtrd 2796	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (exp‘𝑦) = ((exp‘(ℜ‘𝑦)) · (exp‘(i · (ℑ‘𝑦)))))
124	123, 100	oveq12d 7439	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ((exp‘𝑦) / (abs‘(exp‘𝑦))) = (((exp‘(ℜ‘𝑦)) · (exp‘(i · (ℑ‘𝑦)))) / (exp‘(ℜ‘𝑦))))
125		elpreima 7058	. . . . . . . . . . . . . . . 16 ⊢ (ℑ Fn ℂ → (𝑦 ∈ (◡ℑ “ 𝐷) ↔ (𝑦 ∈ ℂ ∧ (ℑ‘𝑦) ∈ 𝐷)))
126	3, 66, 125	mp2b 10	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (◡ℑ “ 𝐷) ↔ (𝑦 ∈ ℂ ∧ (ℑ‘𝑦) ∈ 𝐷))
127	126	simprbi 503	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (◡ℑ “ 𝐷) → (ℑ‘𝑦) ∈ 𝐷)
128	127, 2	eleq2s 2879	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝑆 → (ℑ‘𝑦) ∈ 𝐷)
129	128	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (ℑ‘𝑦) ∈ 𝐷)
130		oveq2 7429	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (ℑ‘𝑦) → (i · 𝑤) = (i · (ℑ‘𝑦)))
131	130	fveq2d 6890	. . . . . . . . . . . . 13 ⊢ (𝑤 = (ℑ‘𝑦) → (exp‘(i · 𝑤)) = (exp‘(i · (ℑ‘𝑦))))
132		fvex 6899	. . . . . . . . . . . . 13 ⊢ (exp‘(i · (ℑ‘𝑦))) ∈ V
133	131, 33, 132	fvmpt 6994	. . . . . . . . . . . 12 ⊢ ((ℑ‘𝑦) ∈ 𝐷 → (𝐹‘(ℑ‘𝑦)) = (exp‘(i · (ℑ‘𝑦))))
134	129, 133	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝐹‘(ℑ‘𝑦)) = (exp‘(i · (ℑ‘𝑦))))
135	119, 124, 134	3eqtr4d 2806	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ((exp‘𝑦) / (abs‘(exp‘𝑦))) = (𝐹‘(ℑ‘𝑦)))
136	135	fveq2d 6890	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦)))) = (◡𝐹‘(𝐹‘(ℑ‘𝑦))))
137		f1ocnvfv1 7285	. . . . . . . . . 10 ⊢ ((𝐹:𝐷–1-1-onto→(◡abs “ {1}) ∧ (ℑ‘𝑦) ∈ 𝐷) → (◡𝐹‘(𝐹‘(ℑ‘𝑦))) = (ℑ‘𝑦))
138	38, 128, 137	syl2an 608	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (◡𝐹‘(𝐹‘(ℑ‘𝑦))) = (ℑ‘𝑦))
139	136, 138	eqtrd 2796	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦)))) = (ℑ‘𝑦))
140	139	oveq2d 7437	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (i · (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦))))) = (i · (ℑ‘𝑦)))
141	107, 140	oveq12d 7439	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ((◡(exp ↾ ℝ)‘(abs‘(exp‘𝑦))) + (i · (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦)))))) = ((ℜ‘𝑦) + (i · (ℑ‘𝑦))))
142	98, 141	eqtr4d 2799	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑦 = ((◡(exp ↾ ℝ)‘(abs‘(exp‘𝑦))) + (i · (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦)))))))
143		fveq2 6886	. . . . . . . 8 ⊢ (𝑥 = (exp‘𝑦) → (abs‘𝑥) = (abs‘(exp‘𝑦)))
144	143	fveq2d 6890	. . . . . . 7 ⊢ (𝑥 = (exp‘𝑦) → (◡(exp ↾ ℝ)‘(abs‘𝑥)) = (◡(exp ↾ ℝ)‘(abs‘(exp‘𝑦))))
145		id 23	. . . . . . . . . 10 ⊢ (𝑥 = (exp‘𝑦) → 𝑥 = (exp‘𝑦))
146	145, 143	oveq12d 7439	. . . . . . . . 9 ⊢ (𝑥 = (exp‘𝑦) → (𝑥 / (abs‘𝑥)) = ((exp‘𝑦) / (abs‘(exp‘𝑦))))
147	146	fveq2d 6890	. . . . . . . 8 ⊢ (𝑥 = (exp‘𝑦) → (◡𝐹‘(𝑥 / (abs‘𝑥))) = (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦)))))
148	147	oveq2d 7437	. . . . . . 7 ⊢ (𝑥 = (exp‘𝑦) → (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))) = (i · (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦))))))
149	144, 148	oveq12d 7439	. . . . . 6 ⊢ (𝑥 = (exp‘𝑦) → ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) = ((◡(exp ↾ ℝ)‘(abs‘(exp‘𝑦))) + (i · (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦)))))))
150	149	eqeq2d 2772	. . . . 5 ⊢ (𝑥 = (exp‘𝑦) → (𝑦 = ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ↔ 𝑦 = ((◡(exp ↾ ℝ)‘(abs‘(exp‘𝑦))) + (i · (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦))))))))
151	142, 150	syl5ibrcom 250	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝑥 = (exp‘𝑦) → 𝑦 = ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))))
152	151	adantrr 730	. . 3 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ (ℂ ∖ {0}))) → (𝑥 = (exp‘𝑦) → 𝑦 = ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))))
153	96, 152	impbid 215	. 2 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ (ℂ ∖ {0}))) → (𝑦 = ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ↔ 𝑥 = (exp‘𝑦)))
154	13, 17, 70, 153	f1o2d 7676	1 ⊢ (𝜑 → (exp ↾ 𝑆):𝑆–1-1-onto→(ℂ ∖ {0}))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ≠ wne 2956  ∃wrex 3087   ∖ cdif 3896   ⊆ wss 3914  {csn 4584   class class class wbr 5103   ↦ cmpt 5186  ^◡ccnv 5650  dom cdm 5651   ↾ cres 5653   “ cima 5654   Fn wfn 6534  ⟶wf 6535  –1-1-onto→wf1o 6538  ‘cfv 6539  (class class class)co 7421  ℂcc 11199  ℝcr 11200  0cc0 11201  1c1 11202  ici 11203   + caddc 11204   · cmul 11206   < clt 11344   − cmin 11542   -cneg 11543   / cdiv 11974  2c2 12398  ℤcz 12694  ℝ⁺crp 13121  [,]cicc 13480  ℜcre 15265  ℑcim 15266  abscabs 15402  expce 16228  sincsin 16230  πcpi 16233

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7752  ax-inf2 9643  ax-cnex 11257  ax-resscn 11258  ax-1cn 11259  ax-icn 11260  ax-addcl 11261  ax-addrcl 11262  ax-mulcl 11263  ax-mulrcl 11264  ax-mulcom 11265  ax-addass 11266  ax-mulass 11267  ax-distr 11268  ax-i2m1 11269  ax-1ne0 11270  ax-1rid 11271  ax-rnegex 11272  ax-rrecex 11273  ax-cnre 11274  ax-pre-lttri 11275  ax-pre-lttrn 11276  ax-pre-ltadd 11277  ax-pre-mulgt0 11278  ax-pre-sup 11279  ax-addf 11280

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3900  df-un 3902  df-in 3904  df-ss 3915  df-pss 4035  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6305  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6495  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-isom 6548  df-riota 7378  df-ov 7424  df-oprab 7425  df-mpo 7426  df-of 7694  df-om 7879  df-1st 8002  df-2nd 8003  df-supp 8179  df-frecs 8300  df-wrecs 8331  df-recs 8380  df-rdg 8419  df-1o 8477  df-2o 8478  df-er 8718  df-map 8850  df-pm 8851  df-ixp 8927  df-en 8975  df-dom 8976  df-sdom 8977  df-fin 8978  df-fsupp 9355  df-fi 9404  df-sup 9435  df-inf 9436  df-oi 9505  df-card 10021  df-pnf 11346  df-mnf 11347  df-xr 11348  df-ltxr 11349  df-le 11350  df-sub 11544  df-neg 11545  df-div 11975  df-nn 12337  df-2 12406  df-3 12407  df-4 12408  df-5 12409  df-6 12410  df-7 12411  df-8 12412  df-9 12413  df-n0 12608  df-z 12695  df-dec 12816  df-uz 12967  df-q 13077  df-rp 13122  df-xneg 13242  df-xadd 13243  df-xmul 13244  df-ioo 13481  df-ioc 13482  df-ico 13483  df-icc 13484  df-fz 13641  df-fzo 13790  df-fl 13933  df-mod 14011  df-seq 14146  df-exp 14206  df-fac 14419  df-bc 14448  df-hash 14476  df-shft 15221  df-cj 15267  df-re 15268  df-im 15269  df-sqrt 15403  df-abs 15404  df-limsup 15639  df-clim 15656  df-rlim 15657  df-sum 15855  df-ef 16234  df-sin 16236  df-cos 16237  df-pi 16239  df-struct 17326  df-sets 17343  df-slot 17361  df-ndx 17373  df-base 17389  df-ress 17410  df-plusg 17442  df-mulr 17443  df-starv 17444  df-sca 17445  df-vsca 17446  df-ip 17447  df-tset 17448  df-ple 17449  df-ds 17451  df-unif 17452  df-hom 17453  df-cco 17454  df-rest 17594  df-topn 17595  df-0g 17613  df-gsum 17614  df-topgen 17615  df-pt 17616  df-prds 17619  df-xrs 17675  df-qtop 17680  df-imas 17681  df-xps 17683  df-mre 17757  df-mrc 17758  df-acs 17760  df-mgm 18817  df-sgrp 18909  df-mnd 18925  df-submnd 18980  df-mulg 19279  df-cntz 19532  df-cmn 19997  df-psmet 21671  df-xmet 21672  df-met 21673  df-bl 21674  df-mopn 21675  df-fbas 21676  df-fg 21677  df-cnfld 21680  df-top 23213  df-topon 23230  df-topsp 23252  df-bases 23265  df-cld 23338  df-ntr 23339  df-cls 23340  df-nei 23417  df-lp 23455  df-perf 23456  df-cn 23546  df-cnp 23547  df-haus 23634  df-tx 23882  df-hmeo 24075  df-fil 24166  df-fm 24258  df-flim 24259  df-flf 24260  df-xms 24640  df-ms 24641  df-tms 24642  df-cncf 25200  df-limc 26187  df-dv 26188

This theorem is used by:  eff1o  26878