Step | Hyp | Ref
| Expression |
1 | | logf1o 24748 |
. . . . . . 7
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log |
2 | | f1of 6391 |
. . . . . . 7
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → log:(ℂ ∖ {0})⟶ran log) |
3 | 1, 2 | ax-mp 5 |
. . . . . 6
⊢
log:(ℂ ∖ {0})⟶ran log |
4 | | logcn.d |
. . . . . . 7
⊢ 𝐷 = (ℂ ∖
(-∞(,]0)) |
5 | 4 | logdmss 24825 |
. . . . . 6
⊢ 𝐷 ⊆ (ℂ ∖
{0}) |
6 | | fssres 6320 |
. . . . . 6
⊢
((log:(ℂ ∖ {0})⟶ran log ∧ 𝐷 ⊆ (ℂ ∖ {0})) → (log
↾ 𝐷):𝐷⟶ran
log) |
7 | 3, 5, 6 | mp2an 682 |
. . . . 5
⊢ (log
↾ 𝐷):𝐷⟶ran log |
8 | | ffn 6291 |
. . . . 5
⊢ ((log
↾ 𝐷):𝐷⟶ran log → (log
↾ 𝐷) Fn 𝐷) |
9 | 7, 8 | ax-mp 5 |
. . . 4
⊢ (log
↾ 𝐷) Fn 𝐷 |
10 | | dffn5 6501 |
. . . 4
⊢ ((log
↾ 𝐷) Fn 𝐷 ↔ (log ↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ ((log ↾ 𝐷)‘𝑥))) |
11 | 9, 10 | mpbi 222 |
. . 3
⊢ (log
↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ ((log ↾ 𝐷)‘𝑥)) |
12 | | fvres 6465 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → ((log ↾ 𝐷)‘𝑥) = (log‘𝑥)) |
13 | 4 | ellogdm 24822 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ ℂ ∧ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ+))) |
14 | 13 | simplbi 493 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ) |
15 | 4 | logdmn0 24823 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → 𝑥 ≠ 0) |
16 | 14, 15 | logcld 24754 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (log‘𝑥) ∈ ℂ) |
17 | 16 | replimd 14344 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (log‘𝑥) = ((ℜ‘(log‘𝑥)) + (i ·
(ℑ‘(log‘𝑥))))) |
18 | | relog 24780 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) →
(ℜ‘(log‘𝑥)) = (log‘(abs‘𝑥))) |
19 | 14, 15, 18 | syl2anc 579 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (ℜ‘(log‘𝑥)) = (log‘(abs‘𝑥))) |
20 | 14, 15 | absrpcld 14595 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (abs‘𝑥) ∈
ℝ+) |
21 | | fvres 6465 |
. . . . . . . 8
⊢
((abs‘𝑥)
∈ ℝ+ → ((log ↾
ℝ+)‘(abs‘𝑥)) = (log‘(abs‘𝑥))) |
22 | 20, 21 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → ((log ↾
ℝ+)‘(abs‘𝑥)) = (log‘(abs‘𝑥))) |
23 | 19, 22 | eqtr4d 2817 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (ℜ‘(log‘𝑥)) = ((log ↾
ℝ+)‘(abs‘𝑥))) |
24 | 23 | oveq1d 6937 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → ((ℜ‘(log‘𝑥)) + (i ·
(ℑ‘(log‘𝑥)))) = (((log ↾
ℝ+)‘(abs‘𝑥)) + (i ·
(ℑ‘(log‘𝑥))))) |
25 | 12, 17, 24 | 3eqtrd 2818 |
. . . 4
⊢ (𝑥 ∈ 𝐷 → ((log ↾ 𝐷)‘𝑥) = (((log ↾
ℝ+)‘(abs‘𝑥)) + (i ·
(ℑ‘(log‘𝑥))))) |
26 | 25 | mpteq2ia 4975 |
. . 3
⊢ (𝑥 ∈ 𝐷 ↦ ((log ↾ 𝐷)‘𝑥)) = (𝑥 ∈ 𝐷 ↦ (((log ↾
ℝ+)‘(abs‘𝑥)) + (i ·
(ℑ‘(log‘𝑥))))) |
27 | 11, 26 | eqtri 2802 |
. 2
⊢ (log
↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ (((log ↾
ℝ+)‘(abs‘𝑥)) + (i ·
(ℑ‘(log‘𝑥))))) |
28 | | eqid 2778 |
. . . 4
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
29 | 28 | addcn 23076 |
. . . . 5
⊢ + ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
30 | 29 | a1i 11 |
. . . 4
⊢ (⊤
→ + ∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
31 | 28 | cnfldtopon 22994 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
32 | 14 | ssriv 3825 |
. . . . . . . 8
⊢ 𝐷 ⊆
ℂ |
33 | | resttopon 21373 |
. . . . . . . 8
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ 𝐷 ⊆ ℂ)
→ ((TopOpen‘ℂfld) ↾t 𝐷) ∈ (TopOn‘𝐷)) |
34 | 31, 32, 33 | mp2an 682 |
. . . . . . 7
⊢
((TopOpen‘ℂfld) ↾t 𝐷) ∈ (TopOn‘𝐷) |
35 | 34 | a1i 11 |
. . . . . 6
⊢ (⊤
→ ((TopOpen‘ℂfld) ↾t 𝐷) ∈ (TopOn‘𝐷)) |
36 | | absf 14484 |
. . . . . . . . . . . 12
⊢
abs:ℂ⟶ℝ |
37 | | fssres 6320 |
. . . . . . . . . . . 12
⊢
((abs:ℂ⟶ℝ ∧ 𝐷 ⊆ ℂ) → (abs ↾ 𝐷):𝐷⟶ℝ) |
38 | 36, 32, 37 | mp2an 682 |
. . . . . . . . . . 11
⊢ (abs
↾ 𝐷):𝐷⟶ℝ |
39 | 38 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ (abs ↾ 𝐷):𝐷⟶ℝ) |
40 | 39 | feqmptd 6509 |
. . . . . . . . 9
⊢ (⊤
→ (abs ↾ 𝐷) =
(𝑥 ∈ 𝐷 ↦ ((abs ↾ 𝐷)‘𝑥))) |
41 | | fvres 6465 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → ((abs ↾ 𝐷)‘𝑥) = (abs‘𝑥)) |
42 | 41 | mpteq2ia 4975 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 ↦ ((abs ↾ 𝐷)‘𝑥)) = (𝑥 ∈ 𝐷 ↦ (abs‘𝑥)) |
43 | 40, 42 | syl6eq 2830 |
. . . . . . . 8
⊢ (⊤
→ (abs ↾ 𝐷) =
(𝑥 ∈ 𝐷 ↦ (abs‘𝑥))) |
44 | | ffn 6291 |
. . . . . . . . . . 11
⊢ ((abs
↾ 𝐷):𝐷⟶ℝ → (abs
↾ 𝐷) Fn 𝐷) |
45 | 38, 44 | ax-mp 5 |
. . . . . . . . . 10
⊢ (abs
↾ 𝐷) Fn 𝐷 |
46 | 41, 20 | eqeltrd 2859 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → ((abs ↾ 𝐷)‘𝑥) ∈
ℝ+) |
47 | 46 | rgen 3104 |
. . . . . . . . . 10
⊢
∀𝑥 ∈
𝐷 ((abs ↾ 𝐷)‘𝑥) ∈ ℝ+ |
48 | | ffnfv 6652 |
. . . . . . . . . 10
⊢ ((abs
↾ 𝐷):𝐷⟶ℝ+
↔ ((abs ↾ 𝐷) Fn
𝐷 ∧ ∀𝑥 ∈ 𝐷 ((abs ↾ 𝐷)‘𝑥) ∈
ℝ+)) |
49 | 45, 47, 48 | mpbir2an 701 |
. . . . . . . . 9
⊢ (abs
↾ 𝐷):𝐷⟶ℝ+ |
50 | | rpssre 12144 |
. . . . . . . . . . 11
⊢
ℝ+ ⊆ ℝ |
51 | | ax-resscn 10329 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℂ |
52 | 50, 51 | sstri 3830 |
. . . . . . . . . 10
⊢
ℝ+ ⊆ ℂ |
53 | | abscncf 23112 |
. . . . . . . . . . 11
⊢ abs
∈ (ℂ–cn→ℝ) |
54 | | rescncf 23108 |
. . . . . . . . . . 11
⊢ (𝐷 ⊆ ℂ → (abs
∈ (ℂ–cn→ℝ)
→ (abs ↾ 𝐷)
∈ (𝐷–cn→ℝ))) |
55 | 32, 53, 54 | mp2 9 |
. . . . . . . . . 10
⊢ (abs
↾ 𝐷) ∈ (𝐷–cn→ℝ) |
56 | | cncffvrn 23109 |
. . . . . . . . . 10
⊢
((ℝ+ ⊆ ℂ ∧ (abs ↾ 𝐷) ∈ (𝐷–cn→ℝ)) → ((abs ↾ 𝐷) ∈ (𝐷–cn→ℝ+) ↔ (abs ↾ 𝐷):𝐷⟶ℝ+)) |
57 | 52, 55, 56 | mp2an 682 |
. . . . . . . . 9
⊢ ((abs
↾ 𝐷) ∈ (𝐷–cn→ℝ+) ↔ (abs ↾ 𝐷):𝐷⟶ℝ+) |
58 | 49, 57 | mpbir 223 |
. . . . . . . 8
⊢ (abs
↾ 𝐷) ∈ (𝐷–cn→ℝ+) |
59 | 43, 58 | syl6eqelr 2868 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈ 𝐷 ↦ (abs‘𝑥)) ∈ (𝐷–cn→ℝ+)) |
60 | | eqid 2778 |
. . . . . . . . 9
⊢
((TopOpen‘ℂfld) ↾t 𝐷) =
((TopOpen‘ℂfld) ↾t 𝐷) |
61 | | eqid 2778 |
. . . . . . . . 9
⊢
((TopOpen‘ℂfld) ↾t
ℝ+) = ((TopOpen‘ℂfld)
↾t ℝ+) |
62 | 28, 60, 61 | cncfcn 23120 |
. . . . . . . 8
⊢ ((𝐷 ⊆ ℂ ∧
ℝ+ ⊆ ℂ) → (𝐷–cn→ℝ+) =
(((TopOpen‘ℂfld) ↾t 𝐷) Cn ((TopOpen‘ℂfld)
↾t ℝ+))) |
63 | 32, 52, 62 | mp2an 682 |
. . . . . . 7
⊢ (𝐷–cn→ℝ+) =
(((TopOpen‘ℂfld) ↾t 𝐷) Cn ((TopOpen‘ℂfld)
↾t ℝ+)) |
64 | 59, 63 | syl6eleq 2869 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈ 𝐷 ↦ (abs‘𝑥)) ∈
(((TopOpen‘ℂfld) ↾t 𝐷) Cn ((TopOpen‘ℂfld)
↾t ℝ+))) |
65 | | ssid 3842 |
. . . . . . . . . 10
⊢ ℂ
⊆ ℂ |
66 | | cncfss 23110 |
. . . . . . . . . 10
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) →
(ℝ+–cn→ℝ) ⊆
(ℝ+–cn→ℂ)) |
67 | 51, 65, 66 | mp2an 682 |
. . . . . . . . 9
⊢
(ℝ+–cn→ℝ) ⊆
(ℝ+–cn→ℂ) |
68 | | relogcn 24821 |
. . . . . . . . 9
⊢ (log
↾ ℝ+) ∈ (ℝ+–cn→ℝ) |
69 | 67, 68 | sselii 3818 |
. . . . . . . 8
⊢ (log
↾ ℝ+) ∈ (ℝ+–cn→ℂ) |
70 | 69 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ (log ↾ ℝ+) ∈
(ℝ+–cn→ℂ)) |
71 | 31 | toponrestid 21133 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
72 | 28, 61, 71 | cncfcn 23120 |
. . . . . . . 8
⊢
((ℝ+ ⊆ ℂ ∧ ℂ ⊆ ℂ)
→ (ℝ+–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t
ℝ+) Cn
(TopOpen‘ℂfld))) |
73 | 52, 65, 72 | mp2an 682 |
. . . . . . 7
⊢
(ℝ+–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t
ℝ+) Cn (TopOpen‘ℂfld)) |
74 | 70, 73 | syl6eleq 2869 |
. . . . . 6
⊢ (⊤
→ (log ↾ ℝ+) ∈
(((TopOpen‘ℂfld) ↾t
ℝ+) Cn
(TopOpen‘ℂfld))) |
75 | 35, 64, 74 | cnmpt11f 21876 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈ 𝐷 ↦ ((log ↾
ℝ+)‘(abs‘𝑥))) ∈
(((TopOpen‘ℂfld) ↾t 𝐷) Cn
(TopOpen‘ℂfld))) |
76 | 28, 60, 71 | cncfcn 23120 |
. . . . . 6
⊢ ((𝐷 ⊆ ℂ ∧ ℂ
⊆ ℂ) → (𝐷–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t 𝐷) Cn
(TopOpen‘ℂfld))) |
77 | 32, 65, 76 | mp2an 682 |
. . . . 5
⊢ (𝐷–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t 𝐷) Cn
(TopOpen‘ℂfld)) |
78 | 75, 77 | syl6eleqr 2870 |
. . . 4
⊢ (⊤
→ (𝑥 ∈ 𝐷 ↦ ((log ↾
ℝ+)‘(abs‘𝑥))) ∈ (𝐷–cn→ℂ)) |
79 | 16 | imcld 14342 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ∈
ℝ) |
80 | 79 | recnd 10405 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ∈
ℂ) |
81 | 80 | adantl 475 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ 𝐷) →
(ℑ‘(log‘𝑥)) ∈ ℂ) |
82 | | eqidd 2779 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈ 𝐷 ↦
(ℑ‘(log‘𝑥))) = (𝑥 ∈ 𝐷 ↦ (ℑ‘(log‘𝑥)))) |
83 | | eqidd 2779 |
. . . . . 6
⊢ (⊤
→ (𝑦 ∈ ℂ
↦ (i · 𝑦)) =
(𝑦 ∈ ℂ ↦
(i · 𝑦))) |
84 | | oveq2 6930 |
. . . . . 6
⊢ (𝑦 =
(ℑ‘(log‘𝑥)) → (i · 𝑦) = (i ·
(ℑ‘(log‘𝑥)))) |
85 | 81, 82, 83, 84 | fmptco 6661 |
. . . . 5
⊢ (⊤
→ ((𝑦 ∈ ℂ
↦ (i · 𝑦))
∘ (𝑥 ∈ 𝐷 ↦
(ℑ‘(log‘𝑥)))) = (𝑥 ∈ 𝐷 ↦ (i ·
(ℑ‘(log‘𝑥))))) |
86 | | cncfss 23110 |
. . . . . . . . 9
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝐷–cn→ℝ) ⊆ (𝐷–cn→ℂ)) |
87 | 51, 65, 86 | mp2an 682 |
. . . . . . . 8
⊢ (𝐷–cn→ℝ) ⊆ (𝐷–cn→ℂ) |
88 | 4 | logcnlem5 24829 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 ↦ (ℑ‘(log‘𝑥))) ∈ (𝐷–cn→ℝ) |
89 | 87, 88 | sselii 3818 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 ↦ (ℑ‘(log‘𝑥))) ∈ (𝐷–cn→ℂ) |
90 | 89 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈ 𝐷 ↦
(ℑ‘(log‘𝑥))) ∈ (𝐷–cn→ℂ)) |
91 | | ax-icn 10331 |
. . . . . . 7
⊢ i ∈
ℂ |
92 | | eqid 2778 |
. . . . . . . 8
⊢ (𝑦 ∈ ℂ ↦ (i
· 𝑦)) = (𝑦 ∈ ℂ ↦ (i
· 𝑦)) |
93 | 92 | mulc1cncf 23116 |
. . . . . . 7
⊢ (i ∈
ℂ → (𝑦 ∈
ℂ ↦ (i · 𝑦)) ∈ (ℂ–cn→ℂ)) |
94 | 91, 93 | mp1i 13 |
. . . . . 6
⊢ (⊤
→ (𝑦 ∈ ℂ
↦ (i · 𝑦))
∈ (ℂ–cn→ℂ)) |
95 | 90, 94 | cncfco 23118 |
. . . . 5
⊢ (⊤
→ ((𝑦 ∈ ℂ
↦ (i · 𝑦))
∘ (𝑥 ∈ 𝐷 ↦
(ℑ‘(log‘𝑥)))) ∈ (𝐷–cn→ℂ)) |
96 | 85, 95 | eqeltrrd 2860 |
. . . 4
⊢ (⊤
→ (𝑥 ∈ 𝐷 ↦ (i ·
(ℑ‘(log‘𝑥)))) ∈ (𝐷–cn→ℂ)) |
97 | 28, 30, 78, 96 | cncfmpt2f 23125 |
. . 3
⊢ (⊤
→ (𝑥 ∈ 𝐷 ↦ (((log ↾
ℝ+)‘(abs‘𝑥)) + (i ·
(ℑ‘(log‘𝑥))))) ∈ (𝐷–cn→ℂ)) |
98 | 97 | mptru 1609 |
. 2
⊢ (𝑥 ∈ 𝐷 ↦ (((log ↾
ℝ+)‘(abs‘𝑥)) + (i ·
(ℑ‘(log‘𝑥))))) ∈ (𝐷–cn→ℂ) |
99 | 27, 98 | eqeltri 2855 |
1
⊢ (log
↾ 𝐷) ∈ (𝐷–cn→ℂ) |