Proof of Theorem eff1olem
Step | Hyp | Ref
| Expression |
1 | | cnvimass 5404 |
. . . 4
⊢ (◡ℑ “ 𝐷) ⊆ dom ℑ |
2 | | eff1olem.2 |
. . . 4
⊢ 𝑆 = (◡ℑ “ 𝐷) |
3 | | imf 13701 |
. . . . . 6
⊢
ℑ:ℂ⟶ℝ |
4 | 3 | fdmi 5965 |
. . . . 5
⊢ dom
ℑ = ℂ |
5 | 4 | eqcomi 2619 |
. . . 4
⊢ ℂ =
dom ℑ |
6 | 1, 2, 5 | 3sstr4i 3607 |
. . 3
⊢ 𝑆 ⊆
ℂ |
7 | | eff2 14668 |
. . . . . . 7
⊢
exp:ℂ⟶(ℂ ∖ {0}) |
8 | 7 | a1i 11 |
. . . . . 6
⊢ (𝑆 ⊆ ℂ →
exp:ℂ⟶(ℂ ∖ {0})) |
9 | 8 | feqmptd 6159 |
. . . . 5
⊢ (𝑆 ⊆ ℂ → exp =
(𝑦 ∈ ℂ ↦
(exp‘𝑦))) |
10 | 9 | reseq1d 5316 |
. . . 4
⊢ (𝑆 ⊆ ℂ → (exp
↾ 𝑆) = ((𝑦 ∈ ℂ ↦
(exp‘𝑦)) ↾
𝑆)) |
11 | | resmpt 5369 |
. . . 4
⊢ (𝑆 ⊆ ℂ → ((𝑦 ∈ ℂ ↦
(exp‘𝑦)) ↾
𝑆) = (𝑦 ∈ 𝑆 ↦ (exp‘𝑦))) |
12 | 10, 11 | eqtrd 2644 |
. . 3
⊢ (𝑆 ⊆ ℂ → (exp
↾ 𝑆) = (𝑦 ∈ 𝑆 ↦ (exp‘𝑦))) |
13 | 6, 12 | ax-mp 5 |
. 2
⊢ (exp
↾ 𝑆) = (𝑦 ∈ 𝑆 ↦ (exp‘𝑦)) |
14 | 6 | sseli 3564 |
. . . 4
⊢ (𝑦 ∈ 𝑆 → 𝑦 ∈ ℂ) |
15 | 7 | ffvelrni 6266 |
. . . 4
⊢ (𝑦 ∈ ℂ →
(exp‘𝑦) ∈
(ℂ ∖ {0})) |
16 | 14, 15 | syl 17 |
. . 3
⊢ (𝑦 ∈ 𝑆 → (exp‘𝑦) ∈ (ℂ ∖
{0})) |
17 | 16 | adantl 481 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (exp‘𝑦) ∈ (ℂ ∖
{0})) |
18 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑥 ∈ (ℂ ∖
{0})) |
19 | | eldifsn 4260 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (ℂ ∖ {0})
↔ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
20 | 18, 19 | sylib 207 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
21 | 20 | simpld 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑥 ∈
ℂ) |
22 | 20 | simprd 478 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑥 ≠ 0) |
23 | 21, 22 | absrpcld 14035 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(abs‘𝑥) ∈
ℝ+) |
24 | | reeff1o 24005 |
. . . . . . . . 9
⊢ (exp
↾ ℝ):ℝ–1-1-onto→ℝ+ |
25 | | f1ocnv 6062 |
. . . . . . . . 9
⊢ ((exp
↾ ℝ):ℝ–1-1-onto→ℝ+ → ◡(exp ↾
ℝ):ℝ+–1-1-onto→ℝ) |
26 | | f1of 6050 |
. . . . . . . . 9
⊢ (◡(exp ↾
ℝ):ℝ+–1-1-onto→ℝ → ◡(exp ↾
ℝ):ℝ+⟶ℝ) |
27 | 24, 25, 26 | mp2b 10 |
. . . . . . . 8
⊢ ◡(exp ↾
ℝ):ℝ+⟶ℝ |
28 | 27 | ffvelrni 6266 |
. . . . . . 7
⊢
((abs‘𝑥)
∈ ℝ+ → (◡(exp ↾ ℝ)‘(abs‘𝑥)) ∈
ℝ) |
29 | 23, 28 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (◡(exp ↾ ℝ)‘(abs‘𝑥)) ∈
ℝ) |
30 | 29 | recnd 9947 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (◡(exp ↾ ℝ)‘(abs‘𝑥)) ∈
ℂ) |
31 | | ax-icn 9874 |
. . . . . 6
⊢ i ∈
ℂ |
32 | | eff1olem.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ⊆ ℝ) |
33 | 32 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝐷 ⊆
ℝ) |
34 | | eff1olem.1 |
. . . . . . . . . . . 12
⊢ 𝐹 = (𝑤 ∈ 𝐷 ↦ (exp‘(i · 𝑤))) |
35 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (◡abs “ {1}) = (◡abs “ {1}) |
36 | | eff1olem.4 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → (abs‘(𝑥 − 𝑦)) < (2 · π)) |
37 | | eff1olem.5 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → ∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈
ℤ) |
38 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (sin
↾ (-(π / 2)[,](π / 2))) = (sin ↾ (-(π / 2)[,](π /
2))) |
39 | 34, 35, 32, 36, 37, 38 | efif1olem4 24095 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐷–1-1-onto→(◡abs
“ {1})) |
40 | | f1ocnv 6062 |
. . . . . . . . . . 11
⊢ (𝐹:𝐷–1-1-onto→(◡abs
“ {1}) → ◡𝐹:(◡abs “ {1})–1-1-onto→𝐷) |
41 | | f1of 6050 |
. . . . . . . . . . 11
⊢ (◡𝐹:(◡abs “ {1})–1-1-onto→𝐷 → ◡𝐹:(◡abs “ {1})⟶𝐷) |
42 | 39, 40, 41 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → ◡𝐹:(◡abs “ {1})⟶𝐷) |
43 | 42 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ◡𝐹:(◡abs “ {1})⟶𝐷) |
44 | 21 | abscld 14023 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(abs‘𝑥) ∈
ℝ) |
45 | 44 | recnd 9947 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(abs‘𝑥) ∈
ℂ) |
46 | 21, 22 | absne0d 14034 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(abs‘𝑥) ≠
0) |
47 | 21, 45, 46 | divcld 10680 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑥 / (abs‘𝑥)) ∈ ℂ) |
48 | 21, 45, 46 | absdivd 14042 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(abs‘(𝑥 /
(abs‘𝑥))) =
((abs‘𝑥) /
(abs‘(abs‘𝑥)))) |
49 | | absidm 13911 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ →
(abs‘(abs‘𝑥)) =
(abs‘𝑥)) |
50 | 21, 49 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(abs‘(abs‘𝑥)) =
(abs‘𝑥)) |
51 | 50 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
((abs‘𝑥) /
(abs‘(abs‘𝑥)))
= ((abs‘𝑥) /
(abs‘𝑥))) |
52 | 45, 46 | dividd 10678 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
((abs‘𝑥) /
(abs‘𝑥)) =
1) |
53 | 48, 51, 52 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(abs‘(𝑥 /
(abs‘𝑥))) =
1) |
54 | | absf 13925 |
. . . . . . . . . . 11
⊢
abs:ℂ⟶ℝ |
55 | | ffn 5958 |
. . . . . . . . . . 11
⊢
(abs:ℂ⟶ℝ → abs Fn ℂ) |
56 | | fniniseg 6246 |
. . . . . . . . . . 11
⊢ (abs Fn
ℂ → ((𝑥 /
(abs‘𝑥)) ∈
(◡abs “ {1}) ↔ ((𝑥 / (abs‘𝑥)) ∈ ℂ ∧ (abs‘(𝑥 / (abs‘𝑥))) = 1))) |
57 | 54, 55, 56 | mp2b 10 |
. . . . . . . . . 10
⊢ ((𝑥 / (abs‘𝑥)) ∈ (◡abs “ {1}) ↔ ((𝑥 / (abs‘𝑥)) ∈ ℂ ∧ (abs‘(𝑥 / (abs‘𝑥))) = 1)) |
58 | 47, 53, 57 | sylanbrc 695 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑥 / (abs‘𝑥)) ∈ (◡abs “ {1})) |
59 | 43, 58 | ffvelrnd 6268 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (◡𝐹‘(𝑥 / (abs‘𝑥))) ∈ 𝐷) |
60 | 33, 59 | sseldd 3569 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (◡𝐹‘(𝑥 / (abs‘𝑥))) ∈ ℝ) |
61 | 60 | recnd 9947 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (◡𝐹‘(𝑥 / (abs‘𝑥))) ∈ ℂ) |
62 | | mulcl 9899 |
. . . . . 6
⊢ ((i
∈ ℂ ∧ (◡𝐹‘(𝑥 / (abs‘𝑥))) ∈ ℂ) → (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))) ∈ ℂ) |
63 | 31, 61, 62 | sylancr 694 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (i
· (◡𝐹‘(𝑥 / (abs‘𝑥)))) ∈ ℂ) |
64 | 30, 63 | addcld 9938 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ∈ ℂ) |
65 | 29, 60 | crimd 13820 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(ℑ‘((◡(exp ↾
ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))) = (◡𝐹‘(𝑥 / (abs‘𝑥)))) |
66 | 65, 59 | eqeltrd 2688 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(ℑ‘((◡(exp ↾
ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))) ∈ 𝐷) |
67 | | ffn 5958 |
. . . . 5
⊢
(ℑ:ℂ⟶ℝ → ℑ Fn
ℂ) |
68 | | elpreima 6245 |
. . . . 5
⊢ (ℑ
Fn ℂ → (((◡(exp ↾
ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ∈ (◡ℑ “ 𝐷) ↔ (((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ∈ ℂ ∧
(ℑ‘((◡(exp ↾
ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))) ∈ 𝐷))) |
69 | 3, 67, 68 | mp2b 10 |
. . . 4
⊢ (((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ∈ (◡ℑ “ 𝐷) ↔ (((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ∈ ℂ ∧
(ℑ‘((◡(exp ↾
ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))) ∈ 𝐷)) |
70 | 64, 66, 69 | sylanbrc 695 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ∈ (◡ℑ “ 𝐷)) |
71 | 70, 2 | syl6eleqr 2699 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ∈ 𝑆) |
72 | | efadd 14663 |
. . . . . . 7
⊢ (((◡(exp ↾ ℝ)‘(abs‘𝑥)) ∈ ℂ ∧ (i
· (◡𝐹‘(𝑥 / (abs‘𝑥)))) ∈ ℂ) →
(exp‘((◡(exp ↾
ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))) = ((exp‘(◡(exp ↾ ℝ)‘(abs‘𝑥))) · (exp‘(i
· (◡𝐹‘(𝑥 / (abs‘𝑥))))))) |
73 | 30, 63, 72 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(exp‘((◡(exp ↾
ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))) = ((exp‘(◡(exp ↾ ℝ)‘(abs‘𝑥))) · (exp‘(i
· (◡𝐹‘(𝑥 / (abs‘𝑥))))))) |
74 | | fvres 6117 |
. . . . . . . . 9
⊢ ((◡(exp ↾ ℝ)‘(abs‘𝑥)) ∈ ℝ → ((exp
↾ ℝ)‘(◡(exp ↾
ℝ)‘(abs‘𝑥))) = (exp‘(◡(exp ↾ ℝ)‘(abs‘𝑥)))) |
75 | 29, 74 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((exp
↾ ℝ)‘(◡(exp ↾
ℝ)‘(abs‘𝑥))) = (exp‘(◡(exp ↾ ℝ)‘(abs‘𝑥)))) |
76 | | f1ocnvfv2 6433 |
. . . . . . . . 9
⊢ (((exp
↾ ℝ):ℝ–1-1-onto→ℝ+ ∧
(abs‘𝑥) ∈
ℝ+) → ((exp ↾ ℝ)‘(◡(exp ↾ ℝ)‘(abs‘𝑥))) = (abs‘𝑥)) |
77 | 24, 23, 76 | sylancr 694 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((exp
↾ ℝ)‘(◡(exp ↾
ℝ)‘(abs‘𝑥))) = (abs‘𝑥)) |
78 | 75, 77 | eqtr3d 2646 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(exp‘(◡(exp ↾
ℝ)‘(abs‘𝑥))) = (abs‘𝑥)) |
79 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑧 = (◡𝐹‘(𝑥 / (abs‘𝑥))) → (i · 𝑧) = (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) |
80 | 79 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑧 = (◡𝐹‘(𝑥 / (abs‘𝑥))) → (exp‘(i · 𝑧)) = (exp‘(i ·
(◡𝐹‘(𝑥 / (abs‘𝑥)))))) |
81 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑧 → (i · 𝑤) = (i · 𝑧)) |
82 | 81 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑧 → (exp‘(i · 𝑤)) = (exp‘(i ·
𝑧))) |
83 | 82 | cbvmptv 4678 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ 𝐷 ↦ (exp‘(i · 𝑤))) = (𝑧 ∈ 𝐷 ↦ (exp‘(i · 𝑧))) |
84 | 34, 83 | eqtri 2632 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑧 ∈ 𝐷 ↦ (exp‘(i · 𝑧))) |
85 | | fvex 6113 |
. . . . . . . . . 10
⊢
(exp‘(i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ∈ V |
86 | 80, 84, 85 | fvmpt 6191 |
. . . . . . . . 9
⊢ ((◡𝐹‘(𝑥 / (abs‘𝑥))) ∈ 𝐷 → (𝐹‘(◡𝐹‘(𝑥 / (abs‘𝑥)))) = (exp‘(i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))) |
87 | 59, 86 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝐹‘(◡𝐹‘(𝑥 / (abs‘𝑥)))) = (exp‘(i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))) |
88 | 39 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝐹:𝐷–1-1-onto→(◡abs
“ {1})) |
89 | | f1ocnvfv2 6433 |
. . . . . . . . 9
⊢ ((𝐹:𝐷–1-1-onto→(◡abs
“ {1}) ∧ (𝑥 /
(abs‘𝑥)) ∈
(◡abs “ {1})) → (𝐹‘(◡𝐹‘(𝑥 / (abs‘𝑥)))) = (𝑥 / (abs‘𝑥))) |
90 | 88, 58, 89 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝐹‘(◡𝐹‘(𝑥 / (abs‘𝑥)))) = (𝑥 / (abs‘𝑥))) |
91 | 87, 90 | eqtr3d 2646 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(exp‘(i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) = (𝑥 / (abs‘𝑥))) |
92 | 78, 91 | oveq12d 6567 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
((exp‘(◡(exp ↾
ℝ)‘(abs‘𝑥))) · (exp‘(i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))) = ((abs‘𝑥) · (𝑥 / (abs‘𝑥)))) |
93 | 21, 45, 46 | divcan2d 10682 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
((abs‘𝑥) ·
(𝑥 / (abs‘𝑥))) = 𝑥) |
94 | 73, 92, 93 | 3eqtrrd 2649 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑥 = (exp‘((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))))) |
95 | 94 | adantrl 748 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ (ℂ ∖ {0}))) → 𝑥 = (exp‘((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))))) |
96 | | fveq2 6103 |
. . . . 5
⊢ (𝑦 = ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) → (exp‘𝑦) = (exp‘((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))))) |
97 | 96 | eqeq2d 2620 |
. . . 4
⊢ (𝑦 = ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) → (𝑥 = (exp‘𝑦) ↔ 𝑥 = (exp‘((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))))) |
98 | 95, 97 | syl5ibrcom 236 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ (ℂ ∖ {0}))) → (𝑦 = ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) → 𝑥 = (exp‘𝑦))) |
99 | 14 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ ℂ) |
100 | 99 | replimd 13785 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑦 = ((ℜ‘𝑦) + (i · (ℑ‘𝑦)))) |
101 | | absef 14766 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℂ →
(abs‘(exp‘𝑦)) =
(exp‘(ℜ‘𝑦))) |
102 | 99, 101 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (abs‘(exp‘𝑦)) =
(exp‘(ℜ‘𝑦))) |
103 | 99 | recld 13782 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (ℜ‘𝑦) ∈ ℝ) |
104 | | fvres 6117 |
. . . . . . . . . . 11
⊢
((ℜ‘𝑦)
∈ ℝ → ((exp ↾ ℝ)‘(ℜ‘𝑦)) =
(exp‘(ℜ‘𝑦))) |
105 | 103, 104 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ((exp ↾
ℝ)‘(ℜ‘𝑦)) = (exp‘(ℜ‘𝑦))) |
106 | 102, 105 | eqtr4d 2647 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (abs‘(exp‘𝑦)) = ((exp ↾
ℝ)‘(ℜ‘𝑦))) |
107 | 106 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (◡(exp ↾
ℝ)‘(abs‘(exp‘𝑦))) = (◡(exp ↾ ℝ)‘((exp ↾
ℝ)‘(ℜ‘𝑦)))) |
108 | | f1ocnvfv1 6432 |
. . . . . . . . 9
⊢ (((exp
↾ ℝ):ℝ–1-1-onto→ℝ+ ∧
(ℜ‘𝑦) ∈
ℝ) → (◡(exp ↾
ℝ)‘((exp ↾ ℝ)‘(ℜ‘𝑦))) = (ℜ‘𝑦)) |
109 | 24, 103, 108 | sylancr 694 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (◡(exp ↾ ℝ)‘((exp ↾
ℝ)‘(ℜ‘𝑦))) = (ℜ‘𝑦)) |
110 | 107, 109 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (◡(exp ↾
ℝ)‘(abs‘(exp‘𝑦))) = (ℜ‘𝑦)) |
111 | 99 | imcld 13783 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (ℑ‘𝑦) ∈ ℝ) |
112 | 111 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (ℑ‘𝑦) ∈ ℂ) |
113 | | mulcl 9899 |
. . . . . . . . . . . . . 14
⊢ ((i
∈ ℂ ∧ (ℑ‘𝑦) ∈ ℂ) → (i ·
(ℑ‘𝑦)) ∈
ℂ) |
114 | 31, 112, 113 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (i · (ℑ‘𝑦)) ∈
ℂ) |
115 | | efcl 14652 |
. . . . . . . . . . . . 13
⊢ ((i
· (ℑ‘𝑦))
∈ ℂ → (exp‘(i · (ℑ‘𝑦))) ∈ ℂ) |
116 | 114, 115 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (exp‘(i ·
(ℑ‘𝑦))) ∈
ℂ) |
117 | 103 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (ℜ‘𝑦) ∈ ℂ) |
118 | | efcl 14652 |
. . . . . . . . . . . . 13
⊢
((ℜ‘𝑦)
∈ ℂ → (exp‘(ℜ‘𝑦)) ∈ ℂ) |
119 | 117, 118 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (exp‘(ℜ‘𝑦)) ∈
ℂ) |
120 | | efne0 14666 |
. . . . . . . . . . . . 13
⊢
((ℜ‘𝑦)
∈ ℂ → (exp‘(ℜ‘𝑦)) ≠ 0) |
121 | 117, 120 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (exp‘(ℜ‘𝑦)) ≠ 0) |
122 | 116, 119,
121 | divcan3d 10685 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (((exp‘(ℜ‘𝑦)) · (exp‘(i
· (ℑ‘𝑦)))) / (exp‘(ℜ‘𝑦))) = (exp‘(i ·
(ℑ‘𝑦)))) |
123 | 100 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (exp‘𝑦) = (exp‘((ℜ‘𝑦) + (i ·
(ℑ‘𝑦))))) |
124 | | efadd 14663 |
. . . . . . . . . . . . . 14
⊢
(((ℜ‘𝑦)
∈ ℂ ∧ (i · (ℑ‘𝑦)) ∈ ℂ) →
(exp‘((ℜ‘𝑦) + (i · (ℑ‘𝑦)))) =
((exp‘(ℜ‘𝑦)) · (exp‘(i ·
(ℑ‘𝑦))))) |
125 | 117, 114,
124 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (exp‘((ℜ‘𝑦) + (i ·
(ℑ‘𝑦)))) =
((exp‘(ℜ‘𝑦)) · (exp‘(i ·
(ℑ‘𝑦))))) |
126 | 123, 125 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (exp‘𝑦) = ((exp‘(ℜ‘𝑦)) · (exp‘(i
· (ℑ‘𝑦))))) |
127 | 126, 102 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ((exp‘𝑦) / (abs‘(exp‘𝑦))) = (((exp‘(ℜ‘𝑦)) · (exp‘(i
· (ℑ‘𝑦)))) / (exp‘(ℜ‘𝑦)))) |
128 | | elpreima 6245 |
. . . . . . . . . . . . . . . 16
⊢ (ℑ
Fn ℂ → (𝑦 ∈
(◡ℑ “ 𝐷) ↔ (𝑦 ∈ ℂ ∧ (ℑ‘𝑦) ∈ 𝐷))) |
129 | 3, 67, 128 | mp2b 10 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (◡ℑ “ 𝐷) ↔ (𝑦 ∈ ℂ ∧ (ℑ‘𝑦) ∈ 𝐷)) |
130 | 129 | simprbi 479 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (◡ℑ “ 𝐷) → (ℑ‘𝑦) ∈ 𝐷) |
131 | 130, 2 | eleq2s 2706 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑆 → (ℑ‘𝑦) ∈ 𝐷) |
132 | 131 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (ℑ‘𝑦) ∈ 𝐷) |
133 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (ℑ‘𝑦) → (i · 𝑤) = (i ·
(ℑ‘𝑦))) |
134 | 133 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (ℑ‘𝑦) → (exp‘(i ·
𝑤)) = (exp‘(i
· (ℑ‘𝑦)))) |
135 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢
(exp‘(i · (ℑ‘𝑦))) ∈ V |
136 | 134, 34, 135 | fvmpt 6191 |
. . . . . . . . . . . 12
⊢
((ℑ‘𝑦)
∈ 𝐷 → (𝐹‘(ℑ‘𝑦)) = (exp‘(i ·
(ℑ‘𝑦)))) |
137 | 132, 136 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝐹‘(ℑ‘𝑦)) = (exp‘(i ·
(ℑ‘𝑦)))) |
138 | 122, 127,
137 | 3eqtr4d 2654 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ((exp‘𝑦) / (abs‘(exp‘𝑦))) = (𝐹‘(ℑ‘𝑦))) |
139 | 138 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦)))) = (◡𝐹‘(𝐹‘(ℑ‘𝑦)))) |
140 | | f1ocnvfv1 6432 |
. . . . . . . . . 10
⊢ ((𝐹:𝐷–1-1-onto→(◡abs
“ {1}) ∧ (ℑ‘𝑦) ∈ 𝐷) → (◡𝐹‘(𝐹‘(ℑ‘𝑦))) = (ℑ‘𝑦)) |
141 | 39, 131, 140 | syl2an 493 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (◡𝐹‘(𝐹‘(ℑ‘𝑦))) = (ℑ‘𝑦)) |
142 | 139, 141 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦)))) = (ℑ‘𝑦)) |
143 | 142 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (i · (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦))))) = (i · (ℑ‘𝑦))) |
144 | 110, 143 | oveq12d 6567 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ((◡(exp ↾
ℝ)‘(abs‘(exp‘𝑦))) + (i · (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦)))))) = ((ℜ‘𝑦) + (i · (ℑ‘𝑦)))) |
145 | 100, 144 | eqtr4d 2647 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑦 = ((◡(exp ↾
ℝ)‘(abs‘(exp‘𝑦))) + (i · (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦))))))) |
146 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = (exp‘𝑦) → (abs‘𝑥) = (abs‘(exp‘𝑦))) |
147 | 146 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑥 = (exp‘𝑦) → (◡(exp ↾ ℝ)‘(abs‘𝑥)) = (◡(exp ↾
ℝ)‘(abs‘(exp‘𝑦)))) |
148 | | id 22 |
. . . . . . . . . 10
⊢ (𝑥 = (exp‘𝑦) → 𝑥 = (exp‘𝑦)) |
149 | 148, 146 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑥 = (exp‘𝑦) → (𝑥 / (abs‘𝑥)) = ((exp‘𝑦) / (abs‘(exp‘𝑦)))) |
150 | 149 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑥 = (exp‘𝑦) → (◡𝐹‘(𝑥 / (abs‘𝑥))) = (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦))))) |
151 | 150 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑥 = (exp‘𝑦) → (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))) = (i · (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦)))))) |
152 | 147, 151 | oveq12d 6567 |
. . . . . 6
⊢ (𝑥 = (exp‘𝑦) → ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) = ((◡(exp ↾
ℝ)‘(abs‘(exp‘𝑦))) + (i · (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦))))))) |
153 | 152 | eqeq2d 2620 |
. . . . 5
⊢ (𝑥 = (exp‘𝑦) → (𝑦 = ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ↔ 𝑦 = ((◡(exp ↾
ℝ)‘(abs‘(exp‘𝑦))) + (i · (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦)))))))) |
154 | 145, 153 | syl5ibrcom 236 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝑥 = (exp‘𝑦) → 𝑦 = ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))))) |
155 | 154 | adantrr 749 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ (ℂ ∖ {0}))) → (𝑥 = (exp‘𝑦) → 𝑦 = ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))))) |
156 | 98, 155 | impbid 201 |
. 2
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ (ℂ ∖ {0}))) → (𝑦 = ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ↔ 𝑥 = (exp‘𝑦))) |
157 | 13, 17, 71, 156 | f1o2d 6785 |
1
⊢ (𝜑 → (exp ↾ 𝑆):𝑆–1-1-onto→(ℂ ∖ {0})) |