Step | Hyp | Ref
| Expression |
1 | | logf1o 24311 |
. . . . . . 7
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log |
2 | | f1of 6137 |
. . . . . . 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 24388 |
. . . . . 6
⊢ 𝐷 ⊆ (ℂ ∖
{0}) |
6 | | fssres 6070 |
. . . . . 6
⊢
((log:(ℂ ∖ {0})⟶ran log ∧ 𝐷 ⊆ (ℂ ∖ {0})) → (log
↾ 𝐷):𝐷⟶ran
log) |
7 | 3, 5, 6 | mp2an 708 |
. . . . 5
⊢ (log
↾ 𝐷):𝐷⟶ran log |
8 | | ffn 6045 |
. . . . 5
⊢ ((log
↾ 𝐷):𝐷⟶ran log → (log
↾ 𝐷) Fn 𝐷) |
9 | 7, 8 | ax-mp 5 |
. . . 4
⊢ (log
↾ 𝐷) Fn 𝐷 |
10 | | dffn5 6241 |
. . . 4
⊢ ((log
↾ 𝐷) Fn 𝐷 ↔ (log ↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ ((log ↾ 𝐷)‘𝑥))) |
11 | 9, 10 | mpbi 220 |
. . 3
⊢ (log
↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ ((log ↾ 𝐷)‘𝑥)) |
12 | | fvres 6207 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → ((log ↾ 𝐷)‘𝑥) = (log‘𝑥)) |
13 | 4 | ellogdm 24385 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ ℂ ∧ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ+))) |
14 | 13 | simplbi 476 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ) |
15 | 4 | logdmn0 24386 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → 𝑥 ≠ 0) |
16 | 14, 15 | logcld 24317 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (log‘𝑥) ∈ ℂ) |
17 | 16 | replimd 13937 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (log‘𝑥) = ((ℜ‘(log‘𝑥)) + (i ·
(ℑ‘(log‘𝑥))))) |
18 | | relog 24343 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) →
(ℜ‘(log‘𝑥)) = (log‘(abs‘𝑥))) |
19 | 14, 15, 18 | syl2anc 693 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (ℜ‘(log‘𝑥)) = (log‘(abs‘𝑥))) |
20 | 14, 15 | absrpcld 14187 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (abs‘𝑥) ∈
ℝ+) |
21 | | fvres 6207 |
. . . . . . . 8
⊢
((abs‘𝑥)
∈ ℝ+ → ((log ↾
ℝ+)‘(abs‘𝑥)) = (log‘(abs‘𝑥))) |
22 | 20, 21 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → ((log ↾
ℝ+)‘(abs‘𝑥)) = (log‘(abs‘𝑥))) |
23 | 19, 22 | eqtr4d 2659 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (ℜ‘(log‘𝑥)) = ((log ↾
ℝ+)‘(abs‘𝑥))) |
24 | 23 | oveq1d 6665 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → ((ℜ‘(log‘𝑥)) + (i ·
(ℑ‘(log‘𝑥)))) = (((log ↾
ℝ+)‘(abs‘𝑥)) + (i ·
(ℑ‘(log‘𝑥))))) |
25 | 12, 17, 24 | 3eqtrd 2660 |
. . . 4
⊢ (𝑥 ∈ 𝐷 → ((log ↾ 𝐷)‘𝑥) = (((log ↾
ℝ+)‘(abs‘𝑥)) + (i ·
(ℑ‘(log‘𝑥))))) |
26 | 25 | mpteq2ia 4740 |
. . 3
⊢ (𝑥 ∈ 𝐷 ↦ ((log ↾ 𝐷)‘𝑥)) = (𝑥 ∈ 𝐷 ↦ (((log ↾
ℝ+)‘(abs‘𝑥)) + (i ·
(ℑ‘(log‘𝑥))))) |
27 | 11, 26 | eqtri 2644 |
. 2
⊢ (log
↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ (((log ↾
ℝ+)‘(abs‘𝑥)) + (i ·
(ℑ‘(log‘𝑥))))) |
28 | | eqid 2622 |
. . . 4
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
29 | 28 | addcn 22668 |
. . . . 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 22586 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
32 | 14 | ssriv 3607 |
. . . . . . . 8
⊢ 𝐷 ⊆
ℂ |
33 | | resttopon 20965 |
. . . . . . . 8
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ 𝐷 ⊆ ℂ)
→ ((TopOpen‘ℂfld) ↾t 𝐷) ∈ (TopOn‘𝐷)) |
34 | 31, 32, 33 | mp2an 708 |
. . . . . . 7
⊢
((TopOpen‘ℂfld) ↾t 𝐷) ∈ (TopOn‘𝐷) |
35 | 34 | a1i 11 |
. . . . . 6
⊢ (⊤
→ ((TopOpen‘ℂfld) ↾t 𝐷) ∈ (TopOn‘𝐷)) |
36 | | absf 14077 |
. . . . . . . . . . . 12
⊢
abs:ℂ⟶ℝ |
37 | | fssres 6070 |
. . . . . . . . . . . 12
⊢
((abs:ℂ⟶ℝ ∧ 𝐷 ⊆ ℂ) → (abs ↾ 𝐷):𝐷⟶ℝ) |
38 | 36, 32, 37 | mp2an 708 |
. . . . . . . . . . 11
⊢ (abs
↾ 𝐷):𝐷⟶ℝ |
39 | 38 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ (abs ↾ 𝐷):𝐷⟶ℝ) |
40 | 39 | feqmptd 6249 |
. . . . . . . . 9
⊢ (⊤
→ (abs ↾ 𝐷) =
(𝑥 ∈ 𝐷 ↦ ((abs ↾ 𝐷)‘𝑥))) |
41 | | fvres 6207 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → ((abs ↾ 𝐷)‘𝑥) = (abs‘𝑥)) |
42 | 41 | mpteq2ia 4740 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 ↦ ((abs ↾ 𝐷)‘𝑥)) = (𝑥 ∈ 𝐷 ↦ (abs‘𝑥)) |
43 | 40, 42 | syl6eq 2672 |
. . . . . . . 8
⊢ (⊤
→ (abs ↾ 𝐷) =
(𝑥 ∈ 𝐷 ↦ (abs‘𝑥))) |
44 | | ffn 6045 |
. . . . . . . . . . 11
⊢ ((abs
↾ 𝐷):𝐷⟶ℝ → (abs
↾ 𝐷) Fn 𝐷) |
45 | 38, 44 | ax-mp 5 |
. . . . . . . . . 10
⊢ (abs
↾ 𝐷) Fn 𝐷 |
46 | 41, 20 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → ((abs ↾ 𝐷)‘𝑥) ∈
ℝ+) |
47 | 46 | rgen 2922 |
. . . . . . . . . 10
⊢
∀𝑥 ∈
𝐷 ((abs ↾ 𝐷)‘𝑥) ∈ ℝ+ |
48 | | ffnfv 6388 |
. . . . . . . . . 10
⊢ ((abs
↾ 𝐷):𝐷⟶ℝ+
↔ ((abs ↾ 𝐷) Fn
𝐷 ∧ ∀𝑥 ∈ 𝐷 ((abs ↾ 𝐷)‘𝑥) ∈
ℝ+)) |
49 | 45, 47, 48 | mpbir2an 955 |
. . . . . . . . 9
⊢ (abs
↾ 𝐷):𝐷⟶ℝ+ |
50 | | rpssre 11843 |
. . . . . . . . . . 11
⊢
ℝ+ ⊆ ℝ |
51 | | ax-resscn 9993 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℂ |
52 | 50, 51 | sstri 3612 |
. . . . . . . . . 10
⊢
ℝ+ ⊆ ℂ |
53 | | abscncf 22704 |
. . . . . . . . . . 11
⊢ abs
∈ (ℂ–cn→ℝ) |
54 | | rescncf 22700 |
. . . . . . . . . . 11
⊢ (𝐷 ⊆ ℂ → (abs
∈ (ℂ–cn→ℝ)
→ (abs ↾ 𝐷)
∈ (𝐷–cn→ℝ))) |
55 | 32, 53, 54 | mp2 9 |
. . . . . . . . . 10
⊢ (abs
↾ 𝐷) ∈ (𝐷–cn→ℝ) |
56 | | cncffvrn 22701 |
. . . . . . . . . 10
⊢
((ℝ+ ⊆ ℂ ∧ (abs ↾ 𝐷) ∈ (𝐷–cn→ℝ)) → ((abs ↾ 𝐷) ∈ (𝐷–cn→ℝ+) ↔ (abs ↾ 𝐷):𝐷⟶ℝ+)) |
57 | 52, 55, 56 | mp2an 708 |
. . . . . . . . 9
⊢ ((abs
↾ 𝐷) ∈ (𝐷–cn→ℝ+) ↔ (abs ↾ 𝐷):𝐷⟶ℝ+) |
58 | 49, 57 | mpbir 221 |
. . . . . . . 8
⊢ (abs
↾ 𝐷) ∈ (𝐷–cn→ℝ+) |
59 | 43, 58 | syl6eqelr 2710 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈ 𝐷 ↦ (abs‘𝑥)) ∈ (𝐷–cn→ℝ+)) |
60 | | eqid 2622 |
. . . . . . . . 9
⊢
((TopOpen‘ℂfld) ↾t 𝐷) =
((TopOpen‘ℂfld) ↾t 𝐷) |
61 | | eqid 2622 |
. . . . . . . . 9
⊢
((TopOpen‘ℂfld) ↾t
ℝ+) = ((TopOpen‘ℂfld)
↾t ℝ+) |
62 | 28, 60, 61 | cncfcn 22712 |
. . . . . . . 8
⊢ ((𝐷 ⊆ ℂ ∧
ℝ+ ⊆ ℂ) → (𝐷–cn→ℝ+) =
(((TopOpen‘ℂfld) ↾t 𝐷) Cn ((TopOpen‘ℂfld)
↾t ℝ+))) |
63 | 32, 52, 62 | mp2an 708 |
. . . . . . 7
⊢ (𝐷–cn→ℝ+) =
(((TopOpen‘ℂfld) ↾t 𝐷) Cn ((TopOpen‘ℂfld)
↾t ℝ+)) |
64 | 59, 63 | syl6eleq 2711 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈ 𝐷 ↦ (abs‘𝑥)) ∈
(((TopOpen‘ℂfld) ↾t 𝐷) Cn ((TopOpen‘ℂfld)
↾t ℝ+))) |
65 | | ssid 3624 |
. . . . . . . . . 10
⊢ ℂ
⊆ ℂ |
66 | | cncfss 22702 |
. . . . . . . . . 10
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) →
(ℝ+–cn→ℝ) ⊆
(ℝ+–cn→ℂ)) |
67 | 51, 65, 66 | mp2an 708 |
. . . . . . . . 9
⊢
(ℝ+–cn→ℝ) ⊆
(ℝ+–cn→ℂ) |
68 | | relogcn 24384 |
. . . . . . . . 9
⊢ (log
↾ ℝ+) ∈ (ℝ+–cn→ℝ) |
69 | 67, 68 | sselii 3600 |
. . . . . . . 8
⊢ (log
↾ ℝ+) ∈ (ℝ+–cn→ℂ) |
70 | 69 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ (log ↾ ℝ+) ∈
(ℝ+–cn→ℂ)) |
71 | 28 | cnfldtop 22587 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) ∈ Top |
72 | 31 | toponunii 20721 |
. . . . . . . . . . . 12
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
73 | 72 | restid 16094 |
. . . . . . . . . . 11
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
74 | 71, 73 | ax-mp 5 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
75 | 74 | eqcomi 2631 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
76 | 28, 61, 75 | cncfcn 22712 |
. . . . . . . 8
⊢
((ℝ+ ⊆ ℂ ∧ ℂ ⊆ ℂ)
→ (ℝ+–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t
ℝ+) Cn
(TopOpen‘ℂfld))) |
77 | 52, 65, 76 | mp2an 708 |
. . . . . . 7
⊢
(ℝ+–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t
ℝ+) Cn (TopOpen‘ℂfld)) |
78 | 70, 77 | syl6eleq 2711 |
. . . . . 6
⊢ (⊤
→ (log ↾ ℝ+) ∈
(((TopOpen‘ℂfld) ↾t
ℝ+) Cn
(TopOpen‘ℂfld))) |
79 | 35, 64, 78 | cnmpt11f 21467 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈ 𝐷 ↦ ((log ↾
ℝ+)‘(abs‘𝑥))) ∈
(((TopOpen‘ℂfld) ↾t 𝐷) Cn
(TopOpen‘ℂfld))) |
80 | 28, 60, 75 | cncfcn 22712 |
. . . . . 6
⊢ ((𝐷 ⊆ ℂ ∧ ℂ
⊆ ℂ) → (𝐷–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t 𝐷) Cn
(TopOpen‘ℂfld))) |
81 | 32, 65, 80 | mp2an 708 |
. . . . 5
⊢ (𝐷–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t 𝐷) Cn
(TopOpen‘ℂfld)) |
82 | 79, 81 | syl6eleqr 2712 |
. . . 4
⊢ (⊤
→ (𝑥 ∈ 𝐷 ↦ ((log ↾
ℝ+)‘(abs‘𝑥))) ∈ (𝐷–cn→ℂ)) |
83 | 16 | imcld 13935 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ∈
ℝ) |
84 | 83 | recnd 10068 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ∈
ℂ) |
85 | 84 | adantl 482 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ 𝐷) →
(ℑ‘(log‘𝑥)) ∈ ℂ) |
86 | | eqidd 2623 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈ 𝐷 ↦
(ℑ‘(log‘𝑥))) = (𝑥 ∈ 𝐷 ↦ (ℑ‘(log‘𝑥)))) |
87 | | eqidd 2623 |
. . . . . 6
⊢ (⊤
→ (𝑦 ∈ ℂ
↦ (i · 𝑦)) =
(𝑦 ∈ ℂ ↦
(i · 𝑦))) |
88 | | oveq2 6658 |
. . . . . 6
⊢ (𝑦 =
(ℑ‘(log‘𝑥)) → (i · 𝑦) = (i ·
(ℑ‘(log‘𝑥)))) |
89 | 85, 86, 87, 88 | fmptco 6396 |
. . . . 5
⊢ (⊤
→ ((𝑦 ∈ ℂ
↦ (i · 𝑦))
∘ (𝑥 ∈ 𝐷 ↦
(ℑ‘(log‘𝑥)))) = (𝑥 ∈ 𝐷 ↦ (i ·
(ℑ‘(log‘𝑥))))) |
90 | | cncfss 22702 |
. . . . . . . . 9
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝐷–cn→ℝ) ⊆ (𝐷–cn→ℂ)) |
91 | 51, 65, 90 | mp2an 708 |
. . . . . . . 8
⊢ (𝐷–cn→ℝ) ⊆ (𝐷–cn→ℂ) |
92 | 4 | logcnlem5 24392 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 ↦ (ℑ‘(log‘𝑥))) ∈ (𝐷–cn→ℝ) |
93 | 91, 92 | sselii 3600 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 ↦ (ℑ‘(log‘𝑥))) ∈ (𝐷–cn→ℂ) |
94 | 93 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈ 𝐷 ↦
(ℑ‘(log‘𝑥))) ∈ (𝐷–cn→ℂ)) |
95 | | ax-icn 9995 |
. . . . . . 7
⊢ i ∈
ℂ |
96 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑦 ∈ ℂ ↦ (i
· 𝑦)) = (𝑦 ∈ ℂ ↦ (i
· 𝑦)) |
97 | 96 | mulc1cncf 22708 |
. . . . . . 7
⊢ (i ∈
ℂ → (𝑦 ∈
ℂ ↦ (i · 𝑦)) ∈ (ℂ–cn→ℂ)) |
98 | 95, 97 | mp1i 13 |
. . . . . 6
⊢ (⊤
→ (𝑦 ∈ ℂ
↦ (i · 𝑦))
∈ (ℂ–cn→ℂ)) |
99 | 94, 98 | cncfco 22710 |
. . . . 5
⊢ (⊤
→ ((𝑦 ∈ ℂ
↦ (i · 𝑦))
∘ (𝑥 ∈ 𝐷 ↦
(ℑ‘(log‘𝑥)))) ∈ (𝐷–cn→ℂ)) |
100 | 89, 99 | eqeltrrd 2702 |
. . . 4
⊢ (⊤
→ (𝑥 ∈ 𝐷 ↦ (i ·
(ℑ‘(log‘𝑥)))) ∈ (𝐷–cn→ℂ)) |
101 | 28, 30, 82, 100 | cncfmpt2f 22717 |
. . 3
⊢ (⊤
→ (𝑥 ∈ 𝐷 ↦ (((log ↾
ℝ+)‘(abs‘𝑥)) + (i ·
(ℑ‘(log‘𝑥))))) ∈ (𝐷–cn→ℂ)) |
102 | 101 | trud 1493 |
. 2
⊢ (𝑥 ∈ 𝐷 ↦ (((log ↾
ℝ+)‘(abs‘𝑥)) + (i ·
(ℑ‘(log‘𝑥))))) ∈ (𝐷–cn→ℂ) |
103 | 27, 102 | eqeltri 2697 |
1
⊢ (log
↾ 𝐷) ∈ (𝐷–cn→ℂ) |