MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eff1olem Structured version   Visualization version   GIF version

Theorem eff1olem 24589
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
StepHypRef Expression
1 cnvimass 5669 . . . 4 (ℑ “ 𝐷) ⊆ dom ℑ
2 eff1olem.2 . . . 4 𝑆 = (ℑ “ 𝐷)
3 imf 14141 . . . . . 6 ℑ:ℂ⟶ℝ
43fdmi 6235 . . . . 5 dom ℑ = ℂ
54eqcomi 2774 . . . 4 ℂ = dom ℑ
61, 2, 53sstr4i 3806 . . 3 𝑆 ⊆ ℂ
7 eff2 15114 . . . . . . 7 exp:ℂ⟶(ℂ ∖ {0})
87a1i 11 . . . . . 6 (𝑆 ⊆ ℂ → exp:ℂ⟶(ℂ ∖ {0}))
98feqmptd 6440 . . . . 5 (𝑆 ⊆ ℂ → exp = (𝑦 ∈ ℂ ↦ (exp‘𝑦)))
109reseq1d 5566 . . . 4 (𝑆 ⊆ ℂ → (exp ↾ 𝑆) = ((𝑦 ∈ ℂ ↦ (exp‘𝑦)) ↾ 𝑆))
11 resmpt 5628 . . . 4 (𝑆 ⊆ ℂ → ((𝑦 ∈ ℂ ↦ (exp‘𝑦)) ↾ 𝑆) = (𝑦𝑆 ↦ (exp‘𝑦)))
1210, 11eqtrd 2799 . . 3 (𝑆 ⊆ ℂ → (exp ↾ 𝑆) = (𝑦𝑆 ↦ (exp‘𝑦)))
136, 12ax-mp 5 . 2 (exp ↾ 𝑆) = (𝑦𝑆 ↦ (exp‘𝑦))
146sseli 3759 . . . 4 (𝑦𝑆𝑦 ∈ ℂ)
157ffvelrni 6550 . . . 4 (𝑦 ∈ ℂ → (exp‘𝑦) ∈ (ℂ ∖ {0}))
1614, 15syl 17 . . 3 (𝑦𝑆 → (exp‘𝑦) ∈ (ℂ ∖ {0}))
1716adantl 473 . 2 ((𝜑𝑦𝑆) → (exp‘𝑦) ∈ (ℂ ∖ {0}))
18 simpr 477 . . . . . . . . . 10 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → 𝑥 ∈ (ℂ ∖ {0}))
19 eldifsn 4474 . . . . . . . . . 10 (𝑥 ∈ (ℂ ∖ {0}) ↔ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
2018, 19sylib 209 . . . . . . . . 9 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
2120simpld 488 . . . . . . . 8 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → 𝑥 ∈ ℂ)
2220simprd 489 . . . . . . . 8 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → 𝑥 ≠ 0)
2321, 22absrpcld 14475 . . . . . . 7 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (abs‘𝑥) ∈ ℝ+)
24 reeff1o 24495 . . . . . . . . 9 (exp ↾ ℝ):ℝ–1-1-onto→ℝ+
25 f1ocnv 6334 . . . . . . . . 9 ((exp ↾ ℝ):ℝ–1-1-onto→ℝ+(exp ↾ ℝ):ℝ+1-1-onto→ℝ)
26 f1of 6322 . . . . . . . . 9 ((exp ↾ ℝ):ℝ+1-1-onto→ℝ → (exp ↾ ℝ):ℝ+⟶ℝ)
2724, 25, 26mp2b 10 . . . . . . . 8 (exp ↾ ℝ):ℝ+⟶ℝ
2827ffvelrni 6550 . . . . . . 7 ((abs‘𝑥) ∈ ℝ+ → ((exp ↾ ℝ)‘(abs‘𝑥)) ∈ ℝ)
2923, 28syl 17 . . . . . 6 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → ((exp ↾ ℝ)‘(abs‘𝑥)) ∈ ℝ)
3029recnd 10324 . . . . 5 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → ((exp ↾ ℝ)‘(abs‘𝑥)) ∈ ℂ)
31 ax-icn 10250 . . . . . 6 i ∈ ℂ
32 eff1olem.3 . . . . . . . . 9 (𝜑𝐷 ⊆ ℝ)
3332adantr 472 . . . . . . . 8 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → 𝐷 ⊆ ℝ)
34 eff1olem.1 . . . . . . . . . . . 12 𝐹 = (𝑤𝐷 ↦ (exp‘(i · 𝑤)))
35 eqid 2765 . . . . . . . . . . . 12 (abs “ {1}) = (abs “ {1})
36 eff1olem.4 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐷𝑦𝐷)) → (abs‘(𝑥𝑦)) < (2 · π))
37 eff1olem.5 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ ℝ) → ∃𝑦𝐷 ((𝑧𝑦) / (2 · π)) ∈ ℤ)
38 eqid 2765 . . . . . . . . . . . 12 (sin ↾ (-(π / 2)[,](π / 2))) = (sin ↾ (-(π / 2)[,](π / 2)))
3934, 35, 32, 36, 37, 38efif1olem4 24586 . . . . . . . . . . 11 (𝜑𝐹:𝐷1-1-onto→(abs “ {1}))
40 f1ocnv 6334 . . . . . . . . . . 11 (𝐹:𝐷1-1-onto→(abs “ {1}) → 𝐹:(abs “ {1})–1-1-onto𝐷)
41 f1of 6322 . . . . . . . . . . 11 (𝐹:(abs “ {1})–1-1-onto𝐷𝐹:(abs “ {1})⟶𝐷)
4239, 40, 413syl 18 . . . . . . . . . 10 (𝜑𝐹:(abs “ {1})⟶𝐷)
4342adantr 472 . . . . . . . . 9 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → 𝐹:(abs “ {1})⟶𝐷)
4421abscld 14463 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (abs‘𝑥) ∈ ℝ)
4544recnd 10324 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (abs‘𝑥) ∈ ℂ)
4621, 22absne0d 14474 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (abs‘𝑥) ≠ 0)
4721, 45, 46divcld 11057 . . . . . . . . . 10 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (𝑥 / (abs‘𝑥)) ∈ ℂ)
4821, 45, 46absdivd 14482 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (abs‘(𝑥 / (abs‘𝑥))) = ((abs‘𝑥) / (abs‘(abs‘𝑥))))
49 absidm 14351 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → (abs‘(abs‘𝑥)) = (abs‘𝑥))
5021, 49syl 17 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (abs‘(abs‘𝑥)) = (abs‘𝑥))
5150oveq2d 6860 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → ((abs‘𝑥) / (abs‘(abs‘𝑥))) = ((abs‘𝑥) / (abs‘𝑥)))
5245, 46dividd 11055 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → ((abs‘𝑥) / (abs‘𝑥)) = 1)
5348, 51, 523eqtrd 2803 . . . . . . . . . 10 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (abs‘(𝑥 / (abs‘𝑥))) = 1)
54 absf 14365 . . . . . . . . . . 11 abs:ℂ⟶ℝ
55 ffn 6225 . . . . . . . . . . 11 (abs:ℂ⟶ℝ → abs Fn ℂ)
56 fniniseg 6530 . . . . . . . . . . 11 (abs Fn ℂ → ((𝑥 / (abs‘𝑥)) ∈ (abs “ {1}) ↔ ((𝑥 / (abs‘𝑥)) ∈ ℂ ∧ (abs‘(𝑥 / (abs‘𝑥))) = 1)))
5754, 55, 56mp2b 10 . . . . . . . . . 10 ((𝑥 / (abs‘𝑥)) ∈ (abs “ {1}) ↔ ((𝑥 / (abs‘𝑥)) ∈ ℂ ∧ (abs‘(𝑥 / (abs‘𝑥))) = 1))
5847, 53, 57sylanbrc 578 . . . . . . . . 9 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (𝑥 / (abs‘𝑥)) ∈ (abs “ {1}))
5943, 58ffvelrnd 6552 . . . . . . . 8 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (𝐹‘(𝑥 / (abs‘𝑥))) ∈ 𝐷)
6033, 59sseldd 3764 . . . . . . 7 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (𝐹‘(𝑥 / (abs‘𝑥))) ∈ ℝ)
6160recnd 10324 . . . . . 6 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (𝐹‘(𝑥 / (abs‘𝑥))) ∈ ℂ)
62 mulcl 10275 . . . . . 6 ((i ∈ ℂ ∧ (𝐹‘(𝑥 / (abs‘𝑥))) ∈ ℂ) → (i · (𝐹‘(𝑥 / (abs‘𝑥)))) ∈ ℂ)
6331, 61, 62sylancr 581 . . . . 5 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (i · (𝐹‘(𝑥 / (abs‘𝑥)))) ∈ ℂ)
6430, 63addcld 10315 . . . 4 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (((exp ↾ ℝ)‘(abs‘𝑥)) + (i · (𝐹‘(𝑥 / (abs‘𝑥))))) ∈ ℂ)
6529, 60crimd 14260 . . . . 5 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (ℑ‘(((exp ↾ ℝ)‘(abs‘𝑥)) + (i · (𝐹‘(𝑥 / (abs‘𝑥)))))) = (𝐹‘(𝑥 / (abs‘𝑥))))
6665, 59eqeltrd 2844 . . . 4 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (ℑ‘(((exp ↾ ℝ)‘(abs‘𝑥)) + (i · (𝐹‘(𝑥 / (abs‘𝑥)))))) ∈ 𝐷)
67 ffn 6225 . . . . 5 (ℑ:ℂ⟶ℝ → ℑ Fn ℂ)
68 elpreima 6529 . . . . 5 (ℑ Fn ℂ → ((((exp ↾ ℝ)‘(abs‘𝑥)) + (i · (𝐹‘(𝑥 / (abs‘𝑥))))) ∈ (ℑ “ 𝐷) ↔ ((((exp ↾ ℝ)‘(abs‘𝑥)) + (i · (𝐹‘(𝑥 / (abs‘𝑥))))) ∈ ℂ ∧ (ℑ‘(((exp ↾ ℝ)‘(abs‘𝑥)) + (i · (𝐹‘(𝑥 / (abs‘𝑥)))))) ∈ 𝐷)))
693, 67, 68mp2b 10 . . . 4 ((((exp ↾ ℝ)‘(abs‘𝑥)) + (i · (𝐹‘(𝑥 / (abs‘𝑥))))) ∈ (ℑ “ 𝐷) ↔ ((((exp ↾ ℝ)‘(abs‘𝑥)) + (i · (𝐹‘(𝑥 / (abs‘𝑥))))) ∈ ℂ ∧ (ℑ‘(((exp ↾ ℝ)‘(abs‘𝑥)) + (i · (𝐹‘(𝑥 / (abs‘𝑥)))))) ∈ 𝐷))
7064, 66, 69sylanbrc 578 . . 3 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (((exp ↾ ℝ)‘(abs‘𝑥)) + (i · (𝐹‘(𝑥 / (abs‘𝑥))))) ∈ (ℑ “ 𝐷))
7170, 2syl6eleqr 2855 . 2 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (((exp ↾ ℝ)‘(abs‘𝑥)) + (i · (𝐹‘(𝑥 / (abs‘𝑥))))) ∈ 𝑆)
72 efadd 15109 . . . . . . 7 ((((exp ↾ ℝ)‘(abs‘𝑥)) ∈ ℂ ∧ (i · (𝐹‘(𝑥 / (abs‘𝑥)))) ∈ ℂ) → (exp‘(((exp ↾ ℝ)‘(abs‘𝑥)) + (i · (𝐹‘(𝑥 / (abs‘𝑥)))))) = ((exp‘((exp ↾ ℝ)‘(abs‘𝑥))) · (exp‘(i · (𝐹‘(𝑥 / (abs‘𝑥)))))))
7330, 63, 72syl2anc 579 . . . . . 6 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (exp‘(((exp ↾ ℝ)‘(abs‘𝑥)) + (i · (𝐹‘(𝑥 / (abs‘𝑥)))))) = ((exp‘((exp ↾ ℝ)‘(abs‘𝑥))) · (exp‘(i · (𝐹‘(𝑥 / (abs‘𝑥)))))))
74 fvres 6396 . . . . . . . . 9 (((exp ↾ ℝ)‘(abs‘𝑥)) ∈ ℝ → ((exp ↾ ℝ)‘((exp ↾ ℝ)‘(abs‘𝑥))) = (exp‘((exp ↾ ℝ)‘(abs‘𝑥))))
7529, 74syl 17 . . . . . . . 8 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → ((exp ↾ ℝ)‘((exp ↾ ℝ)‘(abs‘𝑥))) = (exp‘((exp ↾ ℝ)‘(abs‘𝑥))))
76 f1ocnvfv2 6727 . . . . . . . . 9 (((exp ↾ ℝ):ℝ–1-1-onto→ℝ+ ∧ (abs‘𝑥) ∈ ℝ+) → ((exp ↾ ℝ)‘((exp ↾ ℝ)‘(abs‘𝑥))) = (abs‘𝑥))
7724, 23, 76sylancr 581 . . . . . . . 8 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → ((exp ↾ ℝ)‘((exp ↾ ℝ)‘(abs‘𝑥))) = (abs‘𝑥))
7875, 77eqtr3d 2801 . . . . . . 7 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (exp‘((exp ↾ ℝ)‘(abs‘𝑥))) = (abs‘𝑥))
79 oveq2 6852 . . . . . . . . . . 11 (𝑧 = (𝐹‘(𝑥 / (abs‘𝑥))) → (i · 𝑧) = (i · (𝐹‘(𝑥 / (abs‘𝑥)))))
8079fveq2d 6381 . . . . . . . . . 10 (𝑧 = (𝐹‘(𝑥 / (abs‘𝑥))) → (exp‘(i · 𝑧)) = (exp‘(i · (𝐹‘(𝑥 / (abs‘𝑥))))))
81 oveq2 6852 . . . . . . . . . . . . 13 (𝑤 = 𝑧 → (i · 𝑤) = (i · 𝑧))
8281fveq2d 6381 . . . . . . . . . . . 12 (𝑤 = 𝑧 → (exp‘(i · 𝑤)) = (exp‘(i · 𝑧)))
8382cbvmptv 4911 . . . . . . . . . . 11 (𝑤𝐷 ↦ (exp‘(i · 𝑤))) = (𝑧𝐷 ↦ (exp‘(i · 𝑧)))
8434, 83eqtri 2787 . . . . . . . . . 10 𝐹 = (𝑧𝐷 ↦ (exp‘(i · 𝑧)))
85 fvex 6390 . . . . . . . . . 10 (exp‘(i · (𝐹‘(𝑥 / (abs‘𝑥))))) ∈ V
8680, 84, 85fvmpt 6473 . . . . . . . . 9 ((𝐹‘(𝑥 / (abs‘𝑥))) ∈ 𝐷 → (𝐹‘(𝐹‘(𝑥 / (abs‘𝑥)))) = (exp‘(i · (𝐹‘(𝑥 / (abs‘𝑥))))))
8759, 86syl 17 . . . . . . . 8 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (𝐹‘(𝐹‘(𝑥 / (abs‘𝑥)))) = (exp‘(i · (𝐹‘(𝑥 / (abs‘𝑥))))))
8839adantr 472 . . . . . . . . 9 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → 𝐹:𝐷1-1-onto→(abs “ {1}))
89 f1ocnvfv2 6727 . . . . . . . . 9 ((𝐹:𝐷1-1-onto→(abs “ {1}) ∧ (𝑥 / (abs‘𝑥)) ∈ (abs “ {1})) → (𝐹‘(𝐹‘(𝑥 / (abs‘𝑥)))) = (𝑥 / (abs‘𝑥)))
9088, 58, 89syl2anc 579 . . . . . . . 8 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (𝐹‘(𝐹‘(𝑥 / (abs‘𝑥)))) = (𝑥 / (abs‘𝑥)))
9187, 90eqtr3d 2801 . . . . . . 7 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → (exp‘(i · (𝐹‘(𝑥 / (abs‘𝑥))))) = (𝑥 / (abs‘𝑥)))
9278, 91oveq12d 6862 . . . . . 6 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → ((exp‘((exp ↾ ℝ)‘(abs‘𝑥))) · (exp‘(i · (𝐹‘(𝑥 / (abs‘𝑥)))))) = ((abs‘𝑥) · (𝑥 / (abs‘𝑥))))
9321, 45, 46divcan2d 11059 . . . . . 6 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → ((abs‘𝑥) · (𝑥 / (abs‘𝑥))) = 𝑥)
9473, 92, 933eqtrrd 2804 . . . . 5 ((𝜑𝑥 ∈ (ℂ ∖ {0})) → 𝑥 = (exp‘(((exp ↾ ℝ)‘(abs‘𝑥)) + (i · (𝐹‘(𝑥 / (abs‘𝑥)))))))
9594adantrl 707 . . . 4 ((𝜑 ∧ (𝑦𝑆𝑥 ∈ (ℂ ∖ {0}))) → 𝑥 = (exp‘(((exp ↾ ℝ)‘(abs‘𝑥)) + (i · (𝐹‘(𝑥 / (abs‘𝑥)))))))
96 fveq2 6377 . . . . 5 (𝑦 = (((exp ↾ ℝ)‘(abs‘𝑥)) + (i · (𝐹‘(𝑥 / (abs‘𝑥))))) → (exp‘𝑦) = (exp‘(((exp ↾ ℝ)‘(abs‘𝑥)) + (i · (𝐹‘(𝑥 / (abs‘𝑥)))))))
9796eqeq2d 2775 . . . 4 (𝑦 = (((exp ↾ ℝ)‘(abs‘𝑥)) + (i · (𝐹‘(𝑥 / (abs‘𝑥))))) → (𝑥 = (exp‘𝑦) ↔ 𝑥 = (exp‘(((exp ↾ ℝ)‘(abs‘𝑥)) + (i · (𝐹‘(𝑥 / (abs‘𝑥))))))))
9895, 97syl5ibrcom 238 . . 3 ((𝜑 ∧ (𝑦𝑆𝑥 ∈ (ℂ ∖ {0}))) → (𝑦 = (((exp ↾ ℝ)‘(abs‘𝑥)) + (i · (𝐹‘(𝑥 / (abs‘𝑥))))) → 𝑥 = (exp‘𝑦)))
9914adantl 473 . . . . . . 7 ((𝜑𝑦𝑆) → 𝑦 ∈ ℂ)
10099replimd 14225 . . . . . 6 ((𝜑𝑦𝑆) → 𝑦 = ((ℜ‘𝑦) + (i · (ℑ‘𝑦))))
101 absef 15212 . . . . . . . . . . 11 (𝑦 ∈ ℂ → (abs‘(exp‘𝑦)) = (exp‘(ℜ‘𝑦)))
10299, 101syl 17 . . . . . . . . . 10 ((𝜑𝑦𝑆) → (abs‘(exp‘𝑦)) = (exp‘(ℜ‘𝑦)))
10399recld 14222 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → (ℜ‘𝑦) ∈ ℝ)
104 fvres 6396 . . . . . . . . . . 11 ((ℜ‘𝑦) ∈ ℝ → ((exp ↾ ℝ)‘(ℜ‘𝑦)) = (exp‘(ℜ‘𝑦)))
105103, 104syl 17 . . . . . . . . . 10 ((𝜑𝑦𝑆) → ((exp ↾ ℝ)‘(ℜ‘𝑦)) = (exp‘(ℜ‘𝑦)))
106102, 105eqtr4d 2802 . . . . . . . . 9 ((𝜑𝑦𝑆) → (abs‘(exp‘𝑦)) = ((exp ↾ ℝ)‘(ℜ‘𝑦)))
107106fveq2d 6381 . . . . . . . 8 ((𝜑𝑦𝑆) → ((exp ↾ ℝ)‘(abs‘(exp‘𝑦))) = ((exp ↾ ℝ)‘((exp ↾ ℝ)‘(ℜ‘𝑦))))
108 f1ocnvfv1 6726 . . . . . . . . 9 (((exp ↾ ℝ):ℝ–1-1-onto→ℝ+ ∧ (ℜ‘𝑦) ∈ ℝ) → ((exp ↾ ℝ)‘((exp ↾ ℝ)‘(ℜ‘𝑦))) = (ℜ‘𝑦))
10924, 103, 108sylancr 581 . . . . . . . 8 ((𝜑𝑦𝑆) → ((exp ↾ ℝ)‘((exp ↾ ℝ)‘(ℜ‘𝑦))) = (ℜ‘𝑦))
110107, 109eqtrd 2799 . . . . . . 7 ((𝜑𝑦𝑆) → ((exp ↾ ℝ)‘(abs‘(exp‘𝑦))) = (ℜ‘𝑦))
11199imcld 14223 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑆) → (ℑ‘𝑦) ∈ ℝ)
112111recnd 10324 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑆) → (ℑ‘𝑦) ∈ ℂ)
113 mulcl 10275 . . . . . . . . . . . . . 14 ((i ∈ ℂ ∧ (ℑ‘𝑦) ∈ ℂ) → (i · (ℑ‘𝑦)) ∈ ℂ)
11431, 112, 113sylancr 581 . . . . . . . . . . . . 13 ((𝜑𝑦𝑆) → (i · (ℑ‘𝑦)) ∈ ℂ)
115 efcl 15098 . . . . . . . . . . . . 13 ((i · (ℑ‘𝑦)) ∈ ℂ → (exp‘(i · (ℑ‘𝑦))) ∈ ℂ)
116114, 115syl 17 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → (exp‘(i · (ℑ‘𝑦))) ∈ ℂ)
117103recnd 10324 . . . . . . . . . . . . 13 ((𝜑𝑦𝑆) → (ℜ‘𝑦) ∈ ℂ)
118 efcl 15098 . . . . . . . . . . . . 13 ((ℜ‘𝑦) ∈ ℂ → (exp‘(ℜ‘𝑦)) ∈ ℂ)
119117, 118syl 17 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → (exp‘(ℜ‘𝑦)) ∈ ℂ)
120 efne0 15112 . . . . . . . . . . . . 13 ((ℜ‘𝑦) ∈ ℂ → (exp‘(ℜ‘𝑦)) ≠ 0)
121117, 120syl 17 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → (exp‘(ℜ‘𝑦)) ≠ 0)
122116, 119, 121divcan3d 11062 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → (((exp‘(ℜ‘𝑦)) · (exp‘(i · (ℑ‘𝑦)))) / (exp‘(ℜ‘𝑦))) = (exp‘(i · (ℑ‘𝑦))))
123100fveq2d 6381 . . . . . . . . . . . . 13 ((𝜑𝑦𝑆) → (exp‘𝑦) = (exp‘((ℜ‘𝑦) + (i · (ℑ‘𝑦)))))
124 efadd 15109 . . . . . . . . . . . . . 14 (((ℜ‘𝑦) ∈ ℂ ∧ (i · (ℑ‘𝑦)) ∈ ℂ) → (exp‘((ℜ‘𝑦) + (i · (ℑ‘𝑦)))) = ((exp‘(ℜ‘𝑦)) · (exp‘(i · (ℑ‘𝑦)))))
125117, 114, 124syl2anc 579 . . . . . . . . . . . . 13 ((𝜑𝑦𝑆) → (exp‘((ℜ‘𝑦) + (i · (ℑ‘𝑦)))) = ((exp‘(ℜ‘𝑦)) · (exp‘(i · (ℑ‘𝑦)))))
126123, 125eqtrd 2799 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → (exp‘𝑦) = ((exp‘(ℜ‘𝑦)) · (exp‘(i · (ℑ‘𝑦)))))
127126, 102oveq12d 6862 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → ((exp‘𝑦) / (abs‘(exp‘𝑦))) = (((exp‘(ℜ‘𝑦)) · (exp‘(i · (ℑ‘𝑦)))) / (exp‘(ℜ‘𝑦))))
128 elpreima 6529 . . . . . . . . . . . . . . . 16 (ℑ Fn ℂ → (𝑦 ∈ (ℑ “ 𝐷) ↔ (𝑦 ∈ ℂ ∧ (ℑ‘𝑦) ∈ 𝐷)))
1293, 67, 128mp2b 10 . . . . . . . . . . . . . . 15 (𝑦 ∈ (ℑ “ 𝐷) ↔ (𝑦 ∈ ℂ ∧ (ℑ‘𝑦) ∈ 𝐷))
130129simprbi 490 . . . . . . . . . . . . . 14 (𝑦 ∈ (ℑ “ 𝐷) → (ℑ‘𝑦) ∈ 𝐷)
131130, 2eleq2s 2862 . . . . . . . . . . . . 13 (𝑦𝑆 → (ℑ‘𝑦) ∈ 𝐷)
132131adantl 473 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → (ℑ‘𝑦) ∈ 𝐷)
133 oveq2 6852 . . . . . . . . . . . . . 14 (𝑤 = (ℑ‘𝑦) → (i · 𝑤) = (i · (ℑ‘𝑦)))
134133fveq2d 6381 . . . . . . . . . . . . 13 (𝑤 = (ℑ‘𝑦) → (exp‘(i · 𝑤)) = (exp‘(i · (ℑ‘𝑦))))
135 fvex 6390 . . . . . . . . . . . . 13 (exp‘(i · (ℑ‘𝑦))) ∈ V
136134, 34, 135fvmpt 6473 . . . . . . . . . . . 12 ((ℑ‘𝑦) ∈ 𝐷 → (𝐹‘(ℑ‘𝑦)) = (exp‘(i · (ℑ‘𝑦))))
137132, 136syl 17 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → (𝐹‘(ℑ‘𝑦)) = (exp‘(i · (ℑ‘𝑦))))
138122, 127, 1373eqtr4d 2809 . . . . . . . . . 10 ((𝜑𝑦𝑆) → ((exp‘𝑦) / (abs‘(exp‘𝑦))) = (𝐹‘(ℑ‘𝑦)))
139138fveq2d 6381 . . . . . . . . 9 ((𝜑𝑦𝑆) → (𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦)))) = (𝐹‘(𝐹‘(ℑ‘𝑦))))
140 f1ocnvfv1 6726 . . . . . . . . . 10 ((𝐹:𝐷1-1-onto→(abs “ {1}) ∧ (ℑ‘𝑦) ∈ 𝐷) → (𝐹‘(𝐹‘(ℑ‘𝑦))) = (ℑ‘𝑦))
14139, 131, 140syl2an 589 . . . . . . . . 9 ((𝜑𝑦𝑆) → (𝐹‘(𝐹‘(ℑ‘𝑦))) = (ℑ‘𝑦))
142139, 141eqtrd 2799 . . . . . . . 8 ((𝜑𝑦𝑆) → (𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦)))) = (ℑ‘𝑦))
143142oveq2d 6860 . . . . . . 7 ((𝜑𝑦𝑆) → (i · (𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦))))) = (i · (ℑ‘𝑦)))
144110, 143oveq12d 6862 . . . . . 6 ((𝜑𝑦𝑆) → (((exp ↾ ℝ)‘(abs‘(exp‘𝑦))) + (i · (𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦)))))) = ((ℜ‘𝑦) + (i · (ℑ‘𝑦))))
145100, 144eqtr4d 2802 . . . . 5 ((𝜑𝑦𝑆) → 𝑦 = (((exp ↾ ℝ)‘(abs‘(exp‘𝑦))) + (i · (𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦)))))))
146 fveq2 6377 . . . . . . . 8 (𝑥 = (exp‘𝑦) → (abs‘𝑥) = (abs‘(exp‘𝑦)))
147146fveq2d 6381 . . . . . . 7 (𝑥 = (exp‘𝑦) → ((exp ↾ ℝ)‘(abs‘𝑥)) = ((exp ↾ ℝ)‘(abs‘(exp‘𝑦))))
148 id 22 . . . . . . . . . 10 (𝑥 = (exp‘𝑦) → 𝑥 = (exp‘𝑦))
149148, 146oveq12d 6862 . . . . . . . . 9 (𝑥 = (exp‘𝑦) → (𝑥 / (abs‘𝑥)) = ((exp‘𝑦) / (abs‘(exp‘𝑦))))
150149fveq2d 6381 . . . . . . . 8 (𝑥 = (exp‘𝑦) → (𝐹‘(𝑥 / (abs‘𝑥))) = (𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦)))))
151150oveq2d 6860 . . . . . . 7 (𝑥 = (exp‘𝑦) → (i · (𝐹‘(𝑥 / (abs‘𝑥)))) = (i · (𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦))))))
152147, 151oveq12d 6862 . . . . . 6 (𝑥 = (exp‘𝑦) → (((exp ↾ ℝ)‘(abs‘𝑥)) + (i · (𝐹‘(𝑥 / (abs‘𝑥))))) = (((exp ↾ ℝ)‘(abs‘(exp‘𝑦))) + (i · (𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦)))))))
153152eqeq2d 2775 . . . . 5 (𝑥 = (exp‘𝑦) → (𝑦 = (((exp ↾ ℝ)‘(abs‘𝑥)) + (i · (𝐹‘(𝑥 / (abs‘𝑥))))) ↔ 𝑦 = (((exp ↾ ℝ)‘(abs‘(exp‘𝑦))) + (i · (𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦))))))))
154145, 153syl5ibrcom 238 . . . 4 ((𝜑𝑦𝑆) → (𝑥 = (exp‘𝑦) → 𝑦 = (((exp ↾ ℝ)‘(abs‘𝑥)) + (i · (𝐹‘(𝑥 / (abs‘𝑥)))))))
155154adantrr 708 . . 3 ((𝜑 ∧ (𝑦𝑆𝑥 ∈ (ℂ ∖ {0}))) → (𝑥 = (exp‘𝑦) → 𝑦 = (((exp ↾ ℝ)‘(abs‘𝑥)) + (i · (𝐹‘(𝑥 / (abs‘𝑥)))))))
15698, 155impbid 203 . 2 ((𝜑 ∧ (𝑦𝑆𝑥 ∈ (ℂ ∖ {0}))) → (𝑦 = (((exp ↾ ℝ)‘(abs‘𝑥)) + (i · (𝐹‘(𝑥 / (abs‘𝑥))))) ↔ 𝑥 = (exp‘𝑦)))
15713, 17, 71, 156f1o2d 7087 1 (𝜑 → (exp ↾ 𝑆):𝑆1-1-onto→(ℂ ∖ {0}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wne 2937  wrex 3056  cdif 3731  wss 3734  {csn 4336   class class class wbr 4811  cmpt 4890  ccnv 5278  dom cdm 5279  cres 5281  cima 5282   Fn wfn 6065  wf 6066  1-1-ontowf1o 6069  cfv 6070  (class class class)co 6844  cc 10189  cr 10190  0cc0 10191  1c1 10192  ici 10193   + caddc 10194   · cmul 10196   < clt 10330  cmin 10522  -cneg 10523   / cdiv 10940  2c2 11329  cz 11626  +crp 12031  [,]cicc 12383  cre 14125  cim 14126  abscabs 14262  expce 15077  sincsin 15079  πcpi 15082
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7149  ax-inf2 8755  ax-cnex 10247  ax-resscn 10248  ax-1cn 10249  ax-icn 10250  ax-addcl 10251  ax-addrcl 10252  ax-mulcl 10253  ax-mulrcl 10254  ax-mulcom 10255  ax-addass 10256  ax-mulass 10257  ax-distr 10258  ax-i2m1 10259  ax-1ne0 10260  ax-1rid 10261  ax-rnegex 10262  ax-rrecex 10263  ax-cnre 10264  ax-pre-lttri 10265  ax-pre-lttrn 10266  ax-pre-ltadd 10267  ax-pre-mulgt0 10268  ax-pre-sup 10269  ax-addf 10270  ax-mulf 10271
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-iin 4681  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-se 5239  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-isom 6079  df-riota 6805  df-ov 6847  df-oprab 6848  df-mpt2 6849  df-of 7097  df-om 7266  df-1st 7368  df-2nd 7369  df-supp 7500  df-wrecs 7612  df-recs 7674  df-rdg 7712  df-1o 7766  df-2o 7767  df-oadd 7770  df-er 7949  df-map 8064  df-pm 8065  df-ixp 8116  df-en 8163  df-dom 8164  df-sdom 8165  df-fin 8166  df-fsupp 8485  df-fi 8526  df-sup 8557  df-inf 8558  df-oi 8624  df-card 9018  df-cda 9245  df-pnf 10332  df-mnf 10333  df-xr 10334  df-ltxr 10335  df-le 10336  df-sub 10524  df-neg 10525  df-div 10941  df-nn 11277  df-2 11337  df-3 11338  df-4 11339  df-5 11340  df-6 11341  df-7 11342  df-8 11343  df-9 11344  df-n0 11541  df-z 11627  df-dec 11744  df-uz 11890  df-q 11993  df-rp 12032  df-xneg 12149  df-xadd 12150  df-xmul 12151  df-ioo 12384  df-ioc 12385  df-ico 12386  df-icc 12387  df-fz 12537  df-fzo 12677  df-fl 12804  df-mod 12880  df-seq 13012  df-exp 13071  df-fac 13268  df-bc 13297  df-hash 13325  df-shft 14095  df-cj 14127  df-re 14128  df-im 14129  df-sqrt 14263  df-abs 14264  df-limsup 14490  df-clim 14507  df-rlim 14508  df-sum 14705  df-ef 15083  df-sin 15085  df-cos 15086  df-pi 15088  df-struct 16135  df-ndx 16136  df-slot 16137  df-base 16139  df-sets 16140  df-ress 16141  df-plusg 16230  df-mulr 16231  df-starv 16232  df-sca 16233  df-vsca 16234  df-ip 16235  df-tset 16236  df-ple 16237  df-ds 16239  df-unif 16240  df-hom 16241  df-cco 16242  df-rest 16352  df-topn 16353  df-0g 16371  df-gsum 16372  df-topgen 16373  df-pt 16374  df-prds 16377  df-xrs 16431  df-qtop 16436  df-imas 16437  df-xps 16439  df-mre 16515  df-mrc 16516  df-acs 16518  df-mgm 17511  df-sgrp 17553  df-mnd 17564  df-submnd 17605  df-mulg 17811  df-cntz 18016  df-cmn 18464  df-psmet 20014  df-xmet 20015  df-met 20016  df-bl 20017  df-mopn 20018  df-fbas 20019  df-fg 20020  df-cnfld 20023  df-top 20981  df-topon 20998  df-topsp 21020  df-bases 21033  df-cld 21106  df-ntr 21107  df-cls 21108  df-nei 21185  df-lp 21223  df-perf 21224  df-cn 21314  df-cnp 21315  df-haus 21402  df-tx 21648  df-hmeo 21841  df-fil 21932  df-fm 22024  df-flim 22025  df-flf 22026  df-xms 22407  df-ms 22408  df-tms 22409  df-cncf 22963  df-limc 23924  df-dv 23925
This theorem is referenced by:  eff1o  24590
  Copyright terms: Public domain W3C validator