Step |
Hyp |
Ref |
Expression |
1 |
|
logcn.d |
⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) ) |
2 |
|
logf1o |
⊢ log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log |
3 |
|
f1of1 |
⊢ ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → log : ( ℂ ∖ { 0 } ) –1-1→ ran log ) |
4 |
2 3
|
ax-mp |
⊢ log : ( ℂ ∖ { 0 } ) –1-1→ ran log |
5 |
1
|
logdmss |
⊢ 𝐷 ⊆ ( ℂ ∖ { 0 } ) |
6 |
|
f1ores |
⊢ ( ( log : ( ℂ ∖ { 0 } ) –1-1→ ran log ∧ 𝐷 ⊆ ( ℂ ∖ { 0 } ) ) → ( log ↾ 𝐷 ) : 𝐷 –1-1-onto→ ( log “ 𝐷 ) ) |
7 |
4 5 6
|
mp2an |
⊢ ( log ↾ 𝐷 ) : 𝐷 –1-1-onto→ ( log “ 𝐷 ) |
8 |
|
f1ofun |
⊢ ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → Fun log ) |
9 |
2 8
|
ax-mp |
⊢ Fun log |
10 |
|
f1of |
⊢ ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → log : ( ℂ ∖ { 0 } ) ⟶ ran log ) |
11 |
2 10
|
ax-mp |
⊢ log : ( ℂ ∖ { 0 } ) ⟶ ran log |
12 |
11
|
fdmi |
⊢ dom log = ( ℂ ∖ { 0 } ) |
13 |
5 12
|
sseqtrri |
⊢ 𝐷 ⊆ dom log |
14 |
|
funimass4 |
⊢ ( ( Fun log ∧ 𝐷 ⊆ dom log ) → ( ( log “ 𝐷 ) ⊆ ( ◡ ℑ “ ( - π (,) π ) ) ↔ ∀ 𝑥 ∈ 𝐷 ( log ‘ 𝑥 ) ∈ ( ◡ ℑ “ ( - π (,) π ) ) ) ) |
15 |
9 13 14
|
mp2an |
⊢ ( ( log “ 𝐷 ) ⊆ ( ◡ ℑ “ ( - π (,) π ) ) ↔ ∀ 𝑥 ∈ 𝐷 ( log ‘ 𝑥 ) ∈ ( ◡ ℑ “ ( - π (,) π ) ) ) |
16 |
1
|
ellogdm |
⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ+ ) ) ) |
17 |
16
|
simplbi |
⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ ) |
18 |
1
|
logdmn0 |
⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ≠ 0 ) |
19 |
17 18
|
logcld |
⊢ ( 𝑥 ∈ 𝐷 → ( log ‘ 𝑥 ) ∈ ℂ ) |
20 |
19
|
imcld |
⊢ ( 𝑥 ∈ 𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ℝ ) |
21 |
17 18
|
logimcld |
⊢ ( 𝑥 ∈ 𝐷 → ( - π < ( ℑ ‘ ( log ‘ 𝑥 ) ) ∧ ( ℑ ‘ ( log ‘ 𝑥 ) ) ≤ π ) ) |
22 |
21
|
simpld |
⊢ ( 𝑥 ∈ 𝐷 → - π < ( ℑ ‘ ( log ‘ 𝑥 ) ) ) |
23 |
|
pire |
⊢ π ∈ ℝ |
24 |
23
|
a1i |
⊢ ( 𝑥 ∈ 𝐷 → π ∈ ℝ ) |
25 |
21
|
simprd |
⊢ ( 𝑥 ∈ 𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) ≤ π ) |
26 |
1
|
logdmnrp |
⊢ ( 𝑥 ∈ 𝐷 → ¬ - 𝑥 ∈ ℝ+ ) |
27 |
|
lognegb |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( - 𝑥 ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ 𝑥 ) ) = π ) ) |
28 |
17 18 27
|
syl2anc |
⊢ ( 𝑥 ∈ 𝐷 → ( - 𝑥 ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ 𝑥 ) ) = π ) ) |
29 |
28
|
necon3bbid |
⊢ ( 𝑥 ∈ 𝐷 → ( ¬ - 𝑥 ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ 𝑥 ) ) ≠ π ) ) |
30 |
26 29
|
mpbid |
⊢ ( 𝑥 ∈ 𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) ≠ π ) |
31 |
30
|
necomd |
⊢ ( 𝑥 ∈ 𝐷 → π ≠ ( ℑ ‘ ( log ‘ 𝑥 ) ) ) |
32 |
20 24 25 31
|
leneltd |
⊢ ( 𝑥 ∈ 𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) < π ) |
33 |
23
|
renegcli |
⊢ - π ∈ ℝ |
34 |
33
|
rexri |
⊢ - π ∈ ℝ* |
35 |
23
|
rexri |
⊢ π ∈ ℝ* |
36 |
|
elioo2 |
⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ* ) → ( ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ( - π (,) π ) ↔ ( ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ℝ ∧ - π < ( ℑ ‘ ( log ‘ 𝑥 ) ) ∧ ( ℑ ‘ ( log ‘ 𝑥 ) ) < π ) ) ) |
37 |
34 35 36
|
mp2an |
⊢ ( ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ( - π (,) π ) ↔ ( ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ℝ ∧ - π < ( ℑ ‘ ( log ‘ 𝑥 ) ) ∧ ( ℑ ‘ ( log ‘ 𝑥 ) ) < π ) ) |
38 |
20 22 32 37
|
syl3anbrc |
⊢ ( 𝑥 ∈ 𝐷 → ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ( - π (,) π ) ) |
39 |
|
imf |
⊢ ℑ : ℂ ⟶ ℝ |
40 |
|
ffn |
⊢ ( ℑ : ℂ ⟶ ℝ → ℑ Fn ℂ ) |
41 |
|
elpreima |
⊢ ( ℑ Fn ℂ → ( ( log ‘ 𝑥 ) ∈ ( ◡ ℑ “ ( - π (,) π ) ) ↔ ( ( log ‘ 𝑥 ) ∈ ℂ ∧ ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ( - π (,) π ) ) ) ) |
42 |
39 40 41
|
mp2b |
⊢ ( ( log ‘ 𝑥 ) ∈ ( ◡ ℑ “ ( - π (,) π ) ) ↔ ( ( log ‘ 𝑥 ) ∈ ℂ ∧ ( ℑ ‘ ( log ‘ 𝑥 ) ) ∈ ( - π (,) π ) ) ) |
43 |
19 38 42
|
sylanbrc |
⊢ ( 𝑥 ∈ 𝐷 → ( log ‘ 𝑥 ) ∈ ( ◡ ℑ “ ( - π (,) π ) ) ) |
44 |
15 43
|
mprgbir |
⊢ ( log “ 𝐷 ) ⊆ ( ◡ ℑ “ ( - π (,) π ) ) |
45 |
|
elpreima |
⊢ ( ℑ Fn ℂ → ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ) ) |
46 |
39 40 45
|
mp2b |
⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ) |
47 |
|
simpl |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → 𝑥 ∈ ℂ ) |
48 |
|
eliooord |
⊢ ( ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) → ( - π < ( ℑ ‘ 𝑥 ) ∧ ( ℑ ‘ 𝑥 ) < π ) ) |
49 |
48
|
adantl |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( - π < ( ℑ ‘ 𝑥 ) ∧ ( ℑ ‘ 𝑥 ) < π ) ) |
50 |
49
|
simpld |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → - π < ( ℑ ‘ 𝑥 ) ) |
51 |
49
|
simprd |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( ℑ ‘ 𝑥 ) < π ) |
52 |
|
imcl |
⊢ ( 𝑥 ∈ ℂ → ( ℑ ‘ 𝑥 ) ∈ ℝ ) |
53 |
52
|
adantr |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( ℑ ‘ 𝑥 ) ∈ ℝ ) |
54 |
|
ltle |
⊢ ( ( ( ℑ ‘ 𝑥 ) ∈ ℝ ∧ π ∈ ℝ ) → ( ( ℑ ‘ 𝑥 ) < π → ( ℑ ‘ 𝑥 ) ≤ π ) ) |
55 |
53 23 54
|
sylancl |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( ( ℑ ‘ 𝑥 ) < π → ( ℑ ‘ 𝑥 ) ≤ π ) ) |
56 |
51 55
|
mpd |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( ℑ ‘ 𝑥 ) ≤ π ) |
57 |
|
ellogrn |
⊢ ( 𝑥 ∈ ran log ↔ ( 𝑥 ∈ ℂ ∧ - π < ( ℑ ‘ 𝑥 ) ∧ ( ℑ ‘ 𝑥 ) ≤ π ) ) |
58 |
47 50 56 57
|
syl3anbrc |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → 𝑥 ∈ ran log ) |
59 |
|
logef |
⊢ ( 𝑥 ∈ ran log → ( log ‘ ( exp ‘ 𝑥 ) ) = 𝑥 ) |
60 |
58 59
|
syl |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( log ‘ ( exp ‘ 𝑥 ) ) = 𝑥 ) |
61 |
|
efcl |
⊢ ( 𝑥 ∈ ℂ → ( exp ‘ 𝑥 ) ∈ ℂ ) |
62 |
61
|
adantr |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( exp ‘ 𝑥 ) ∈ ℂ ) |
63 |
53
|
adantr |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℑ ‘ 𝑥 ) ∈ ℝ ) |
64 |
63
|
recnd |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℑ ‘ 𝑥 ) ∈ ℂ ) |
65 |
|
picn |
⊢ π ∈ ℂ |
66 |
65
|
a1i |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → π ∈ ℂ ) |
67 |
|
pipos |
⊢ 0 < π |
68 |
23 67
|
gt0ne0ii |
⊢ π ≠ 0 |
69 |
68
|
a1i |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → π ≠ 0 ) |
70 |
51
|
adantr |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℑ ‘ 𝑥 ) < π ) |
71 |
65
|
mulid1i |
⊢ ( π · 1 ) = π |
72 |
70 71
|
breqtrrdi |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℑ ‘ 𝑥 ) < ( π · 1 ) ) |
73 |
|
1re |
⊢ 1 ∈ ℝ |
74 |
73
|
a1i |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → 1 ∈ ℝ ) |
75 |
23
|
a1i |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → π ∈ ℝ ) |
76 |
67
|
a1i |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → 0 < π ) |
77 |
|
ltdivmul |
⊢ ( ( ( ℑ ‘ 𝑥 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( π ∈ ℝ ∧ 0 < π ) ) → ( ( ( ℑ ‘ 𝑥 ) / π ) < 1 ↔ ( ℑ ‘ 𝑥 ) < ( π · 1 ) ) ) |
78 |
63 74 75 76 77
|
syl112anc |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ( ℑ ‘ 𝑥 ) / π ) < 1 ↔ ( ℑ ‘ 𝑥 ) < ( π · 1 ) ) ) |
79 |
72 78
|
mpbird |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ℑ ‘ 𝑥 ) / π ) < 1 ) |
80 |
|
1e0p1 |
⊢ 1 = ( 0 + 1 ) |
81 |
79 80
|
breqtrdi |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ℑ ‘ 𝑥 ) / π ) < ( 0 + 1 ) ) |
82 |
63
|
recoscld |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( cos ‘ ( ℑ ‘ 𝑥 ) ) ∈ ℝ ) |
83 |
63
|
resincld |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( sin ‘ ( ℑ ‘ 𝑥 ) ) ∈ ℝ ) |
84 |
82 83
|
crimd |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℑ ‘ ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ) = ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) |
85 |
|
efeul |
⊢ ( 𝑥 ∈ ℂ → ( exp ‘ 𝑥 ) = ( ( exp ‘ ( ℜ ‘ 𝑥 ) ) · ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ) ) |
86 |
85
|
ad2antrr |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( exp ‘ 𝑥 ) = ( ( exp ‘ ( ℜ ‘ 𝑥 ) ) · ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ) ) |
87 |
86
|
oveq1d |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( exp ‘ 𝑥 ) / ( exp ‘ ( ℜ ‘ 𝑥 ) ) ) = ( ( ( exp ‘ ( ℜ ‘ 𝑥 ) ) · ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ) / ( exp ‘ ( ℜ ‘ 𝑥 ) ) ) ) |
88 |
82
|
recnd |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( cos ‘ ( ℑ ‘ 𝑥 ) ) ∈ ℂ ) |
89 |
|
ax-icn |
⊢ i ∈ ℂ |
90 |
83
|
recnd |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( sin ‘ ( ℑ ‘ 𝑥 ) ) ∈ ℂ ) |
91 |
|
mulcl |
⊢ ( ( i ∈ ℂ ∧ ( sin ‘ ( ℑ ‘ 𝑥 ) ) ∈ ℂ ) → ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ∈ ℂ ) |
92 |
89 90 91
|
sylancr |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ∈ ℂ ) |
93 |
88 92
|
addcld |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ∈ ℂ ) |
94 |
|
recl |
⊢ ( 𝑥 ∈ ℂ → ( ℜ ‘ 𝑥 ) ∈ ℝ ) |
95 |
94
|
ad2antrr |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℜ ‘ 𝑥 ) ∈ ℝ ) |
96 |
95
|
recnd |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℜ ‘ 𝑥 ) ∈ ℂ ) |
97 |
|
efcl |
⊢ ( ( ℜ ‘ 𝑥 ) ∈ ℂ → ( exp ‘ ( ℜ ‘ 𝑥 ) ) ∈ ℂ ) |
98 |
96 97
|
syl |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( exp ‘ ( ℜ ‘ 𝑥 ) ) ∈ ℂ ) |
99 |
|
efne0 |
⊢ ( ( ℜ ‘ 𝑥 ) ∈ ℂ → ( exp ‘ ( ℜ ‘ 𝑥 ) ) ≠ 0 ) |
100 |
96 99
|
syl |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( exp ‘ ( ℜ ‘ 𝑥 ) ) ≠ 0 ) |
101 |
93 98 100
|
divcan3d |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ( exp ‘ ( ℜ ‘ 𝑥 ) ) · ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ) / ( exp ‘ ( ℜ ‘ 𝑥 ) ) ) = ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ) |
102 |
87 101
|
eqtrd |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( exp ‘ 𝑥 ) / ( exp ‘ ( ℜ ‘ 𝑥 ) ) ) = ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ) |
103 |
|
simpr |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( exp ‘ 𝑥 ) ∈ ℝ ) |
104 |
95
|
reefcld |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( exp ‘ ( ℜ ‘ 𝑥 ) ) ∈ ℝ ) |
105 |
103 104 100
|
redivcld |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( exp ‘ 𝑥 ) / ( exp ‘ ( ℜ ‘ 𝑥 ) ) ) ∈ ℝ ) |
106 |
102 105
|
eqeltrrd |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ∈ ℝ ) |
107 |
106
|
reim0d |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℑ ‘ ( ( cos ‘ ( ℑ ‘ 𝑥 ) ) + ( i · ( sin ‘ ( ℑ ‘ 𝑥 ) ) ) ) ) = 0 ) |
108 |
84 107
|
eqtr3d |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( sin ‘ ( ℑ ‘ 𝑥 ) ) = 0 ) |
109 |
|
sineq0 |
⊢ ( ( ℑ ‘ 𝑥 ) ∈ ℂ → ( ( sin ‘ ( ℑ ‘ 𝑥 ) ) = 0 ↔ ( ( ℑ ‘ 𝑥 ) / π ) ∈ ℤ ) ) |
110 |
64 109
|
syl |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( sin ‘ ( ℑ ‘ 𝑥 ) ) = 0 ↔ ( ( ℑ ‘ 𝑥 ) / π ) ∈ ℤ ) ) |
111 |
108 110
|
mpbid |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ℑ ‘ 𝑥 ) / π ) ∈ ℤ ) |
112 |
|
0z |
⊢ 0 ∈ ℤ |
113 |
|
zleltp1 |
⊢ ( ( ( ( ℑ ‘ 𝑥 ) / π ) ∈ ℤ ∧ 0 ∈ ℤ ) → ( ( ( ℑ ‘ 𝑥 ) / π ) ≤ 0 ↔ ( ( ℑ ‘ 𝑥 ) / π ) < ( 0 + 1 ) ) ) |
114 |
111 112 113
|
sylancl |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ( ℑ ‘ 𝑥 ) / π ) ≤ 0 ↔ ( ( ℑ ‘ 𝑥 ) / π ) < ( 0 + 1 ) ) ) |
115 |
81 114
|
mpbird |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ℑ ‘ 𝑥 ) / π ) ≤ 0 ) |
116 |
|
df-neg |
⊢ - 1 = ( 0 − 1 ) |
117 |
65
|
mulm1i |
⊢ ( - 1 · π ) = - π |
118 |
50
|
adantr |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → - π < ( ℑ ‘ 𝑥 ) ) |
119 |
117 118
|
eqbrtrid |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( - 1 · π ) < ( ℑ ‘ 𝑥 ) ) |
120 |
73
|
renegcli |
⊢ - 1 ∈ ℝ |
121 |
120
|
a1i |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → - 1 ∈ ℝ ) |
122 |
|
ltmuldiv |
⊢ ( ( - 1 ∈ ℝ ∧ ( ℑ ‘ 𝑥 ) ∈ ℝ ∧ ( π ∈ ℝ ∧ 0 < π ) ) → ( ( - 1 · π ) < ( ℑ ‘ 𝑥 ) ↔ - 1 < ( ( ℑ ‘ 𝑥 ) / π ) ) ) |
123 |
121 63 75 76 122
|
syl112anc |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( - 1 · π ) < ( ℑ ‘ 𝑥 ) ↔ - 1 < ( ( ℑ ‘ 𝑥 ) / π ) ) ) |
124 |
119 123
|
mpbid |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → - 1 < ( ( ℑ ‘ 𝑥 ) / π ) ) |
125 |
116 124
|
eqbrtrrid |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( 0 − 1 ) < ( ( ℑ ‘ 𝑥 ) / π ) ) |
126 |
|
zlem1lt |
⊢ ( ( 0 ∈ ℤ ∧ ( ( ℑ ‘ 𝑥 ) / π ) ∈ ℤ ) → ( 0 ≤ ( ( ℑ ‘ 𝑥 ) / π ) ↔ ( 0 − 1 ) < ( ( ℑ ‘ 𝑥 ) / π ) ) ) |
127 |
112 111 126
|
sylancr |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( 0 ≤ ( ( ℑ ‘ 𝑥 ) / π ) ↔ ( 0 − 1 ) < ( ( ℑ ‘ 𝑥 ) / π ) ) ) |
128 |
125 127
|
mpbird |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → 0 ≤ ( ( ℑ ‘ 𝑥 ) / π ) ) |
129 |
63 75 69
|
redivcld |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ℑ ‘ 𝑥 ) / π ) ∈ ℝ ) |
130 |
|
0re |
⊢ 0 ∈ ℝ |
131 |
|
letri3 |
⊢ ( ( ( ( ℑ ‘ 𝑥 ) / π ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ( ℑ ‘ 𝑥 ) / π ) = 0 ↔ ( ( ( ℑ ‘ 𝑥 ) / π ) ≤ 0 ∧ 0 ≤ ( ( ℑ ‘ 𝑥 ) / π ) ) ) ) |
132 |
129 130 131
|
sylancl |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ( ℑ ‘ 𝑥 ) / π ) = 0 ↔ ( ( ( ℑ ‘ 𝑥 ) / π ) ≤ 0 ∧ 0 ≤ ( ( ℑ ‘ 𝑥 ) / π ) ) ) ) |
133 |
115 128 132
|
mpbir2and |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ( ℑ ‘ 𝑥 ) / π ) = 0 ) |
134 |
64 66 69 133
|
diveq0d |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( ℑ ‘ 𝑥 ) = 0 ) |
135 |
|
reim0b |
⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ∈ ℝ ↔ ( ℑ ‘ 𝑥 ) = 0 ) ) |
136 |
135
|
ad2antrr |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( 𝑥 ∈ ℝ ↔ ( ℑ ‘ 𝑥 ) = 0 ) ) |
137 |
134 136
|
mpbird |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → 𝑥 ∈ ℝ ) |
138 |
137
|
rpefcld |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) ∧ ( exp ‘ 𝑥 ) ∈ ℝ ) → ( exp ‘ 𝑥 ) ∈ ℝ+ ) |
139 |
138
|
ex |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( ( exp ‘ 𝑥 ) ∈ ℝ → ( exp ‘ 𝑥 ) ∈ ℝ+ ) ) |
140 |
1
|
ellogdm |
⊢ ( ( exp ‘ 𝑥 ) ∈ 𝐷 ↔ ( ( exp ‘ 𝑥 ) ∈ ℂ ∧ ( ( exp ‘ 𝑥 ) ∈ ℝ → ( exp ‘ 𝑥 ) ∈ ℝ+ ) ) ) |
141 |
62 139 140
|
sylanbrc |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( exp ‘ 𝑥 ) ∈ 𝐷 ) |
142 |
|
funfvima2 |
⊢ ( ( Fun log ∧ 𝐷 ⊆ dom log ) → ( ( exp ‘ 𝑥 ) ∈ 𝐷 → ( log ‘ ( exp ‘ 𝑥 ) ) ∈ ( log “ 𝐷 ) ) ) |
143 |
9 13 142
|
mp2an |
⊢ ( ( exp ‘ 𝑥 ) ∈ 𝐷 → ( log ‘ ( exp ‘ 𝑥 ) ) ∈ ( log “ 𝐷 ) ) |
144 |
141 143
|
syl |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → ( log ‘ ( exp ‘ 𝑥 ) ) ∈ ( log “ 𝐷 ) ) |
145 |
60 144
|
eqeltrrd |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( ℑ ‘ 𝑥 ) ∈ ( - π (,) π ) ) → 𝑥 ∈ ( log “ 𝐷 ) ) |
146 |
46 145
|
sylbi |
⊢ ( 𝑥 ∈ ( ◡ ℑ “ ( - π (,) π ) ) → 𝑥 ∈ ( log “ 𝐷 ) ) |
147 |
146
|
ssriv |
⊢ ( ◡ ℑ “ ( - π (,) π ) ) ⊆ ( log “ 𝐷 ) |
148 |
44 147
|
eqssi |
⊢ ( log “ 𝐷 ) = ( ◡ ℑ “ ( - π (,) π ) ) |
149 |
|
f1oeq3 |
⊢ ( ( log “ 𝐷 ) = ( ◡ ℑ “ ( - π (,) π ) ) → ( ( log ↾ 𝐷 ) : 𝐷 –1-1-onto→ ( log “ 𝐷 ) ↔ ( log ↾ 𝐷 ) : 𝐷 –1-1-onto→ ( ◡ ℑ “ ( - π (,) π ) ) ) ) |
150 |
148 149
|
ax-mp |
⊢ ( ( log ↾ 𝐷 ) : 𝐷 –1-1-onto→ ( log “ 𝐷 ) ↔ ( log ↾ 𝐷 ) : 𝐷 –1-1-onto→ ( ◡ ℑ “ ( - π (,) π ) ) ) |
151 |
7 150
|
mpbi |
⊢ ( log ↾ 𝐷 ) : 𝐷 –1-1-onto→ ( ◡ ℑ “ ( - π (,) π ) ) |