| Step | Hyp | Ref
| Expression |
| 1 | | logf1o 26606 |
. . . . . 6
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log |
| 2 | | f1ofun 6850 |
. . . . . 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 26684 |
. . . . . 6
⊢ 𝐷 ⊆ (ℂ ∖
{0}) |
| 6 | | f1odm 6852 |
. . . . . . 7
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → dom log = (ℂ ∖ {0})) |
| 7 | 1, 6 | ax-mp 5 |
. . . . . 6
⊢ dom log =
(ℂ ∖ {0}) |
| 8 | 5, 7 | sseqtrri 4033 |
. . . . 5
⊢ 𝐷 ⊆ dom
log |
| 9 | | funimass4 6973 |
. . . . 5
⊢ ((Fun log
∧ 𝐷 ⊆ dom log)
→ ((log “ 𝐷)
⊆ (◡ℑ “
(-π(,)π)) ↔ ∀𝑥 ∈ 𝐷 (log‘𝑥) ∈ (◡ℑ “
(-π(,)π)))) |
| 10 | 3, 8, 9 | mp2an 692 |
. . . 4
⊢ ((log
“ 𝐷) ⊆ (◡ℑ “ (-π(,)π)) ↔
∀𝑥 ∈ 𝐷 (log‘𝑥) ∈ (◡ℑ “
(-π(,)π))) |
| 11 | 4 | ellogdm 26681 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ ℂ ∧ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ+))) |
| 12 | 11 | simplbi 497 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ) |
| 13 | 4 | logdmn0 26682 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → 𝑥 ≠ 0) |
| 14 | 12, 13 | logcld 26612 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (log‘𝑥) ∈ ℂ) |
| 15 | 14 | imcld 15234 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ∈
ℝ) |
| 16 | 12, 13 | logimcld 26613 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (-π <
(ℑ‘(log‘𝑥)) ∧ (ℑ‘(log‘𝑥)) ≤ π)) |
| 17 | 16 | simpld 494 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → -π <
(ℑ‘(log‘𝑥))) |
| 18 | | pire 26500 |
. . . . . . . 8
⊢ π
∈ ℝ |
| 19 | 18 | a1i 11 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → π ∈
ℝ) |
| 20 | 16 | simprd 495 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ≤ π) |
| 21 | 4 | logdmnrp 26683 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → ¬ -𝑥 ∈ ℝ+) |
| 22 | | lognegb 26632 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (-𝑥 ∈ ℝ+
↔ (ℑ‘(log‘𝑥)) = π)) |
| 23 | 12, 13, 22 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → (-𝑥 ∈ ℝ+ ↔
(ℑ‘(log‘𝑥)) = π)) |
| 24 | 23 | necon3bbid 2978 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (¬ -𝑥 ∈ ℝ+ ↔
(ℑ‘(log‘𝑥)) ≠ π)) |
| 25 | 21, 24 | mpbid 232 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ≠ π) |
| 26 | 25 | necomd 2996 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → π ≠
(ℑ‘(log‘𝑥))) |
| 27 | 15, 19, 20, 26 | leneltd 11415 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) < π) |
| 28 | 18 | renegcli 11570 |
. . . . . . . 8
⊢ -π
∈ ℝ |
| 29 | 28 | rexri 11319 |
. . . . . . 7
⊢ -π
∈ ℝ* |
| 30 | 18 | rexri 11319 |
. . . . . . 7
⊢ π
∈ ℝ* |
| 31 | | elioo2 13428 |
. . . . . . 7
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ*) →
((ℑ‘(log‘𝑥)) ∈ (-π(,)π) ↔
((ℑ‘(log‘𝑥)) ∈ ℝ ∧ -π <
(ℑ‘(log‘𝑥)) ∧ (ℑ‘(log‘𝑥)) < π))) |
| 32 | 29, 30, 31 | mp2an 692 |
. . . . . 6
⊢
((ℑ‘(log‘𝑥)) ∈ (-π(,)π) ↔
((ℑ‘(log‘𝑥)) ∈ ℝ ∧ -π <
(ℑ‘(log‘𝑥)) ∧ (ℑ‘(log‘𝑥)) < π)) |
| 33 | 15, 17, 27, 32 | syl3anbrc 1344 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ∈
(-π(,)π)) |
| 34 | | imf 15152 |
. . . . . 6
⊢
ℑ:ℂ⟶ℝ |
| 35 | | ffn 6736 |
. . . . . 6
⊢
(ℑ:ℂ⟶ℝ → ℑ Fn
ℂ) |
| 36 | | elpreima 7078 |
. . . . . 6
⊢ (ℑ
Fn ℂ → ((log‘𝑥) ∈ (◡ℑ “ (-π(,)π)) ↔
((log‘𝑥) ∈
ℂ ∧ (ℑ‘(log‘𝑥)) ∈ (-π(,)π)))) |
| 37 | 34, 35, 36 | mp2b 10 |
. . . . 5
⊢
((log‘𝑥)
∈ (◡ℑ “
(-π(,)π)) ↔ ((log‘𝑥) ∈ ℂ ∧
(ℑ‘(log‘𝑥)) ∈ (-π(,)π))) |
| 38 | 14, 33, 37 | sylanbrc 583 |
. . . 4
⊢ (𝑥 ∈ 𝐷 → (log‘𝑥) ∈ (◡ℑ “
(-π(,)π))) |
| 39 | 10, 38 | mprgbir 3068 |
. . 3
⊢ (log
“ 𝐷) ⊆ (◡ℑ “
(-π(,)π)) |
| 40 | | df-ioo 13391 |
. . . . . . . . . 10
⊢ (,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
| 41 | | df-ioc 13392 |
. . . . . . . . . 10
⊢ (,] =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
| 42 | | idd 24 |
. . . . . . . . . 10
⊢ ((-π
∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (-π
< 𝑤 → -π <
𝑤)) |
| 43 | | xrltle 13191 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ ℝ*
∧ π ∈ ℝ*) → (𝑤 < π → 𝑤 ≤ π)) |
| 44 | 40, 41, 42, 43 | ixxssixx 13401 |
. . . . . . . . 9
⊢
(-π(,)π) ⊆ (-π(,]π) |
| 45 | | imass2 6120 |
. . . . . . . . 9
⊢
((-π(,)π) ⊆ (-π(,]π) → (◡ℑ “ (-π(,)π)) ⊆
(◡ℑ “
(-π(,]π))) |
| 46 | 44, 45 | ax-mp 5 |
. . . . . . . 8
⊢ (◡ℑ “ (-π(,)π)) ⊆
(◡ℑ “
(-π(,]π)) |
| 47 | | logrn 26600 |
. . . . . . . 8
⊢ ran log =
(◡ℑ “
(-π(,]π)) |
| 48 | 46, 47 | sseqtrri 4033 |
. . . . . . 7
⊢ (◡ℑ “ (-π(,)π)) ⊆ ran
log |
| 49 | 48 | sseli 3979 |
. . . . . 6
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) → 𝑥 ∈ ran
log) |
| 50 | | logef 26623 |
. . . . . 6
⊢ (𝑥 ∈ ran log →
(log‘(exp‘𝑥)) =
𝑥) |
| 51 | 49, 50 | syl 17 |
. . . . 5
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
(log‘(exp‘𝑥)) =
𝑥) |
| 52 | | elpreima 7078 |
. . . . . . . . . 10
⊢ (ℑ
Fn ℂ → (𝑥 ∈
(◡ℑ “ (-π(,)π))
↔ (𝑥 ∈ ℂ
∧ (ℑ‘𝑥)
∈ (-π(,)π)))) |
| 53 | 34, 35, 52 | mp2b 10 |
. . . . . . . . 9
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) ↔
(𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π))) |
| 54 | | efcl 16118 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ →
(exp‘𝑥) ∈
ℂ) |
| 55 | 54 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (exp‘𝑥) ∈ ℂ) |
| 56 | 53, 55 | sylbi 217 |
. . . . . . . 8
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
(exp‘𝑥) ∈
ℂ) |
| 57 | 53 | simplbi 497 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) → 𝑥 ∈
ℂ) |
| 58 | 57 | imcld 15234 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
(ℑ‘𝑥) ∈
ℝ) |
| 59 | | eliooord 13446 |
. . . . . . . . . . . 12
⊢
((ℑ‘𝑥)
∈ (-π(,)π) → (-π < (ℑ‘𝑥) ∧ (ℑ‘𝑥) < π)) |
| 60 | 53, 59 | simplbiim 504 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
(-π < (ℑ‘𝑥) ∧ (ℑ‘𝑥) < π)) |
| 61 | 60 | simprd 495 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
(ℑ‘𝑥) <
π) |
| 62 | 58, 61 | ltned 11397 |
. . . . . . . . 9
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
(ℑ‘𝑥) ≠
π) |
| 63 | 51 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → (log‘(exp‘𝑥)) = 𝑥) |
| 64 | 63 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → (ℑ‘(log‘(exp‘𝑥))) = (ℑ‘𝑥)) |
| 65 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → (exp‘𝑥) ∈ (-∞(,]0)) |
| 66 | | mnfxr 11318 |
. . . . . . . . . . . . . . . . 17
⊢ -∞
∈ ℝ* |
| 67 | | 0re 11263 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
ℝ |
| 68 | | elioc2 13450 |
. . . . . . . . . . . . . . . . 17
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) →
((exp‘𝑥) ∈
(-∞(,]0) ↔ ((exp‘𝑥) ∈ ℝ ∧ -∞ <
(exp‘𝑥) ∧
(exp‘𝑥) ≤
0))) |
| 69 | 66, 67, 68 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢
((exp‘𝑥)
∈ (-∞(,]0) ↔ ((exp‘𝑥) ∈ ℝ ∧ -∞ <
(exp‘𝑥) ∧
(exp‘𝑥) ≤
0)) |
| 70 | 65, 69 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → ((exp‘𝑥) ∈ ℝ ∧ -∞ <
(exp‘𝑥) ∧
(exp‘𝑥) ≤
0)) |
| 71 | 70 | simp1d 1143 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → (exp‘𝑥) ∈ ℝ) |
| 72 | | 0red 11264 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → 0 ∈ ℝ) |
| 73 | 70 | simp3d 1145 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → (exp‘𝑥) ≤ 0) |
| 74 | | efne0 16133 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ →
(exp‘𝑥) ≠
0) |
| 75 | 57, 74 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
(exp‘𝑥) ≠
0) |
| 76 | 75 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → (exp‘𝑥) ≠ 0) |
| 77 | 76 | necomd 2996 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → 0 ≠ (exp‘𝑥)) |
| 78 | 71, 72, 73, 77 | leneltd 11415 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → (exp‘𝑥) < 0) |
| 79 | 71, 78 | negelrpd 13069 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → -(exp‘𝑥) ∈
ℝ+) |
| 80 | | lognegb 26632 |
. . . . . . . . . . . . . . 15
⊢
(((exp‘𝑥)
∈ ℂ ∧ (exp‘𝑥) ≠ 0) → (-(exp‘𝑥) ∈ ℝ+
↔ (ℑ‘(log‘(exp‘𝑥))) = π)) |
| 81 | 56, 75, 80 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
(-(exp‘𝑥) ∈
ℝ+ ↔ (ℑ‘(log‘(exp‘𝑥))) = π)) |
| 82 | 81 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → (-(exp‘𝑥) ∈ ℝ+ ↔
(ℑ‘(log‘(exp‘𝑥))) = π)) |
| 83 | 79, 82 | mpbid 232 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → (ℑ‘(log‘(exp‘𝑥))) = π) |
| 84 | 64, 83 | eqtr3d 2779 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (◡ℑ “ (-π(,)π)) ∧
(exp‘𝑥) ∈
(-∞(,]0)) → (ℑ‘𝑥) = π) |
| 85 | 84 | ex 412 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
((exp‘𝑥) ∈
(-∞(,]0) → (ℑ‘𝑥) = π)) |
| 86 | 85 | necon3ad 2953 |
. . . . . . . . 9
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
((ℑ‘𝑥) ≠
π → ¬ (exp‘𝑥) ∈ (-∞(,]0))) |
| 87 | 62, 86 | mpd 15 |
. . . . . . . 8
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) → ¬
(exp‘𝑥) ∈
(-∞(,]0)) |
| 88 | 56, 87 | eldifd 3962 |
. . . . . . 7
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
(exp‘𝑥) ∈
(ℂ ∖ (-∞(,]0))) |
| 89 | 88, 4 | eleqtrrdi 2852 |
. . . . . 6
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
(exp‘𝑥) ∈ 𝐷) |
| 90 | | funfvima2 7251 |
. . . . . . 7
⊢ ((Fun log
∧ 𝐷 ⊆ dom log)
→ ((exp‘𝑥)
∈ 𝐷 →
(log‘(exp‘𝑥))
∈ (log “ 𝐷))) |
| 91 | 3, 8, 90 | mp2an 692 |
. . . . . 6
⊢
((exp‘𝑥)
∈ 𝐷 →
(log‘(exp‘𝑥))
∈ (log “ 𝐷)) |
| 92 | 89, 91 | syl 17 |
. . . . 5
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) →
(log‘(exp‘𝑥))
∈ (log “ 𝐷)) |
| 93 | 51, 92 | eqeltrrd 2842 |
. . . 4
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) → 𝑥 ∈ (log “ 𝐷)) |
| 94 | 93 | ssriv 3987 |
. . 3
⊢ (◡ℑ “ (-π(,)π)) ⊆ (log
“ 𝐷) |
| 95 | 39, 94 | eqssi 4000 |
. 2
⊢ (log
“ 𝐷) = (◡ℑ “
(-π(,)π)) |
| 96 | | imcncf 24929 |
. . . 4
⊢ ℑ
∈ (ℂ–cn→ℝ) |
| 97 | | ssid 4006 |
. . . . 5
⊢ ℂ
⊆ ℂ |
| 98 | | ax-resscn 11212 |
. . . . 5
⊢ ℝ
⊆ ℂ |
| 99 | | eqid 2737 |
. . . . . 6
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 100 | 99 | cnfldtopon 24803 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
| 101 | 100 | toponrestid 22927 |
. . . . . 6
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
| 102 | | tgioo4 24826 |
. . . . . 6
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
| 103 | 99, 101, 102 | cncfcn 24936 |
. . . . 5
⊢ ((ℂ
⊆ ℂ ∧ ℝ ⊆ ℂ) → (ℂ–cn→ℝ) =
((TopOpen‘ℂfld) Cn (topGen‘ran
(,)))) |
| 104 | 97, 98, 103 | mp2an 692 |
. . . 4
⊢
(ℂ–cn→ℝ) =
((TopOpen‘ℂfld) Cn (topGen‘ran
(,))) |
| 105 | 96, 104 | eleqtri 2839 |
. . 3
⊢ ℑ
∈ ((TopOpen‘ℂfld) Cn (topGen‘ran
(,))) |
| 106 | | iooretop 24786 |
. . 3
⊢
(-π(,)π) ∈ (topGen‘ran (,)) |
| 107 | | cnima 23273 |
. . 3
⊢ ((ℑ
∈ ((TopOpen‘ℂfld) Cn (topGen‘ran (,))) ∧
(-π(,)π) ∈ (topGen‘ran (,))) → (◡ℑ “ (-π(,)π)) ∈
(TopOpen‘ℂfld)) |
| 108 | 105, 106,
107 | mp2an 692 |
. 2
⊢ (◡ℑ “ (-π(,)π)) ∈
(TopOpen‘ℂfld) |
| 109 | 95, 108 | eqeltri 2837 |
1
⊢ (log
“ 𝐷) ∈
(TopOpen‘ℂfld) |