| Step | Hyp | Ref
| Expression |
| 1 | | logf1o 26606 |
. . . . . . . 8
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log |
| 2 | | f1orn 6858 |
. . . . . . . . 9
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log ↔ (log Fn (ℂ ∖ {0}) ∧ Fun ◡log)) |
| 3 | 2 | simprbi 496 |
. . . . . . . 8
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → Fun ◡log) |
| 4 | | funcnvres 6644 |
. . . . . . . 8
⊢ (Fun
◡log → ◡(log ↾ (ℂ ∖
(-∞(,]0))) = (◡log ↾ (log
“ (ℂ ∖ (-∞(,]0))))) |
| 5 | 1, 3, 4 | mp2b 10 |
. . . . . . 7
⊢ ◡(log ↾ (ℂ ∖
(-∞(,]0))) = (◡log ↾ (log
“ (ℂ ∖ (-∞(,]0)))) |
| 6 | | df-log 26598 |
. . . . . . . . . 10
⊢ log =
◡(exp ↾ (◡ℑ “
(-π(,]π))) |
| 7 | 6 | cnveqi 5885 |
. . . . . . . . 9
⊢ ◡log = ◡◡(exp ↾ (◡ℑ “
(-π(,]π))) |
| 8 | | relres 6023 |
. . . . . . . . . 10
⊢ Rel (exp
↾ (◡ℑ “
(-π(,]π))) |
| 9 | | dfrel2 6209 |
. . . . . . . . . 10
⊢ (Rel (exp
↾ (◡ℑ “
(-π(,]π))) ↔ ◡◡(exp ↾ (◡ℑ “ (-π(,]π))) = (exp
↾ (◡ℑ “
(-π(,]π)))) |
| 10 | 8, 9 | mpbi 230 |
. . . . . . . . 9
⊢ ◡◡(exp ↾ (◡ℑ “ (-π(,]π))) = (exp
↾ (◡ℑ “
(-π(,]π))) |
| 11 | 7, 10 | eqtri 2765 |
. . . . . . . 8
⊢ ◡log = (exp ↾ (◡ℑ “
(-π(,]π))) |
| 12 | 11 | reseq1i 5993 |
. . . . . . 7
⊢ (◡log ↾ (log “ (ℂ ∖
(-∞(,]0)))) = ((exp ↾ (◡ℑ “ (-π(,]π))) ↾
(log “ (ℂ ∖ (-∞(,]0)))) |
| 13 | | imassrn 6089 |
. . . . . . . . 9
⊢ (log
“ (ℂ ∖ (-∞(,]0))) ⊆ ran log |
| 14 | | logrn 26600 |
. . . . . . . . 9
⊢ ran log =
(◡ℑ “
(-π(,]π)) |
| 15 | 13, 14 | sseqtri 4032 |
. . . . . . . 8
⊢ (log
“ (ℂ ∖ (-∞(,]0))) ⊆ (◡ℑ “
(-π(,]π)) |
| 16 | | resabs1 6024 |
. . . . . . . 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 2769 |
. . . . . 6
⊢ ◡(log ↾ (ℂ ∖
(-∞(,]0))) = (exp ↾ (log “ (ℂ ∖
(-∞(,]0)))) |
| 19 | 18 | imaeq1i 6075 |
. . . . 5
⊢ (◡(log ↾ (ℂ ∖
(-∞(,]0))) “ (0(ball‘(abs ∘ − ))𝑅)) = ((exp ↾ (log “ (ℂ
∖ (-∞(,]0)))) “ (0(ball‘(abs ∘ − ))𝑅)) |
| 20 | | cnxmet 24793 |
. . . . . . . . . . . 12
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
| 21 | | 0cnd 11254 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) → 0
∈ ℂ) |
| 22 | | rpxr 13044 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℝ*) |
| 23 | 22 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) →
𝑅 ∈
ℝ*) |
| 24 | | blssm 24428 |
. . . . . . . . . . . 12
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ 𝑅 ∈
ℝ*) → (0(ball‘(abs ∘ − ))𝑅) ⊆
ℂ) |
| 25 | 20, 21, 23, 24 | mp3an2i 1468 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) →
(0(ball‘(abs ∘ − ))𝑅) ⊆ ℂ) |
| 26 | 25 | sselda 3983 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ ℝ+
∧ 𝑅 < π) ∧
𝑥 ∈ (0(ball‘(abs
∘ − ))𝑅))
→ 𝑥 ∈
ℂ) |
| 27 | 26 | imcld 15234 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ ℝ+
∧ 𝑅 < π) ∧
𝑥 ∈ (0(ball‘(abs
∘ − ))𝑅))
→ (ℑ‘𝑥)
∈ ℝ) |
| 28 | | efopnlem1 26698 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ ℝ+
∧ 𝑅 < π) ∧
𝑥 ∈ (0(ball‘(abs
∘ − ))𝑅))
→ (abs‘(ℑ‘𝑥)) < π) |
| 29 | | pire 26500 |
. . . . . . . . . . . . . 14
⊢ π
∈ ℝ |
| 30 | | abslt 15353 |
. . . . . . . . . . . . . 14
⊢
(((ℑ‘𝑥)
∈ ℝ ∧ π ∈ ℝ) →
((abs‘(ℑ‘𝑥)) < π ↔ (-π <
(ℑ‘𝑥) ∧
(ℑ‘𝑥) <
π))) |
| 31 | 27, 29, 30 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ ℝ+
∧ 𝑅 < π) ∧
𝑥 ∈ (0(ball‘(abs
∘ − ))𝑅))
→ ((abs‘(ℑ‘𝑥)) < π ↔ (-π <
(ℑ‘𝑥) ∧
(ℑ‘𝑥) <
π))) |
| 32 | 28, 31 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ ℝ+
∧ 𝑅 < π) ∧
𝑥 ∈ (0(ball‘(abs
∘ − ))𝑅))
→ (-π < (ℑ‘𝑥) ∧ (ℑ‘𝑥) < π)) |
| 33 | 32 | simpld 494 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ ℝ+
∧ 𝑅 < π) ∧
𝑥 ∈ (0(ball‘(abs
∘ − ))𝑅))
→ -π < (ℑ‘𝑥)) |
| 34 | 32 | simprd 495 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ ℝ+
∧ 𝑅 < π) ∧
𝑥 ∈ (0(ball‘(abs
∘ − ))𝑅))
→ (ℑ‘𝑥)
< π) |
| 35 | 29 | renegcli 11570 |
. . . . . . . . . . . . 13
⊢ -π
∈ ℝ |
| 36 | 35 | rexri 11319 |
. . . . . . . . . . . 12
⊢ -π
∈ ℝ* |
| 37 | 29 | rexri 11319 |
. . . . . . . . . . . 12
⊢ π
∈ ℝ* |
| 38 | | elioo2 13428 |
. . . . . . . . . . . 12
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ*) →
((ℑ‘𝑥) ∈
(-π(,)π) ↔ ((ℑ‘𝑥) ∈ ℝ ∧ -π <
(ℑ‘𝑥) ∧
(ℑ‘𝑥) <
π))) |
| 39 | 36, 37, 38 | mp2an 692 |
. . . . . . . . . . 11
⊢
((ℑ‘𝑥)
∈ (-π(,)π) ↔ ((ℑ‘𝑥) ∈ ℝ ∧ -π <
(ℑ‘𝑥) ∧
(ℑ‘𝑥) <
π)) |
| 40 | 27, 33, 34, 39 | syl3anbrc 1344 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ ℝ+
∧ 𝑅 < π) ∧
𝑥 ∈ (0(ball‘(abs
∘ − ))𝑅))
→ (ℑ‘𝑥)
∈ (-π(,)π)) |
| 41 | | imf 15152 |
. . . . . . . . . . 11
⊢
ℑ:ℂ⟶ℝ |
| 42 | | ffn 6736 |
. . . . . . . . . . 11
⊢
(ℑ:ℂ⟶ℝ → ℑ Fn
ℂ) |
| 43 | | elpreima 7078 |
. . . . . . . . . . 11
⊢ (ℑ
Fn ℂ → (𝑥 ∈
(◡ℑ “ (-π(,)π))
↔ (𝑥 ∈ ℂ
∧ (ℑ‘𝑥)
∈ (-π(,)π)))) |
| 44 | 41, 42, 43 | mp2b 10 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) ↔
(𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π))) |
| 45 | 26, 40, 44 | sylanbrc 583 |
. . . . . . . . 9
⊢ (((𝑅 ∈ ℝ+
∧ 𝑅 < π) ∧
𝑥 ∈ (0(ball‘(abs
∘ − ))𝑅))
→ 𝑥 ∈ (◡ℑ “
(-π(,)π))) |
| 46 | 45 | ex 412 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) →
(𝑥 ∈
(0(ball‘(abs ∘ − ))𝑅) → 𝑥 ∈ (◡ℑ “
(-π(,)π)))) |
| 47 | 46 | ssrdv 3989 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) →
(0(ball‘(abs ∘ − ))𝑅) ⊆ (◡ℑ “
(-π(,)π))) |
| 48 | | df-ima 5698 |
. . . . . . . 8
⊢ (log
“ (ℂ ∖ (-∞(,]0))) = ran (log ↾ (ℂ ∖
(-∞(,]0))) |
| 49 | | eqid 2737 |
. . . . . . . . . 10
⊢ (ℂ
∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0)) |
| 50 | 49 | logf1o2 26692 |
. . . . . . . . 9
⊢ (log
↾ (ℂ ∖ (-∞(,]0))):(ℂ ∖
(-∞(,]0))–1-1-onto→(◡ℑ “
(-π(,)π)) |
| 51 | | f1ofo 6855 |
. . . . . . . . 9
⊢ ((log
↾ (ℂ ∖ (-∞(,]0))):(ℂ ∖
(-∞(,]0))–1-1-onto→(◡ℑ “ (-π(,)π)) → (log
↾ (ℂ ∖ (-∞(,]0))):(ℂ ∖
(-∞(,]0))–onto→(◡ℑ “
(-π(,)π))) |
| 52 | | forn 6823 |
. . . . . . . . 9
⊢ ((log
↾ (ℂ ∖ (-∞(,]0))):(ℂ ∖
(-∞(,]0))–onto→(◡ℑ “ (-π(,)π)) → ran
(log ↾ (ℂ ∖ (-∞(,]0))) = (◡ℑ “
(-π(,)π))) |
| 53 | 50, 51, 52 | mp2b 10 |
. . . . . . . 8
⊢ ran (log
↾ (ℂ ∖ (-∞(,]0))) = (◡ℑ “
(-π(,)π)) |
| 54 | 48, 53 | eqtri 2765 |
. . . . . . 7
⊢ (log
“ (ℂ ∖ (-∞(,]0))) = (◡ℑ “
(-π(,)π)) |
| 55 | 47, 54 | sseqtrrdi 4025 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) →
(0(ball‘(abs ∘ − ))𝑅) ⊆ (log “ (ℂ ∖
(-∞(,]0)))) |
| 56 | | resima2 6034 |
. . . . . 6
⊢
((0(ball‘(abs ∘ − ))𝑅) ⊆ (log “ (ℂ ∖
(-∞(,]0))) → ((exp ↾ (log “ (ℂ ∖
(-∞(,]0)))) “ (0(ball‘(abs ∘ − ))𝑅)) = (exp “
(0(ball‘(abs ∘ − ))𝑅))) |
| 57 | 55, 56 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) →
((exp ↾ (log “ (ℂ ∖ (-∞(,]0)))) “
(0(ball‘(abs ∘ − ))𝑅)) = (exp “ (0(ball‘(abs ∘
− ))𝑅))) |
| 58 | 19, 57 | eqtrid 2789 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) →
(◡(log ↾ (ℂ ∖
(-∞(,]0))) “ (0(ball‘(abs ∘ − ))𝑅)) = (exp “ (0(ball‘(abs ∘
− ))𝑅))) |
| 59 | 49 | logcn 26689 |
. . . . . 6
⊢ (log
↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖
(-∞(,]0))–cn→ℂ) |
| 60 | | difss 4136 |
. . . . . . 7
⊢ (ℂ
∖ (-∞(,]0)) ⊆ ℂ |
| 61 | | ssid 4006 |
. . . . . . 7
⊢ ℂ
⊆ ℂ |
| 62 | | efopn.j |
. . . . . . . 8
⊢ 𝐽 =
(TopOpen‘ℂfld) |
| 63 | | eqid 2737 |
. . . . . . . 8
⊢ (𝐽 ↾t (ℂ
∖ (-∞(,]0))) = (𝐽 ↾t (ℂ ∖
(-∞(,]0))) |
| 64 | 62 | cnfldtopon 24803 |
. . . . . . . . 9
⊢ 𝐽 ∈
(TopOn‘ℂ) |
| 65 | 64 | toponrestid 22927 |
. . . . . . . 8
⊢ 𝐽 = (𝐽 ↾t
ℂ) |
| 66 | 62, 63, 65 | cncfcn 24936 |
. . . . . . 7
⊢
(((ℂ ∖ (-∞(,]0)) ⊆ ℂ ∧ ℂ ⊆
ℂ) → ((ℂ ∖ (-∞(,]0))–cn→ℂ) = ((𝐽 ↾t (ℂ ∖
(-∞(,]0))) Cn 𝐽)) |
| 67 | 60, 61, 66 | mp2an 692 |
. . . . . 6
⊢ ((ℂ
∖ (-∞(,]0))–cn→ℂ) = ((𝐽 ↾t (ℂ ∖
(-∞(,]0))) Cn 𝐽) |
| 68 | 59, 67 | eleqtri 2839 |
. . . . 5
⊢ (log
↾ (ℂ ∖ (-∞(,]0))) ∈ ((𝐽 ↾t (ℂ ∖
(-∞(,]0))) Cn 𝐽) |
| 69 | 62 | cnfldtopn 24802 |
. . . . . . 7
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
| 70 | 69 | blopn 24513 |
. . . . . 6
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ 𝑅 ∈
ℝ*) → (0(ball‘(abs ∘ − ))𝑅) ∈ 𝐽) |
| 71 | 20, 21, 23, 70 | mp3an2i 1468 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) →
(0(ball‘(abs ∘ − ))𝑅) ∈ 𝐽) |
| 72 | | cnima 23273 |
. . . . 5
⊢ (((log
↾ (ℂ ∖ (-∞(,]0))) ∈ ((𝐽 ↾t (ℂ ∖
(-∞(,]0))) Cn 𝐽)
∧ (0(ball‘(abs ∘ − ))𝑅) ∈ 𝐽) → (◡(log ↾ (ℂ ∖
(-∞(,]0))) “ (0(ball‘(abs ∘ − ))𝑅)) ∈ (𝐽 ↾t (ℂ ∖
(-∞(,]0)))) |
| 73 | 68, 71, 72 | sylancr 587 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) →
(◡(log ↾ (ℂ ∖
(-∞(,]0))) “ (0(ball‘(abs ∘ − ))𝑅)) ∈ (𝐽 ↾t (ℂ ∖
(-∞(,]0)))) |
| 74 | 58, 73 | eqeltrrd 2842 |
. . 3
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) →
(exp “ (0(ball‘(abs ∘ − ))𝑅)) ∈ (𝐽 ↾t (ℂ ∖
(-∞(,]0)))) |
| 75 | 62 | cnfldtop 24804 |
. . . 4
⊢ 𝐽 ∈ Top |
| 76 | 49 | logdmopn 26691 |
. . . . 5
⊢ (ℂ
∖ (-∞(,]0)) ∈
(TopOpen‘ℂfld) |
| 77 | 76, 62 | eleqtrri 2840 |
. . . 4
⊢ (ℂ
∖ (-∞(,]0)) ∈ 𝐽 |
| 78 | | restopn2 23185 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ (ℂ
∖ (-∞(,]0)) ∈ 𝐽) → ((exp “ (0(ball‘(abs
∘ − ))𝑅))
∈ (𝐽
↾t (ℂ ∖ (-∞(,]0))) ↔ ((exp “
(0(ball‘(abs ∘ − ))𝑅)) ∈ 𝐽 ∧ (exp “ (0(ball‘(abs
∘ − ))𝑅))
⊆ (ℂ ∖ (-∞(,]0))))) |
| 79 | 75, 77, 78 | mp2an 692 |
. . 3
⊢ ((exp
“ (0(ball‘(abs ∘ − ))𝑅)) ∈ (𝐽 ↾t (ℂ ∖
(-∞(,]0))) ↔ ((exp “ (0(ball‘(abs ∘ −
))𝑅)) ∈ 𝐽 ∧ (exp “
(0(ball‘(abs ∘ − ))𝑅)) ⊆ (ℂ ∖
(-∞(,]0)))) |
| 80 | 74, 79 | sylib 218 |
. 2
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) →
((exp “ (0(ball‘(abs ∘ − ))𝑅)) ∈ 𝐽 ∧ (exp “ (0(ball‘(abs
∘ − ))𝑅))
⊆ (ℂ ∖ (-∞(,]0)))) |
| 81 | 80 | simpld 494 |
1
⊢ ((𝑅 ∈ ℝ+
∧ 𝑅 < π) →
(exp “ (0(ball‘(abs ∘ − ))𝑅)) ∈ 𝐽) |