Step | Hyp | Ref
| Expression |
1 | | logf1o 24115 |
. . . . . . . 8
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log |
2 | | f1orn 6060 |
. . . . . . . . 9
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log ↔ (log Fn (ℂ ∖ {0}) ∧ Fun ◡log)) |
3 | 2 | simprbi 479 |
. . . . . . . 8
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → Fun ◡log) |
4 | | funcnvres 5881 |
. . . . . . . 8
⊢ (Fun
◡log → ◡(log ↾ (ℂ ∖
(-∞(,]0))) = (◡log ↾ (log
“ (ℂ ∖ (-∞(,]0))))) |
5 | 1, 3, 4 | mp2b 10 |
. . . . . . 7
⊢ ◡(log ↾ (ℂ ∖
(-∞(,]0))) = (◡log ↾ (log
“ (ℂ ∖ (-∞(,]0)))) |
6 | | df-log 24107 |
. . . . . . . . . 10
⊢ log =
◡(exp ↾ (◡ℑ “
(-π(,]π))) |
7 | 6 | cnveqi 5219 |
. . . . . . . . 9
⊢ ◡log = ◡◡(exp ↾ (◡ℑ “
(-π(,]π))) |
8 | | relres 5346 |
. . . . . . . . . 10
⊢ Rel (exp
↾ (◡ℑ “
(-π(,]π))) |
9 | | dfrel2 5502 |
. . . . . . . . . 10
⊢ (Rel (exp
↾ (◡ℑ “
(-π(,]π))) ↔ ◡◡(exp ↾ (◡ℑ “ (-π(,]π))) = (exp
↾ (◡ℑ “
(-π(,]π)))) |
10 | 8, 9 | mpbi 219 |
. . . . . . . . 9
⊢ ◡◡(exp ↾ (◡ℑ “ (-π(,]π))) = (exp
↾ (◡ℑ “
(-π(,]π))) |
11 | 7, 10 | eqtri 2632 |
. . . . . . . 8
⊢ ◡log = (exp ↾ (◡ℑ “
(-π(,]π))) |
12 | 11 | reseq1i 5313 |
. . . . . . 7
⊢ (◡log ↾ (log “ (ℂ ∖
(-∞(,]0)))) = ((exp ↾ (◡ℑ “ (-π(,]π))) ↾
(log “ (ℂ ∖ (-∞(,]0)))) |
13 | | imassrn 5396 |
. . . . . . . . 9
⊢ (log
“ (ℂ ∖ (-∞(,]0))) ⊆ ran log |
14 | | logrn 24109 |
. . . . . . . . 9
⊢ ran log =
(◡ℑ “
(-π(,]π)) |
15 | 13, 14 | sseqtri 3600 |
. . . . . . . 8
⊢ (log
“ (ℂ ∖ (-∞(,]0))) ⊆ (◡ℑ “
(-π(,]π)) |
16 | | resabs1 5347 |
. . . . . . . 8
⊢ ((log
“ (ℂ ∖ (-∞(,]0))) ⊆ (◡ℑ “ (-π(,]π)) → ((exp
↾ (◡ℑ “
(-π(,]π))) ↾ (log “ (ℂ ∖ (-∞(,]0)))) = (exp
↾ (log “ (ℂ ∖ (-∞(,]0))))) |
17 | 15, 16 | ax-mp 5 |
. . . . . . 7
⊢ ((exp
↾ (◡ℑ “
(-π(,]π))) ↾ (log “ (ℂ ∖ (-∞(,]0)))) = (exp
↾ (log “ (ℂ ∖ (-∞(,]0)))) |
18 | 5, 12, 17 | 3eqtri 2636 |
. . . . . 6
⊢ ◡(log ↾ (ℂ ∖
(-∞(,]0))) = (exp ↾ (log “ (ℂ ∖
(-∞(,]0)))) |
19 | 18 | imaeq1i 5382 |
. . . . 5
⊢ (◡(log ↾ (ℂ ∖
(-∞(,]0))) “ (0(ball‘(abs ∘ − ))𝑅)) = ((exp ↾ (log “ (ℂ
∖ (-∞(,]0)))) “ (0(ball‘(abs ∘ − ))𝑅)) |
20 | | cnxmet 22386 |
. . . . . . . . . . . . 13
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
21 | 20 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) →
(abs ∘ − ) ∈ (∞Met‘ℂ)) |
22 | | 0cnd 9912 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) → 0
∈ ℂ) |
23 | | rpxr 11716 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℝ*) |
24 | 23 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) →
𝑅 ∈
ℝ*) |
25 | | blssm 22033 |
. . . . . . . . . . . 12
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ 𝑅 ∈
ℝ*) → (0(ball‘(abs ∘ − ))𝑅) ⊆
ℂ) |
26 | 21, 22, 24, 25 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) →
(0(ball‘(abs ∘ − ))𝑅) ⊆ ℂ) |
27 | 26 | sselda 3568 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ ℝ+
∧ 𝑅 < π) ∧
𝑥 ∈ (0(ball‘(abs
∘ − ))𝑅))
→ 𝑥 ∈
ℂ) |
28 | 27 | imcld 13783 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ ℝ+
∧ 𝑅 < π) ∧
𝑥 ∈ (0(ball‘(abs
∘ − ))𝑅))
→ (ℑ‘𝑥)
∈ ℝ) |
29 | | efopnlem1 24202 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ ℝ+
∧ 𝑅 < π) ∧
𝑥 ∈ (0(ball‘(abs
∘ − ))𝑅))
→ (abs‘(ℑ‘𝑥)) < π) |
30 | | pire 24014 |
. . . . . . . . . . . . . 14
⊢ π
∈ ℝ |
31 | | abslt 13902 |
. . . . . . . . . . . . . 14
⊢
(((ℑ‘𝑥)
∈ ℝ ∧ π ∈ ℝ) →
((abs‘(ℑ‘𝑥)) < π ↔ (-π <
(ℑ‘𝑥) ∧
(ℑ‘𝑥) <
π))) |
32 | 28, 30, 31 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ ℝ+
∧ 𝑅 < π) ∧
𝑥 ∈ (0(ball‘(abs
∘ − ))𝑅))
→ ((abs‘(ℑ‘𝑥)) < π ↔ (-π <
(ℑ‘𝑥) ∧
(ℑ‘𝑥) <
π))) |
33 | 29, 32 | mpbid 221 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ ℝ+
∧ 𝑅 < π) ∧
𝑥 ∈ (0(ball‘(abs
∘ − ))𝑅))
→ (-π < (ℑ‘𝑥) ∧ (ℑ‘𝑥) < π)) |
34 | 33 | simpld 474 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ ℝ+
∧ 𝑅 < π) ∧
𝑥 ∈ (0(ball‘(abs
∘ − ))𝑅))
→ -π < (ℑ‘𝑥)) |
35 | 33 | simprd 478 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ ℝ+
∧ 𝑅 < π) ∧
𝑥 ∈ (0(ball‘(abs
∘ − ))𝑅))
→ (ℑ‘𝑥)
< π) |
36 | 30 | renegcli 10221 |
. . . . . . . . . . . . 13
⊢ -π
∈ ℝ |
37 | 36 | rexri 9976 |
. . . . . . . . . . . 12
⊢ -π
∈ ℝ* |
38 | 30 | rexri 9976 |
. . . . . . . . . . . 12
⊢ π
∈ ℝ* |
39 | | elioo2 12087 |
. . . . . . . . . . . 12
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ*) →
((ℑ‘𝑥) ∈
(-π(,)π) ↔ ((ℑ‘𝑥) ∈ ℝ ∧ -π <
(ℑ‘𝑥) ∧
(ℑ‘𝑥) <
π))) |
40 | 37, 38, 39 | mp2an 704 |
. . . . . . . . . . 11
⊢
((ℑ‘𝑥)
∈ (-π(,)π) ↔ ((ℑ‘𝑥) ∈ ℝ ∧ -π <
(ℑ‘𝑥) ∧
(ℑ‘𝑥) <
π)) |
41 | 28, 34, 35, 40 | syl3anbrc 1239 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ ℝ+
∧ 𝑅 < π) ∧
𝑥 ∈ (0(ball‘(abs
∘ − ))𝑅))
→ (ℑ‘𝑥)
∈ (-π(,)π)) |
42 | | imf 13701 |
. . . . . . . . . . 11
⊢
ℑ:ℂ⟶ℝ |
43 | | ffn 5958 |
. . . . . . . . . . 11
⊢
(ℑ:ℂ⟶ℝ → ℑ Fn
ℂ) |
44 | | elpreima 6245 |
. . . . . . . . . . 11
⊢ (ℑ
Fn ℂ → (𝑥 ∈
(◡ℑ “ (-π(,)π))
↔ (𝑥 ∈ ℂ
∧ (ℑ‘𝑥)
∈ (-π(,)π)))) |
45 | 42, 43, 44 | mp2b 10 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) ↔
(𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π))) |
46 | 27, 41, 45 | sylanbrc 695 |
. . . . . . . . 9
⊢ (((𝑅 ∈ ℝ+
∧ 𝑅 < π) ∧
𝑥 ∈ (0(ball‘(abs
∘ − ))𝑅))
→ 𝑥 ∈ (◡ℑ “
(-π(,)π))) |
47 | 46 | ex 449 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) →
(𝑥 ∈
(0(ball‘(abs ∘ − ))𝑅) → 𝑥 ∈ (◡ℑ “
(-π(,)π)))) |
48 | 47 | ssrdv 3574 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) →
(0(ball‘(abs ∘ − ))𝑅) ⊆ (◡ℑ “
(-π(,)π))) |
49 | | df-ima 5051 |
. . . . . . . 8
⊢ (log
“ (ℂ ∖ (-∞(,]0))) = ran (log ↾ (ℂ ∖
(-∞(,]0))) |
50 | | eqid 2610 |
. . . . . . . . . 10
⊢ (ℂ
∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0)) |
51 | 50 | logf1o2 24196 |
. . . . . . . . 9
⊢ (log
↾ (ℂ ∖ (-∞(,]0))):(ℂ ∖
(-∞(,]0))–1-1-onto→(◡ℑ “
(-π(,)π)) |
52 | | f1ofo 6057 |
. . . . . . . . 9
⊢ ((log
↾ (ℂ ∖ (-∞(,]0))):(ℂ ∖
(-∞(,]0))–1-1-onto→(◡ℑ “ (-π(,)π)) → (log
↾ (ℂ ∖ (-∞(,]0))):(ℂ ∖
(-∞(,]0))–onto→(◡ℑ “
(-π(,)π))) |
53 | | forn 6031 |
. . . . . . . . 9
⊢ ((log
↾ (ℂ ∖ (-∞(,]0))):(ℂ ∖
(-∞(,]0))–onto→(◡ℑ “ (-π(,)π)) → ran
(log ↾ (ℂ ∖ (-∞(,]0))) = (◡ℑ “
(-π(,)π))) |
54 | 51, 52, 53 | mp2b 10 |
. . . . . . . 8
⊢ ran (log
↾ (ℂ ∖ (-∞(,]0))) = (◡ℑ “
(-π(,)π)) |
55 | 49, 54 | eqtri 2632 |
. . . . . . 7
⊢ (log
“ (ℂ ∖ (-∞(,]0))) = (◡ℑ “
(-π(,)π)) |
56 | 48, 55 | syl6sseqr 3615 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) →
(0(ball‘(abs ∘ − ))𝑅) ⊆ (log “ (ℂ ∖
(-∞(,]0)))) |
57 | | resima2 5352 |
. . . . . 6
⊢
((0(ball‘(abs ∘ − ))𝑅) ⊆ (log “ (ℂ ∖
(-∞(,]0))) → ((exp ↾ (log “ (ℂ ∖
(-∞(,]0)))) “ (0(ball‘(abs ∘ − ))𝑅)) = (exp “
(0(ball‘(abs ∘ − ))𝑅))) |
58 | 56, 57 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) →
((exp ↾ (log “ (ℂ ∖ (-∞(,]0)))) “
(0(ball‘(abs ∘ − ))𝑅)) = (exp “ (0(ball‘(abs ∘
− ))𝑅))) |
59 | 19, 58 | syl5eq 2656 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) →
(◡(log ↾ (ℂ ∖
(-∞(,]0))) “ (0(ball‘(abs ∘ − ))𝑅)) = (exp “ (0(ball‘(abs ∘
− ))𝑅))) |
60 | 50 | logcn 24193 |
. . . . . 6
⊢ (log
↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖
(-∞(,]0))–cn→ℂ) |
61 | | difss 3699 |
. . . . . . 7
⊢ (ℂ
∖ (-∞(,]0)) ⊆ ℂ |
62 | | ssid 3587 |
. . . . . . 7
⊢ ℂ
⊆ ℂ |
63 | | efopn.j |
. . . . . . . 8
⊢ 𝐽 =
(TopOpen‘ℂfld) |
64 | | eqid 2610 |
. . . . . . . 8
⊢ (𝐽 ↾t (ℂ
∖ (-∞(,]0))) = (𝐽 ↾t (ℂ ∖
(-∞(,]0))) |
65 | 63 | cnfldtop 22397 |
. . . . . . . . . 10
⊢ 𝐽 ∈ Top |
66 | 63 | cnfldtopon 22396 |
. . . . . . . . . . . 12
⊢ 𝐽 ∈
(TopOn‘ℂ) |
67 | 66 | toponunii 20547 |
. . . . . . . . . . 11
⊢ ℂ =
∪ 𝐽 |
68 | 67 | restid 15917 |
. . . . . . . . . 10
⊢ (𝐽 ∈ Top → (𝐽 ↾t ℂ) =
𝐽) |
69 | 65, 68 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝐽 ↾t ℂ) =
𝐽 |
70 | 69 | eqcomi 2619 |
. . . . . . . 8
⊢ 𝐽 = (𝐽 ↾t
ℂ) |
71 | 63, 64, 70 | cncfcn 22520 |
. . . . . . 7
⊢
(((ℂ ∖ (-∞(,]0)) ⊆ ℂ ∧ ℂ ⊆
ℂ) → ((ℂ ∖ (-∞(,]0))–cn→ℂ) = ((𝐽 ↾t (ℂ ∖
(-∞(,]0))) Cn 𝐽)) |
72 | 61, 62, 71 | mp2an 704 |
. . . . . 6
⊢ ((ℂ
∖ (-∞(,]0))–cn→ℂ) = ((𝐽 ↾t (ℂ ∖
(-∞(,]0))) Cn 𝐽) |
73 | 60, 72 | eleqtri 2686 |
. . . . 5
⊢ (log
↾ (ℂ ∖ (-∞(,]0))) ∈ ((𝐽 ↾t (ℂ ∖
(-∞(,]0))) Cn 𝐽) |
74 | 63 | cnfldtopn 22395 |
. . . . . . 7
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
75 | 74 | blopn 22115 |
. . . . . 6
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ 𝑅 ∈
ℝ*) → (0(ball‘(abs ∘ − ))𝑅) ∈ 𝐽) |
76 | 21, 22, 24, 75 | syl3anc 1318 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) →
(0(ball‘(abs ∘ − ))𝑅) ∈ 𝐽) |
77 | | cnima 20879 |
. . . . 5
⊢ (((log
↾ (ℂ ∖ (-∞(,]0))) ∈ ((𝐽 ↾t (ℂ ∖
(-∞(,]0))) Cn 𝐽)
∧ (0(ball‘(abs ∘ − ))𝑅) ∈ 𝐽) → (◡(log ↾ (ℂ ∖
(-∞(,]0))) “ (0(ball‘(abs ∘ − ))𝑅)) ∈ (𝐽 ↾t (ℂ ∖
(-∞(,]0)))) |
78 | 73, 76, 77 | sylancr 694 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) →
(◡(log ↾ (ℂ ∖
(-∞(,]0))) “ (0(ball‘(abs ∘ − ))𝑅)) ∈ (𝐽 ↾t (ℂ ∖
(-∞(,]0)))) |
79 | 59, 78 | eqeltrrd 2689 |
. . 3
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) →
(exp “ (0(ball‘(abs ∘ − ))𝑅)) ∈ (𝐽 ↾t (ℂ ∖
(-∞(,]0)))) |
80 | 50 | logdmopn 24195 |
. . . . 5
⊢ (ℂ
∖ (-∞(,]0)) ∈
(TopOpen‘ℂfld) |
81 | 80, 63 | eleqtrri 2687 |
. . . 4
⊢ (ℂ
∖ (-∞(,]0)) ∈ 𝐽 |
82 | | restopn2 20791 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ (ℂ
∖ (-∞(,]0)) ∈ 𝐽) → ((exp “ (0(ball‘(abs
∘ − ))𝑅))
∈ (𝐽
↾t (ℂ ∖ (-∞(,]0))) ↔ ((exp “
(0(ball‘(abs ∘ − ))𝑅)) ∈ 𝐽 ∧ (exp “ (0(ball‘(abs
∘ − ))𝑅))
⊆ (ℂ ∖ (-∞(,]0))))) |
83 | 65, 81, 82 | mp2an 704 |
. . 3
⊢ ((exp
“ (0(ball‘(abs ∘ − ))𝑅)) ∈ (𝐽 ↾t (ℂ ∖
(-∞(,]0))) ↔ ((exp “ (0(ball‘(abs ∘ −
))𝑅)) ∈ 𝐽 ∧ (exp “
(0(ball‘(abs ∘ − ))𝑅)) ⊆ (ℂ ∖
(-∞(,]0)))) |
84 | 79, 83 | sylib 207 |
. 2
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) →
((exp “ (0(ball‘(abs ∘ − ))𝑅)) ∈ 𝐽 ∧ (exp “ (0(ball‘(abs
∘ − ))𝑅))
⊆ (ℂ ∖ (-∞(,]0)))) |
85 | 84 | simpld 474 |
1
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) →
(exp “ (0(ball‘(abs ∘ − ))𝑅)) ∈ 𝐽) |