Step | Hyp | Ref
| Expression |
1 | | logf1o 24311 |
. . . . . 6
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log |
2 | | f1ofun 6139 |
. . . . . 6
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → Fun log) |
3 | 1, 2 | ax-mp 5 |
. . . . 5
⊢ Fun
log |
4 | | logcn.d |
. . . . . . 7
⊢ 𝐷 = (ℂ ∖
(-∞(,]0)) |
5 | 4 | logdmss 24388 |
. . . . . 6
⊢ 𝐷 ⊆ (ℂ ∖
{0}) |
6 | | f1odm 6141 |
. . . . . . 7
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → dom log = (ℂ ∖ {0})) |
7 | 1, 6 | ax-mp 5 |
. . . . . 6
⊢ dom log =
(ℂ ∖ {0}) |
8 | 5, 7 | sseqtr4i 3638 |
. . . . 5
⊢ 𝐷 ⊆ dom
log |
9 | | funimass4 6247 |
. . . . 5
⊢ ((Fun log
∧ 𝐷 ⊆ dom log)
→ ((log “ 𝐷)
⊆ (◡ℑ “
(-π(,)π)) ↔ ∀𝑥 ∈ 𝐷 (log‘𝑥) ∈ (◡ℑ “
(-π(,)π)))) |
10 | 3, 8, 9 | mp2an 708 |
. . . 4
⊢ ((log
“ 𝐷) ⊆ (◡ℑ “ (-π(,)π)) ↔
∀𝑥 ∈ 𝐷 (log‘𝑥) ∈ (◡ℑ “
(-π(,)π))) |
11 | 4 | ellogdm 24385 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ ℂ ∧ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ+))) |
12 | 11 | simplbi 476 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ) |
13 | 4 | logdmn0 24386 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → 𝑥 ≠ 0) |
14 | 12, 13 | logcld 24317 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (log‘𝑥) ∈ ℂ) |
15 | 14 | imcld 13935 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ∈
ℝ) |
16 | 12, 13 | logimcld 24318 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (-π <
(ℑ‘(log‘𝑥)) ∧ (ℑ‘(log‘𝑥)) ≤ π)) |
17 | 16 | simpld 475 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → -π <
(ℑ‘(log‘𝑥))) |
18 | 4 | logdmnrp 24387 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → ¬ -𝑥 ∈ ℝ+) |
19 | | lognegb 24336 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (-𝑥 ∈ ℝ+
↔ (ℑ‘(log‘𝑥)) = π)) |
20 | 12, 13, 19 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → (-𝑥 ∈ ℝ+ ↔
(ℑ‘(log‘𝑥)) = π)) |
21 | 20 | necon3bbid 2831 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (¬ -𝑥 ∈ ℝ+ ↔
(ℑ‘(log‘𝑥)) ≠ π)) |
22 | 18, 21 | mpbid 222 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ≠ π) |
23 | 22 | necomd 2849 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → π ≠
(ℑ‘(log‘𝑥))) |
24 | | pire 24210 |
. . . . . . . . 9
⊢ π
∈ ℝ |
25 | 24 | a1i 11 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → π ∈
ℝ) |
26 | 16 | simprd 479 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ≤ π) |
27 | 15, 25, 26 | leltned 10190 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → ((ℑ‘(log‘𝑥)) < π ↔ π ≠
(ℑ‘(log‘𝑥)))) |
28 | 23, 27 | mpbird 247 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) < π) |
29 | 24 | renegcli 10342 |
. . . . . . . 8
⊢ -π
∈ ℝ |
30 | 29 | rexri 10097 |
. . . . . . 7
⊢ -π
∈ ℝ* |
31 | 24 | rexri 10097 |
. . . . . . 7
⊢ π
∈ ℝ* |
32 | | elioo2 12216 |
. . . . . . 7
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ*) →
((ℑ‘(log‘𝑥)) ∈ (-π(,)π) ↔
((ℑ‘(log‘𝑥)) ∈ ℝ ∧ -π <
(ℑ‘(log‘𝑥)) ∧ (ℑ‘(log‘𝑥)) < π))) |
33 | 30, 31, 32 | mp2an 708 |
. . . . . 6
⊢
((ℑ‘(log‘𝑥)) ∈ (-π(,)π) ↔
((ℑ‘(log‘𝑥)) ∈ ℝ ∧ -π <
(ℑ‘(log‘𝑥)) ∧ (ℑ‘(log‘𝑥)) < π)) |
34 | 15, 17, 28, 33 | syl3anbrc 1246 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ∈
(-π(,)π)) |
35 | | imf 13853 |
. . . . . 6
⊢
ℑ:ℂ⟶ℝ |
36 | | ffn 6045 |
. . . . . 6
⊢
(ℑ:ℂ⟶ℝ → ℑ Fn
ℂ) |
37 | | elpreima 6337 |
. . . . . 6
⊢ (ℑ
Fn ℂ → ((log‘𝑥) ∈ (◡ℑ “ (-π(,)π)) ↔
((log‘𝑥) ∈
ℂ ∧ (ℑ‘(log‘𝑥)) ∈ (-π(,)π)))) |
38 | 35, 36, 37 | mp2b 10 |
. . . . 5
⊢
((log‘𝑥)
∈ (◡ℑ “
(-π(,)π)) ↔ ((log‘𝑥) ∈ ℂ ∧
(ℑ‘(log‘𝑥)) ∈ (-π(,)π))) |
39 | 14, 34, 38 | sylanbrc 698 |
. . . 4
⊢ (𝑥 ∈ 𝐷 → (log‘𝑥) ∈ (◡ℑ “
(-π(,)π))) |
40 | 10, 39 | mprgbir 2927 |
. . 3
⊢ (log
“ 𝐷) ⊆ (◡ℑ “
(-π(,)π)) |
41 | | df-ioo 12179 |
. . . . . . . . . 10
⊢ (,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
42 | | df-ioc 12180 |
. . . . . . . . . 10
⊢ (,] =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
43 | | idd 24 |
. . . . . . . . . 10
⊢ ((-π
∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (-π
< 𝑤 → -π <
𝑤)) |
44 | | xrltle 11982 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ ℝ*
∧ π ∈ ℝ*) → (𝑤 < π → 𝑤 ≤ π)) |
45 | 41, 42, 43, 44 | ixxssixx 12189 |
. . . . . . . . 9
⊢
(-π(,)π) ⊆ (-π(,]π) |
46 | | imass2 5501 |
. . . . . . . . 9
⊢
((-π(,)π) ⊆ (-π(,]π) → (◡ℑ “ (-π(,)π)) ⊆
(◡ℑ “
(-π(,]π))) |
47 | 45, 46 | ax-mp 5 |
. . . . . . . 8
⊢ (◡ℑ “ (-π(,)π)) ⊆
(◡ℑ “
(-π(,]π)) |
48 | | logrn 24305 |
. . . . . . . 8
⊢ ran log =
(◡ℑ “
(-π(,]π)) |
49 | 47, 48 | sseqtr4i 3638 |
. . . . . . 7
⊢ (◡ℑ “ (-π(,)π)) ⊆ ran
log |
50 | 49 | sseli 3599 |
. . . . . 6
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) → 𝑥 ∈ ran
log) |
51 | | logef 24328 |
. . . . . 6
⊢ (𝑥 ∈ ran log →
(log‘(exp‘𝑥)) =
𝑥) |
52 | 50, 51 | syl 17 |
. . . . 5
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
(log‘(exp‘𝑥)) =
𝑥) |
53 | | elpreima 6337 |
. . . . . . . . . 10
⊢ (ℑ
Fn ℂ → (𝑥 ∈
(◡ℑ “ (-π(,)π))
↔ (𝑥 ∈ ℂ
∧ (ℑ‘𝑥)
∈ (-π(,)π)))) |
54 | 35, 36, 53 | mp2b 10 |
. . . . . . . . 9
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) ↔
(𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π))) |
55 | | efcl 14813 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ →
(exp‘𝑥) ∈
ℂ) |
56 | 55 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (exp‘𝑥) ∈ ℂ) |
57 | 54, 56 | sylbi 207 |
. . . . . . . 8
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
(exp‘𝑥) ∈
ℂ) |
58 | 54 | simplbi 476 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) → 𝑥 ∈
ℂ) |
59 | 58 | imcld 13935 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
(ℑ‘𝑥) ∈
ℝ) |
60 | 54 | simprbi 480 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
(ℑ‘𝑥) ∈
(-π(,)π)) |
61 | | eliooord 12233 |
. . . . . . . . . . . 12
⊢
((ℑ‘𝑥)
∈ (-π(,)π) → (-π < (ℑ‘𝑥) ∧ (ℑ‘𝑥) < π)) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
(-π < (ℑ‘𝑥) ∧ (ℑ‘𝑥) < π)) |
63 | 62 | simprd 479 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
(ℑ‘𝑥) <
π) |
64 | 59, 63 | ltned 10173 |
. . . . . . . . 9
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
(ℑ‘𝑥) ≠
π) |
65 | 52 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → (log‘(exp‘𝑥)) = 𝑥) |
66 | 65 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → (ℑ‘(log‘(exp‘𝑥))) = (ℑ‘𝑥)) |
67 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → (exp‘𝑥) ∈ (-∞(,]0)) |
68 | | mnfxr 10096 |
. . . . . . . . . . . . . . . . . 18
⊢ -∞
∈ ℝ* |
69 | | 0re 10040 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℝ |
70 | | elioc2 12236 |
. . . . . . . . . . . . . . . . . 18
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) →
((exp‘𝑥) ∈
(-∞(,]0) ↔ ((exp‘𝑥) ∈ ℝ ∧ -∞ <
(exp‘𝑥) ∧
(exp‘𝑥) ≤
0))) |
71 | 68, 69, 70 | mp2an 708 |
. . . . . . . . . . . . . . . . 17
⊢
((exp‘𝑥)
∈ (-∞(,]0) ↔ ((exp‘𝑥) ∈ ℝ ∧ -∞ <
(exp‘𝑥) ∧
(exp‘𝑥) ≤
0)) |
72 | 67, 71 | sylib 208 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → ((exp‘𝑥) ∈ ℝ ∧ -∞ <
(exp‘𝑥) ∧
(exp‘𝑥) ≤
0)) |
73 | 72 | simp1d 1073 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → (exp‘𝑥) ∈ ℝ) |
74 | 73 | renegcld 10457 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → -(exp‘𝑥) ∈ ℝ) |
75 | | efne0 14827 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ →
(exp‘𝑥) ≠
0) |
76 | 58, 75 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
(exp‘𝑥) ≠
0) |
77 | 76 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → (exp‘𝑥) ≠ 0) |
78 | 77 | necomd 2849 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → 0 ≠ (exp‘𝑥)) |
79 | | 0red 10041 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → 0 ∈ ℝ) |
80 | 72 | simp3d 1075 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → (exp‘𝑥) ≤ 0) |
81 | 73, 79, 80 | leltned 10190 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → ((exp‘𝑥) < 0 ↔ 0 ≠ (exp‘𝑥))) |
82 | 78, 81 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → (exp‘𝑥) < 0) |
83 | 73 | lt0neg1d 10597 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → ((exp‘𝑥) < 0 ↔ 0 < -(exp‘𝑥))) |
84 | 82, 83 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → 0 < -(exp‘𝑥)) |
85 | 74, 84 | elrpd 11869 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → -(exp‘𝑥) ∈
ℝ+) |
86 | | lognegb 24336 |
. . . . . . . . . . . . . . 15
⊢
(((exp‘𝑥)
∈ ℂ ∧ (exp‘𝑥) ≠ 0) → (-(exp‘𝑥) ∈ ℝ+
↔ (ℑ‘(log‘(exp‘𝑥))) = π)) |
87 | 57, 76, 86 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
(-(exp‘𝑥) ∈
ℝ+ ↔ (ℑ‘(log‘(exp‘𝑥))) = π)) |
88 | 87 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → (-(exp‘𝑥) ∈ ℝ+ ↔
(ℑ‘(log‘(exp‘𝑥))) = π)) |
89 | 85, 88 | mpbid 222 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → (ℑ‘(log‘(exp‘𝑥))) = π) |
90 | 66, 89 | eqtr3d 2658 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → (ℑ‘𝑥) = π) |
91 | 90 | ex 450 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
((exp‘𝑥) ∈
(-∞(,]0) → (ℑ‘𝑥) = π)) |
92 | 91 | necon3ad 2807 |
. . . . . . . . 9
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
((ℑ‘𝑥) ≠
π → ¬ (exp‘𝑥) ∈ (-∞(,]0))) |
93 | 64, 92 | mpd 15 |
. . . . . . . 8
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) → ¬
(exp‘𝑥) ∈
(-∞(,]0)) |
94 | 57, 93 | eldifd 3585 |
. . . . . . 7
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
(exp‘𝑥) ∈
(ℂ ∖ (-∞(,]0))) |
95 | 94, 4 | syl6eleqr 2712 |
. . . . . 6
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
(exp‘𝑥) ∈ 𝐷) |
96 | | funfvima2 6493 |
. . . . . . 7
⊢ ((Fun log
∧ 𝐷 ⊆ dom log)
→ ((exp‘𝑥)
∈ 𝐷 →
(log‘(exp‘𝑥))
∈ (log “ 𝐷))) |
97 | 3, 8, 96 | mp2an 708 |
. . . . . 6
⊢
((exp‘𝑥)
∈ 𝐷 →
(log‘(exp‘𝑥))
∈ (log “ 𝐷)) |
98 | 95, 97 | syl 17 |
. . . . 5
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
(log‘(exp‘𝑥))
∈ (log “ 𝐷)) |
99 | 52, 98 | eqeltrrd 2702 |
. . . 4
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) → 𝑥 ∈ (log “ 𝐷)) |
100 | 99 | ssriv 3607 |
. . 3
⊢ (◡ℑ “ (-π(,)π)) ⊆ (log
“ 𝐷) |
101 | 40, 100 | eqssi 3619 |
. 2
⊢ (log
“ 𝐷) = (◡ℑ “
(-π(,)π)) |
102 | | imcncf 22706 |
. . . 4
⊢ ℑ
∈ (ℂ–cn→ℝ) |
103 | | ssid 3624 |
. . . . 5
⊢ ℂ
⊆ ℂ |
104 | | ax-resscn 9993 |
. . . . 5
⊢ ℝ
⊆ ℂ |
105 | | eqid 2622 |
. . . . . 6
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
106 | 105 | cnfldtop 22587 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) ∈ Top |
107 | 105 | cnfldtopon 22586 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
108 | 107 | toponunii 20721 |
. . . . . . . . 9
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
109 | 108 | restid 16094 |
. . . . . . . 8
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
110 | 106, 109 | ax-mp 5 |
. . . . . . 7
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
111 | 110 | eqcomi 2631 |
. . . . . 6
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
112 | 105 | tgioo2 22606 |
. . . . . 6
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
113 | 105, 111,
112 | cncfcn 22712 |
. . . . 5
⊢ ((ℂ
⊆ ℂ ∧ ℝ ⊆ ℂ) → (ℂ–cn→ℝ) =
((TopOpen‘ℂfld) Cn (topGen‘ran
(,)))) |
114 | 103, 104,
113 | mp2an 708 |
. . . 4
⊢
(ℂ–cn→ℝ) =
((TopOpen‘ℂfld) Cn (topGen‘ran
(,))) |
115 | 102, 114 | eleqtri 2699 |
. . 3
⊢ ℑ
∈ ((TopOpen‘ℂfld) Cn (topGen‘ran
(,))) |
116 | | iooretop 22569 |
. . 3
⊢
(-π(,)π) ∈ (topGen‘ran (,)) |
117 | | cnima 21069 |
. . 3
⊢ ((ℑ
∈ ((TopOpen‘ℂfld) Cn (topGen‘ran (,))) ∧
(-π(,)π) ∈ (topGen‘ran (,))) → (◡ℑ “ (-π(,)π)) ∈
(TopOpen‘ℂfld)) |
118 | 115, 116,
117 | mp2an 708 |
. 2
⊢ (◡ℑ “ (-π(,)π)) ∈
(TopOpen‘ℂfld) |
119 | 101, 118 | eqeltri 2697 |
1
⊢ (log
“ 𝐷) ∈
(TopOpen‘ℂfld) |