Step |
Hyp |
Ref |
Expression |
1 |
|
logcn.d |
⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) ) |
2 |
|
logf1o |
⊢ log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log |
3 |
|
f1ofun |
⊢ ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → Fun log ) |
4 |
2 3
|
ax-mp |
⊢ Fun log |
5 |
1
|
logdmss |
⊢ 𝐷 ⊆ ( ℂ ∖ { 0 } ) |
6 |
|
f1odm |
⊢ ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → dom log = ( ℂ ∖ { 0 } ) ) |
7 |
2 6
|
ax-mp |
⊢ dom log = ( ℂ ∖ { 0 } ) |
8 |
5 7
|
sseqtrri |
⊢ 𝐷 ⊆ dom log |
9 |
|
funimass4 |
⊢ ( ( Fun log ∧ 𝐷 ⊆ dom log ) → ( ( log “ 𝐷 ) ⊆ ( ◡ ℑ “ ( - π (,) π ) ) ↔ ∀ 𝑥 ∈ 𝐷 ( log ‘ 𝑥 ) ∈ ( ◡ ℑ “ ( - π (,) π ) ) ) ) |
10 |
4 8 9
|
mp2an |
⊢ ( ( log “ 𝐷 ) ⊆ ( ◡ ℑ “ ( - π (,) π ) ) ↔ ∀ 𝑥 ∈ 𝐷 ( log ‘ 𝑥 ) ∈ ( ◡ ℑ “ ( - π (,) π ) ) ) |
11 |
1
|
ellogdm |
⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ+ ) ) ) |
12 |
11
|
simplbi |
⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ ) |
13 |
1
|
logdmn0 |
⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ≠ 0 ) |
14 |
12 13
|
logcld |
⊢ ( 𝑥 ∈ 𝐷 → ( log ‘ 𝑥 ) ∈ ℂ ) |
15 |
14
|
imcld |
⊢ ( 𝑥 ∈ 𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ℝ ) |
16 |
12 13
|
logimcld |
⊢ ( 𝑥 ∈ 𝐷 → ( - π < ( ℑ ‘ ( log ‘ 𝑥 ) ) ∧ ( ℑ ‘ ( log ‘ 𝑥 ) ) ≤ π ) ) |
17 |
16
|
simpld |
⊢ ( 𝑥 ∈ 𝐷 → - π < ( ℑ ‘ ( log ‘ 𝑥 ) ) ) |
18 |
|
pire |
⊢ π ∈ ℝ |
19 |
18
|
a1i |
⊢ ( 𝑥 ∈ 𝐷 → π ∈ ℝ ) |
20 |
16
|
simprd |
⊢ ( 𝑥 ∈ 𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) ≤ π ) |
21 |
1
|
logdmnrp |
⊢ ( 𝑥 ∈ 𝐷 → ¬ - 𝑥 ∈ ℝ+ ) |
22 |
|
lognegb |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( - 𝑥 ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ 𝑥 ) ) = π ) ) |
23 |
12 13 22
|
syl2anc |
⊢ ( 𝑥 ∈ 𝐷 → ( - 𝑥 ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ 𝑥 ) ) = π ) ) |
24 |
23
|
necon3bbid |
⊢ ( 𝑥 ∈ 𝐷 → ( ¬ - 𝑥 ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ 𝑥 ) ) ≠ π ) ) |
25 |
21 24
|
mpbid |
⊢ ( 𝑥 ∈ 𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) ≠ π ) |
26 |
25
|
necomd |
⊢ ( 𝑥 ∈ 𝐷 → π ≠ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) |
27 |
15 19 20 26
|
leneltd |
⊢ ( 𝑥 ∈ 𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) < π ) |
28 |
18
|
renegcli |
⊢ - π ∈ ℝ |
29 |
28
|
rexri |
⊢ - π ∈ ℝ* |
30 |
18
|
rexri |
⊢ π ∈ ℝ* |
31 |
|
elioo2 |
⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ* ) → ( ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ( - π (,) π ) ↔ ( ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ℝ ∧ - π < ( ℑ ‘ ( log ‘ 𝑥 ) ) ∧ ( ℑ ‘ ( log ‘ 𝑥 ) ) < π ) ) ) |
32 |
29 30 31
|
mp2an |
⊢ ( ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ( - π (,) π ) ↔ ( ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ℝ ∧ - π < ( ℑ ‘ ( log ‘ 𝑥 ) ) ∧ ( ℑ ‘ ( log ‘ 𝑥 ) ) < π ) ) |
33 |
15 17 27 32
|
syl3anbrc |
⊢ ( 𝑥 ∈ 𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ( - π (,) π ) ) |
34 |
|
imf |
⊢ ℑ : ℂ ⟶ ℝ |
35 |
|
ffn |
⊢ ( ℑ : ℂ ⟶ ℝ → ℑ Fn ℂ ) |
36 |
|
elpreima |
⊢ ( ℑ Fn ℂ → ( ( log ‘ 𝑥 ) ∈ ( ◡ ℑ “ ( - π (,) π ) ) ↔ ( ( log ‘ 𝑥 ) ∈ ℂ ∧ ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ( - π (,) π ) ) ) ) |
37 |
34 35 36
|
mp2b |
⊢ ( ( log ‘ 𝑥 ) ∈ ( ◡ ℑ “ ( - π (,) π ) ) ↔ ( ( log ‘ 𝑥 ) ∈ ℂ ∧ ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ( - π (,) π ) ) ) |
38 |
14 33 37
|
sylanbrc |
⊢ ( 𝑥 ∈ 𝐷 → ( log ‘ 𝑥 ) ∈ ( ◡ ℑ “ ( - π (,) π ) ) ) |
39 |
10 38
|
mprgbir |
⊢ ( log “ 𝐷 ) ⊆ ( ◡ ℑ “ ( - π (,) π ) ) |
40 |
|
df-ioo |
⊢ (,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) } ) |
41 |
|
df-ioc |
⊢ (,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦 ) } ) |
42 |
|
idd |
⊢ ( ( - π ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( - π < 𝑤 → - π < 𝑤 ) ) |
43 |
|
xrltle |
⊢ ( ( 𝑤 ∈ ℝ* ∧ π ∈ ℝ* ) → ( 𝑤 < π → 𝑤 ≤ π ) ) |
44 |
40 41 42 43
|
ixxssixx |
⊢ ( - π (,) π ) ⊆ ( - π (,] π ) |
45 |
|
imass2 |
⊢ ( ( - π (,) π ) ⊆ ( - π (,] π ) → ( ◡ ℑ “ ( - π (,) π ) ) ⊆ ( ◡ ℑ “ ( - π (,] π ) ) ) |
46 |
44 45
|
ax-mp |
⊢ ( ◡ ℑ “ ( - π (,) π ) ) ⊆ ( ◡ ℑ “ ( - π (,] π ) ) |
47 |
|
logrn |
⊢ ran log = ( ◡ ℑ “ ( - π (,] π ) ) |
48 |
46 47
|
sseqtrri |
⊢ ( ◡ ℑ “ ( - π (,) π ) ) ⊆ ran log |
49 |
48
|
sseli |
⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → 𝑥 ∈ ran log ) |
50 |
|
logef |
⊢ ( 𝑥 ∈ ran log → ( log ‘ ( exp ‘ 𝑥 ) ) = 𝑥 ) |
51 |
49 50
|
syl |
⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → ( log ‘ ( exp ‘ 𝑥 ) ) = 𝑥 ) |
52 |
|
elpreima |
⊢ ( ℑ Fn ℂ → ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ) ) |
53 |
34 35 52
|
mp2b |
⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ) |
54 |
|
efcl |
⊢ ( 𝑥 ∈ ℂ → ( exp ‘ 𝑥 ) ∈ ℂ ) |
55 |
54
|
adantr |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( exp ‘ 𝑥 ) ∈ ℂ ) |
56 |
53 55
|
sylbi |
⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → ( exp ‘ 𝑥 ) ∈ ℂ ) |
57 |
53
|
simplbi |
⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → 𝑥 ∈ ℂ ) |
58 |
57
|
imcld |
⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → ( ℑ ‘ 𝑥 ) ∈ ℝ ) |
59 |
|
eliooord |
⊢ ( ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) → ( - π < ( ℑ ‘ 𝑥 ) ∧ ( ℑ ‘ 𝑥 ) < π ) ) |
60 |
53 59
|
simplbiim |
⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → ( - π < ( ℑ ‘ 𝑥 ) ∧ ( ℑ ‘ 𝑥 ) < π ) ) |
61 |
60
|
simprd |
⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → ( ℑ ‘ 𝑥 ) < π ) |
62 |
58 61
|
ltned |
⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → ( ℑ ‘ 𝑥 ) ≠ π ) |
63 |
51
|
adantr |
⊢ ( ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( log ‘ ( exp ‘ 𝑥 ) ) = 𝑥 ) |
64 |
63
|
fveq2d |
⊢ ( ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( ℑ ‘ ( log ‘ ( exp ‘ 𝑥 ) ) ) = ( ℑ ‘ 𝑥 ) ) |
65 |
|
simpr |
⊢ ( ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) |
66 |
|
mnfxr |
⊢ -∞ ∈ ℝ* |
67 |
|
0re |
⊢ 0 ∈ ℝ |
68 |
|
elioc2 |
⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ ) → ( ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ↔ ( ( exp ‘ 𝑥 ) ∈ ℝ ∧ -∞ < ( exp ‘ 𝑥 ) ∧ ( exp ‘ 𝑥 ) ≤ 0 ) ) ) |
69 |
66 67 68
|
mp2an |
⊢ ( ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ↔ ( ( exp ‘ 𝑥 ) ∈ ℝ ∧ -∞ < ( exp ‘ 𝑥 ) ∧ ( exp ‘ 𝑥 ) ≤ 0 ) ) |
70 |
65 69
|
sylib |
⊢ ( ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( ( exp ‘ 𝑥 ) ∈ ℝ ∧ -∞ < ( exp ‘ 𝑥 ) ∧ ( exp ‘ 𝑥 ) ≤ 0 ) ) |
71 |
70
|
simp1d |
⊢ ( ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( exp ‘ 𝑥 ) ∈ ℝ ) |
72 |
|
0red |
⊢ ( ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → 0 ∈ ℝ ) |
73 |
70
|
simp3d |
⊢ ( ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( exp ‘ 𝑥 ) ≤ 0 ) |
74 |
|
efne0 |
⊢ ( 𝑥 ∈ ℂ → ( exp ‘ 𝑥 ) ≠ 0 ) |
75 |
57 74
|
syl |
⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → ( exp ‘ 𝑥 ) ≠ 0 ) |
76 |
75
|
adantr |
⊢ ( ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( exp ‘ 𝑥 ) ≠ 0 ) |
77 |
76
|
necomd |
⊢ ( ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → 0 ≠ ( exp ‘ 𝑥 ) ) |
78 |
71 72 73 77
|
leneltd |
⊢ ( ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( exp ‘ 𝑥 ) < 0 ) |
79 |
71 78
|
negelrpd |
⊢ ( ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → - ( exp ‘ 𝑥 ) ∈ ℝ+ ) |
80 |
|
lognegb |
⊢ ( ( ( exp ‘ 𝑥 ) ∈ ℂ ∧ ( exp ‘ 𝑥 ) ≠ 0 ) → ( - ( exp ‘ 𝑥 ) ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ ( exp ‘ 𝑥 ) ) ) = π ) ) |
81 |
56 75 80
|
syl2anc |
⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → ( - ( exp ‘ 𝑥 ) ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ ( exp ‘ 𝑥 ) ) ) = π ) ) |
82 |
81
|
adantr |
⊢ ( ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( - ( exp ‘ 𝑥 ) ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ ( exp ‘ 𝑥 ) ) ) = π ) ) |
83 |
79 82
|
mpbid |
⊢ ( ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( ℑ ‘ ( log ‘ ( exp ‘ 𝑥 ) ) ) = π ) |
84 |
64 83
|
eqtr3d |
⊢ ( ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) → ( ℑ ‘ 𝑥 ) = π ) |
85 |
84
|
ex |
⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → ( ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) → ( ℑ ‘ 𝑥 ) = π ) ) |
86 |
85
|
necon3ad |
⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → ( ( ℑ ‘ 𝑥 ) ≠ π → ¬ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) ) |
87 |
62 86
|
mpd |
⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → ¬ ( exp ‘ 𝑥 ) ∈ ( -∞ (,] 0 ) ) |
88 |
56 87
|
eldifd |
⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → ( exp ‘ 𝑥 ) ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ) |
89 |
88 1
|
eleqtrrdi |
⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → ( exp ‘ 𝑥 ) ∈ 𝐷 ) |
90 |
|
funfvima2 |
⊢ ( ( Fun log ∧ 𝐷 ⊆ dom log ) → ( ( exp ‘ 𝑥 ) ∈ 𝐷 → ( log ‘ ( exp ‘ 𝑥 ) ) ∈ ( log “ 𝐷 ) ) ) |
91 |
4 8 90
|
mp2an |
⊢ ( ( exp ‘ 𝑥 ) ∈ 𝐷 → ( log ‘ ( exp ‘ 𝑥 ) ) ∈ ( log “ 𝐷 ) ) |
92 |
89 91
|
syl |
⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → ( log ‘ ( exp ‘ 𝑥 ) ) ∈ ( log “ 𝐷 ) ) |
93 |
51 92
|
eqeltrrd |
⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → 𝑥 ∈ ( log “ 𝐷 ) ) |
94 |
93
|
ssriv |
⊢ ( ◡ ℑ “ ( - π (,) π ) ) ⊆ ( log “ 𝐷 ) |
95 |
39 94
|
eqssi |
⊢ ( log “ 𝐷 ) = ( ◡ ℑ “ ( - π (,) π ) ) |
96 |
|
imcncf |
⊢ ℑ ∈ ( ℂ –cn→ ℝ ) |
97 |
|
ssid |
⊢ ℂ ⊆ ℂ |
98 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
99 |
|
eqid |
⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) |
100 |
99
|
cnfldtopon |
⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) |
101 |
100
|
toponrestid |
⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) |
102 |
99
|
tgioo2 |
⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) |
103 |
99 101 102
|
cncfcn |
⊢ ( ( ℂ ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( ℂ –cn→ ℝ ) = ( ( TopOpen ‘ ℂfld ) Cn ( topGen ‘ ran (,) ) ) ) |
104 |
97 98 103
|
mp2an |
⊢ ( ℂ –cn→ ℝ ) = ( ( TopOpen ‘ ℂfld ) Cn ( topGen ‘ ran (,) ) ) |
105 |
96 104
|
eleqtri |
⊢ ℑ ∈ ( ( TopOpen ‘ ℂfld ) Cn ( topGen ‘ ran (,) ) ) |
106 |
|
iooretop |
⊢ ( - π (,) π ) ∈ ( topGen ‘ ran (,) ) |
107 |
|
cnima |
⊢ ( ( ℑ ∈ ( ( TopOpen ‘ ℂfld ) Cn ( topGen ‘ ran (,) ) ) ∧ ( - π (,) π ) ∈ ( topGen ‘ ran (,) ) ) → ( ◡ ℑ “ ( - π (,) π ) ) ∈ ( TopOpen ‘ ℂfld ) ) |
108 |
105 106 107
|
mp2an |
⊢ ( ◡ ℑ “ ( - π (,) π ) ) ∈ ( TopOpen ‘ ℂfld ) |
109 |
95 108
|
eqeltri |
⊢ ( log “ 𝐷 ) ∈ ( TopOpen ‘ ℂfld ) |