Proof of Theorem eff1olem
Step | Hyp | Ref
| Expression |
1 | | cnvimass 5989 |
. . . 4
⊢ (◡ℑ “ 𝐷) ⊆ dom ℑ |
2 | | eff1olem.2 |
. . . 4
⊢ 𝑆 = (◡ℑ “ 𝐷) |
3 | | imf 14824 |
. . . . . 6
⊢
ℑ:ℂ⟶ℝ |
4 | 3 | fdmi 6612 |
. . . . 5
⊢ dom
ℑ = ℂ |
5 | 4 | eqcomi 2747 |
. . . 4
⊢ ℂ =
dom ℑ |
6 | 1, 2, 5 | 3sstr4i 3964 |
. . 3
⊢ 𝑆 ⊆
ℂ |
7 | | eff2 15808 |
. . . . . . 7
⊢
exp:ℂ⟶(ℂ ∖ {0}) |
8 | 7 | a1i 11 |
. . . . . 6
⊢ (𝑆 ⊆ ℂ →
exp:ℂ⟶(ℂ ∖ {0})) |
9 | 8 | feqmptd 6837 |
. . . . 5
⊢ (𝑆 ⊆ ℂ → exp =
(𝑦 ∈ ℂ ↦
(exp‘𝑦))) |
10 | 9 | reseq1d 5890 |
. . . 4
⊢ (𝑆 ⊆ ℂ → (exp
↾ 𝑆) = ((𝑦 ∈ ℂ ↦
(exp‘𝑦)) ↾
𝑆)) |
11 | | resmpt 5945 |
. . . 4
⊢ (𝑆 ⊆ ℂ → ((𝑦 ∈ ℂ ↦
(exp‘𝑦)) ↾
𝑆) = (𝑦 ∈ 𝑆 ↦ (exp‘𝑦))) |
12 | 10, 11 | eqtrd 2778 |
. . 3
⊢ (𝑆 ⊆ ℂ → (exp
↾ 𝑆) = (𝑦 ∈ 𝑆 ↦ (exp‘𝑦))) |
13 | 6, 12 | ax-mp 5 |
. 2
⊢ (exp
↾ 𝑆) = (𝑦 ∈ 𝑆 ↦ (exp‘𝑦)) |
14 | 6 | sseli 3917 |
. . . 4
⊢ (𝑦 ∈ 𝑆 → 𝑦 ∈ ℂ) |
15 | 7 | ffvelrni 6960 |
. . . 4
⊢ (𝑦 ∈ ℂ →
(exp‘𝑦) ∈
(ℂ ∖ {0})) |
16 | 14, 15 | syl 17 |
. . 3
⊢ (𝑦 ∈ 𝑆 → (exp‘𝑦) ∈ (ℂ ∖
{0})) |
17 | 16 | adantl 482 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (exp‘𝑦) ∈ (ℂ ∖
{0})) |
18 | | simpr 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑥 ∈ (ℂ ∖
{0})) |
19 | | eldifsn 4720 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (ℂ ∖ {0})
↔ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
20 | 18, 19 | sylib 217 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
21 | 20 | simpld 495 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑥 ∈
ℂ) |
22 | 20 | simprd 496 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑥 ≠ 0) |
23 | 21, 22 | absrpcld 15160 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(abs‘𝑥) ∈
ℝ+) |
24 | | reeff1o 25606 |
. . . . . . . . 9
⊢ (exp
↾ ℝ):ℝ–1-1-onto→ℝ+ |
25 | | f1ocnv 6728 |
. . . . . . . . 9
⊢ ((exp
↾ ℝ):ℝ–1-1-onto→ℝ+ → ◡(exp ↾
ℝ):ℝ+–1-1-onto→ℝ) |
26 | | f1of 6716 |
. . . . . . . . 9
⊢ (◡(exp ↾
ℝ):ℝ+–1-1-onto→ℝ → ◡(exp ↾
ℝ):ℝ+⟶ℝ) |
27 | 24, 25, 26 | mp2b 10 |
. . . . . . . 8
⊢ ◡(exp ↾
ℝ):ℝ+⟶ℝ |
28 | 27 | ffvelrni 6960 |
. . . . . . 7
⊢
((abs‘𝑥)
∈ ℝ+ → (◡(exp ↾ ℝ)‘(abs‘𝑥)) ∈
ℝ) |
29 | 23, 28 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (◡(exp ↾ ℝ)‘(abs‘𝑥)) ∈
ℝ) |
30 | 29 | recnd 11003 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (◡(exp ↾ ℝ)‘(abs‘𝑥)) ∈
ℂ) |
31 | | ax-icn 10930 |
. . . . . 6
⊢ i ∈
ℂ |
32 | | eff1olem.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ⊆ ℝ) |
33 | 32 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝐷 ⊆
ℝ) |
34 | | eff1olem.1 |
. . . . . . . . . . . 12
⊢ 𝐹 = (𝑤 ∈ 𝐷 ↦ (exp‘(i · 𝑤))) |
35 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ (◡abs “ {1}) = (◡abs “ {1}) |
36 | | eff1olem.4 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → (abs‘(𝑥 − 𝑦)) < (2 · π)) |
37 | | eff1olem.5 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → ∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈
ℤ) |
38 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ (sin
↾ (-(π / 2)[,](π / 2))) = (sin ↾ (-(π / 2)[,](π /
2))) |
39 | 34, 35, 32, 36, 37, 38 | efif1olem4 25701 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐷–1-1-onto→(◡abs
“ {1})) |
40 | | f1ocnv 6728 |
. . . . . . . . . . 11
⊢ (𝐹:𝐷–1-1-onto→(◡abs
“ {1}) → ◡𝐹:(◡abs “ {1})–1-1-onto→𝐷) |
41 | | f1of 6716 |
. . . . . . . . . . 11
⊢ (◡𝐹:(◡abs “ {1})–1-1-onto→𝐷 → ◡𝐹:(◡abs “ {1})⟶𝐷) |
42 | 39, 40, 41 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → ◡𝐹:(◡abs “ {1})⟶𝐷) |
43 | 42 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ◡𝐹:(◡abs “ {1})⟶𝐷) |
44 | 21 | abscld 15148 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(abs‘𝑥) ∈
ℝ) |
45 | 44 | recnd 11003 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(abs‘𝑥) ∈
ℂ) |
46 | 21, 22 | absne0d 15159 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(abs‘𝑥) ≠
0) |
47 | 21, 45, 46 | divcld 11751 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑥 / (abs‘𝑥)) ∈ ℂ) |
48 | 21, 45, 46 | absdivd 15167 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(abs‘(𝑥 /
(abs‘𝑥))) =
((abs‘𝑥) /
(abs‘(abs‘𝑥)))) |
49 | | absidm 15035 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ →
(abs‘(abs‘𝑥)) =
(abs‘𝑥)) |
50 | 21, 49 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(abs‘(abs‘𝑥)) =
(abs‘𝑥)) |
51 | 50 | oveq2d 7291 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
((abs‘𝑥) /
(abs‘(abs‘𝑥)))
= ((abs‘𝑥) /
(abs‘𝑥))) |
52 | 45, 46 | dividd 11749 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
((abs‘𝑥) /
(abs‘𝑥)) =
1) |
53 | 48, 51, 52 | 3eqtrd 2782 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(abs‘(𝑥 /
(abs‘𝑥))) =
1) |
54 | | absf 15049 |
. . . . . . . . . . 11
⊢
abs:ℂ⟶ℝ |
55 | | ffn 6600 |
. . . . . . . . . . 11
⊢
(abs:ℂ⟶ℝ → abs Fn ℂ) |
56 | | fniniseg 6937 |
. . . . . . . . . . 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 583 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑥 / (abs‘𝑥)) ∈ (◡abs “ {1})) |
59 | 43, 58 | ffvelrnd 6962 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (◡𝐹‘(𝑥 / (abs‘𝑥))) ∈ 𝐷) |
60 | 33, 59 | sseldd 3922 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (◡𝐹‘(𝑥 / (abs‘𝑥))) ∈ ℝ) |
61 | 60 | recnd 11003 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (◡𝐹‘(𝑥 / (abs‘𝑥))) ∈ ℂ) |
62 | | mulcl 10955 |
. . . . . 6
⊢ ((i
∈ ℂ ∧ (◡𝐹‘(𝑥 / (abs‘𝑥))) ∈ ℂ) → (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))) ∈ ℂ) |
63 | 31, 61, 62 | sylancr 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (i
· (◡𝐹‘(𝑥 / (abs‘𝑥)))) ∈ ℂ) |
64 | 30, 63 | addcld 10994 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ∈ ℂ) |
65 | 29, 60 | crimd 14943 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(ℑ‘((◡(exp ↾
ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))) = (◡𝐹‘(𝑥 / (abs‘𝑥)))) |
66 | 65, 59 | eqeltrd 2839 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(ℑ‘((◡(exp ↾
ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))) ∈ 𝐷) |
67 | | ffn 6600 |
. . . . 5
⊢
(ℑ:ℂ⟶ℝ → ℑ Fn
ℂ) |
68 | | elpreima 6935 |
. . . . 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 583 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ∈ (◡ℑ “ 𝐷)) |
71 | 70, 2 | eleqtrrdi 2850 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ∈ 𝑆) |
72 | | efadd 15803 |
. . . . . . 7
⊢ (((◡(exp ↾ ℝ)‘(abs‘𝑥)) ∈ ℂ ∧ (i
· (◡𝐹‘(𝑥 / (abs‘𝑥)))) ∈ ℂ) →
(exp‘((◡(exp ↾
ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))) = ((exp‘(◡(exp ↾ ℝ)‘(abs‘𝑥))) · (exp‘(i
· (◡𝐹‘(𝑥 / (abs‘𝑥))))))) |
73 | 30, 63, 72 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(exp‘((◡(exp ↾
ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))) = ((exp‘(◡(exp ↾ ℝ)‘(abs‘𝑥))) · (exp‘(i
· (◡𝐹‘(𝑥 / (abs‘𝑥))))))) |
74 | 29 | fvresd 6794 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((exp
↾ ℝ)‘(◡(exp ↾
ℝ)‘(abs‘𝑥))) = (exp‘(◡(exp ↾ ℝ)‘(abs‘𝑥)))) |
75 | | f1ocnvfv2 7149 |
. . . . . . . . 9
⊢ (((exp
↾ ℝ):ℝ–1-1-onto→ℝ+ ∧
(abs‘𝑥) ∈
ℝ+) → ((exp ↾ ℝ)‘(◡(exp ↾ ℝ)‘(abs‘𝑥))) = (abs‘𝑥)) |
76 | 24, 23, 75 | sylancr 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((exp
↾ ℝ)‘(◡(exp ↾
ℝ)‘(abs‘𝑥))) = (abs‘𝑥)) |
77 | 74, 76 | eqtr3d 2780 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(exp‘(◡(exp ↾
ℝ)‘(abs‘𝑥))) = (abs‘𝑥)) |
78 | | oveq2 7283 |
. . . . . . . . . . 11
⊢ (𝑧 = (◡𝐹‘(𝑥 / (abs‘𝑥))) → (i · 𝑧) = (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) |
79 | 78 | fveq2d 6778 |
. . . . . . . . . 10
⊢ (𝑧 = (◡𝐹‘(𝑥 / (abs‘𝑥))) → (exp‘(i · 𝑧)) = (exp‘(i ·
(◡𝐹‘(𝑥 / (abs‘𝑥)))))) |
80 | | oveq2 7283 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑧 → (i · 𝑤) = (i · 𝑧)) |
81 | 80 | fveq2d 6778 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑧 → (exp‘(i · 𝑤)) = (exp‘(i ·
𝑧))) |
82 | 81 | cbvmptv 5187 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ 𝐷 ↦ (exp‘(i · 𝑤))) = (𝑧 ∈ 𝐷 ↦ (exp‘(i · 𝑧))) |
83 | 34, 82 | eqtri 2766 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑧 ∈ 𝐷 ↦ (exp‘(i · 𝑧))) |
84 | | fvex 6787 |
. . . . . . . . . 10
⊢
(exp‘(i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ∈ V |
85 | 79, 83, 84 | fvmpt 6875 |
. . . . . . . . 9
⊢ ((◡𝐹‘(𝑥 / (abs‘𝑥))) ∈ 𝐷 → (𝐹‘(◡𝐹‘(𝑥 / (abs‘𝑥)))) = (exp‘(i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))) |
86 | 59, 85 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝐹‘(◡𝐹‘(𝑥 / (abs‘𝑥)))) = (exp‘(i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))) |
87 | 39 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝐹:𝐷–1-1-onto→(◡abs
“ {1})) |
88 | | f1ocnvfv2 7149 |
. . . . . . . . 9
⊢ ((𝐹:𝐷–1-1-onto→(◡abs
“ {1}) ∧ (𝑥 /
(abs‘𝑥)) ∈
(◡abs “ {1})) → (𝐹‘(◡𝐹‘(𝑥 / (abs‘𝑥)))) = (𝑥 / (abs‘𝑥))) |
89 | 87, 58, 88 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝐹‘(◡𝐹‘(𝑥 / (abs‘𝑥)))) = (𝑥 / (abs‘𝑥))) |
90 | 86, 89 | eqtr3d 2780 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(exp‘(i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) = (𝑥 / (abs‘𝑥))) |
91 | 77, 90 | oveq12d 7293 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
((exp‘(◡(exp ↾
ℝ)‘(abs‘𝑥))) · (exp‘(i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))) = ((abs‘𝑥) · (𝑥 / (abs‘𝑥)))) |
92 | 21, 45, 46 | divcan2d 11753 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
((abs‘𝑥) ·
(𝑥 / (abs‘𝑥))) = 𝑥) |
93 | 73, 91, 92 | 3eqtrrd 2783 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑥 = (exp‘((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))))) |
94 | 93 | adantrl 713 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ (ℂ ∖ {0}))) → 𝑥 = (exp‘((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))))) |
95 | | fveq2 6774 |
. . . . 5
⊢ (𝑦 = ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) → (exp‘𝑦) = (exp‘((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))))) |
96 | 95 | eqeq2d 2749 |
. . . 4
⊢ (𝑦 = ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) → (𝑥 = (exp‘𝑦) ↔ 𝑥 = (exp‘((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))))))) |
97 | 94, 96 | syl5ibrcom 246 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ (ℂ ∖ {0}))) → (𝑦 = ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) → 𝑥 = (exp‘𝑦))) |
98 | 14 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ ℂ) |
99 | 98 | replimd 14908 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑦 = ((ℜ‘𝑦) + (i · (ℑ‘𝑦)))) |
100 | | absef 15906 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℂ →
(abs‘(exp‘𝑦)) =
(exp‘(ℜ‘𝑦))) |
101 | 98, 100 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (abs‘(exp‘𝑦)) =
(exp‘(ℜ‘𝑦))) |
102 | 98 | recld 14905 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (ℜ‘𝑦) ∈ ℝ) |
103 | 102 | fvresd 6794 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ((exp ↾
ℝ)‘(ℜ‘𝑦)) = (exp‘(ℜ‘𝑦))) |
104 | 101, 103 | eqtr4d 2781 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (abs‘(exp‘𝑦)) = ((exp ↾
ℝ)‘(ℜ‘𝑦))) |
105 | 104 | fveq2d 6778 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (◡(exp ↾
ℝ)‘(abs‘(exp‘𝑦))) = (◡(exp ↾ ℝ)‘((exp ↾
ℝ)‘(ℜ‘𝑦)))) |
106 | | f1ocnvfv1 7148 |
. . . . . . . . 9
⊢ (((exp
↾ ℝ):ℝ–1-1-onto→ℝ+ ∧
(ℜ‘𝑦) ∈
ℝ) → (◡(exp ↾
ℝ)‘((exp ↾ ℝ)‘(ℜ‘𝑦))) = (ℜ‘𝑦)) |
107 | 24, 102, 106 | sylancr 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (◡(exp ↾ ℝ)‘((exp ↾
ℝ)‘(ℜ‘𝑦))) = (ℜ‘𝑦)) |
108 | 105, 107 | eqtrd 2778 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (◡(exp ↾
ℝ)‘(abs‘(exp‘𝑦))) = (ℜ‘𝑦)) |
109 | 98 | imcld 14906 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (ℑ‘𝑦) ∈ ℝ) |
110 | 109 | recnd 11003 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (ℑ‘𝑦) ∈ ℂ) |
111 | | mulcl 10955 |
. . . . . . . . . . . . . 14
⊢ ((i
∈ ℂ ∧ (ℑ‘𝑦) ∈ ℂ) → (i ·
(ℑ‘𝑦)) ∈
ℂ) |
112 | 31, 110, 111 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (i · (ℑ‘𝑦)) ∈
ℂ) |
113 | | efcl 15792 |
. . . . . . . . . . . . 13
⊢ ((i
· (ℑ‘𝑦))
∈ ℂ → (exp‘(i · (ℑ‘𝑦))) ∈ ℂ) |
114 | 112, 113 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (exp‘(i ·
(ℑ‘𝑦))) ∈
ℂ) |
115 | 102 | recnd 11003 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (ℜ‘𝑦) ∈ ℂ) |
116 | | efcl 15792 |
. . . . . . . . . . . . 13
⊢
((ℜ‘𝑦)
∈ ℂ → (exp‘(ℜ‘𝑦)) ∈ ℂ) |
117 | 115, 116 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (exp‘(ℜ‘𝑦)) ∈
ℂ) |
118 | | efne0 15806 |
. . . . . . . . . . . . 13
⊢
((ℜ‘𝑦)
∈ ℂ → (exp‘(ℜ‘𝑦)) ≠ 0) |
119 | 115, 118 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (exp‘(ℜ‘𝑦)) ≠ 0) |
120 | 114, 117,
119 | divcan3d 11756 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (((exp‘(ℜ‘𝑦)) · (exp‘(i
· (ℑ‘𝑦)))) / (exp‘(ℜ‘𝑦))) = (exp‘(i ·
(ℑ‘𝑦)))) |
121 | 99 | fveq2d 6778 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (exp‘𝑦) = (exp‘((ℜ‘𝑦) + (i ·
(ℑ‘𝑦))))) |
122 | | efadd 15803 |
. . . . . . . . . . . . . 14
⊢
(((ℜ‘𝑦)
∈ ℂ ∧ (i · (ℑ‘𝑦)) ∈ ℂ) →
(exp‘((ℜ‘𝑦) + (i · (ℑ‘𝑦)))) =
((exp‘(ℜ‘𝑦)) · (exp‘(i ·
(ℑ‘𝑦))))) |
123 | 115, 112,
122 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (exp‘((ℜ‘𝑦) + (i ·
(ℑ‘𝑦)))) =
((exp‘(ℜ‘𝑦)) · (exp‘(i ·
(ℑ‘𝑦))))) |
124 | 121, 123 | eqtrd 2778 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (exp‘𝑦) = ((exp‘(ℜ‘𝑦)) · (exp‘(i
· (ℑ‘𝑦))))) |
125 | 124, 101 | oveq12d 7293 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ((exp‘𝑦) / (abs‘(exp‘𝑦))) = (((exp‘(ℜ‘𝑦)) · (exp‘(i
· (ℑ‘𝑦)))) / (exp‘(ℜ‘𝑦)))) |
126 | | elpreima 6935 |
. . . . . . . . . . . . . . . 16
⊢ (ℑ
Fn ℂ → (𝑦 ∈
(◡ℑ “ 𝐷) ↔ (𝑦 ∈ ℂ ∧ (ℑ‘𝑦) ∈ 𝐷))) |
127 | 3, 67, 126 | mp2b 10 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (◡ℑ “ 𝐷) ↔ (𝑦 ∈ ℂ ∧ (ℑ‘𝑦) ∈ 𝐷)) |
128 | 127 | simprbi 497 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (◡ℑ “ 𝐷) → (ℑ‘𝑦) ∈ 𝐷) |
129 | 128, 2 | eleq2s 2857 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑆 → (ℑ‘𝑦) ∈ 𝐷) |
130 | 129 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (ℑ‘𝑦) ∈ 𝐷) |
131 | | oveq2 7283 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (ℑ‘𝑦) → (i · 𝑤) = (i ·
(ℑ‘𝑦))) |
132 | 131 | fveq2d 6778 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (ℑ‘𝑦) → (exp‘(i ·
𝑤)) = (exp‘(i
· (ℑ‘𝑦)))) |
133 | | fvex 6787 |
. . . . . . . . . . . . 13
⊢
(exp‘(i · (ℑ‘𝑦))) ∈ V |
134 | 132, 34, 133 | fvmpt 6875 |
. . . . . . . . . . . 12
⊢
((ℑ‘𝑦)
∈ 𝐷 → (𝐹‘(ℑ‘𝑦)) = (exp‘(i ·
(ℑ‘𝑦)))) |
135 | 130, 134 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝐹‘(ℑ‘𝑦)) = (exp‘(i ·
(ℑ‘𝑦)))) |
136 | 120, 125,
135 | 3eqtr4d 2788 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ((exp‘𝑦) / (abs‘(exp‘𝑦))) = (𝐹‘(ℑ‘𝑦))) |
137 | 136 | fveq2d 6778 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦)))) = (◡𝐹‘(𝐹‘(ℑ‘𝑦)))) |
138 | | f1ocnvfv1 7148 |
. . . . . . . . . 10
⊢ ((𝐹:𝐷–1-1-onto→(◡abs
“ {1}) ∧ (ℑ‘𝑦) ∈ 𝐷) → (◡𝐹‘(𝐹‘(ℑ‘𝑦))) = (ℑ‘𝑦)) |
139 | 39, 129, 138 | syl2an 596 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (◡𝐹‘(𝐹‘(ℑ‘𝑦))) = (ℑ‘𝑦)) |
140 | 137, 139 | eqtrd 2778 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦)))) = (ℑ‘𝑦)) |
141 | 140 | oveq2d 7291 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (i · (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦))))) = (i · (ℑ‘𝑦))) |
142 | 108, 141 | oveq12d 7293 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ((◡(exp ↾
ℝ)‘(abs‘(exp‘𝑦))) + (i · (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦)))))) = ((ℜ‘𝑦) + (i · (ℑ‘𝑦)))) |
143 | 99, 142 | eqtr4d 2781 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑦 = ((◡(exp ↾
ℝ)‘(abs‘(exp‘𝑦))) + (i · (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦))))))) |
144 | | fveq2 6774 |
. . . . . . . 8
⊢ (𝑥 = (exp‘𝑦) → (abs‘𝑥) = (abs‘(exp‘𝑦))) |
145 | 144 | fveq2d 6778 |
. . . . . . 7
⊢ (𝑥 = (exp‘𝑦) → (◡(exp ↾ ℝ)‘(abs‘𝑥)) = (◡(exp ↾
ℝ)‘(abs‘(exp‘𝑦)))) |
146 | | id 22 |
. . . . . . . . . 10
⊢ (𝑥 = (exp‘𝑦) → 𝑥 = (exp‘𝑦)) |
147 | 146, 144 | oveq12d 7293 |
. . . . . . . . 9
⊢ (𝑥 = (exp‘𝑦) → (𝑥 / (abs‘𝑥)) = ((exp‘𝑦) / (abs‘(exp‘𝑦)))) |
148 | 147 | fveq2d 6778 |
. . . . . . . 8
⊢ (𝑥 = (exp‘𝑦) → (◡𝐹‘(𝑥 / (abs‘𝑥))) = (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦))))) |
149 | 148 | oveq2d 7291 |
. . . . . . 7
⊢ (𝑥 = (exp‘𝑦) → (i · (◡𝐹‘(𝑥 / (abs‘𝑥)))) = (i · (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦)))))) |
150 | 145, 149 | oveq12d 7293 |
. . . . . 6
⊢ (𝑥 = (exp‘𝑦) → ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) = ((◡(exp ↾
ℝ)‘(abs‘(exp‘𝑦))) + (i · (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦))))))) |
151 | 150 | eqeq2d 2749 |
. . . . 5
⊢ (𝑥 = (exp‘𝑦) → (𝑦 = ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ↔ 𝑦 = ((◡(exp ↾
ℝ)‘(abs‘(exp‘𝑦))) + (i · (◡𝐹‘((exp‘𝑦) / (abs‘(exp‘𝑦)))))))) |
152 | 143, 151 | syl5ibrcom 246 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝑥 = (exp‘𝑦) → 𝑦 = ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))))) |
153 | 152 | adantrr 714 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ (ℂ ∖ {0}))) → (𝑥 = (exp‘𝑦) → 𝑦 = ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))))) |
154 | 97, 153 | impbid 211 |
. 2
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ (ℂ ∖ {0}))) → (𝑦 = ((◡(exp ↾ ℝ)‘(abs‘𝑥)) + (i · (◡𝐹‘(𝑥 / (abs‘𝑥))))) ↔ 𝑥 = (exp‘𝑦))) |
155 | 13, 17, 71, 154 | f1o2d 7523 |
1
⊢ (𝜑 → (exp ↾ 𝑆):𝑆–1-1-onto→(ℂ ∖ {0})) |