Step | Hyp | Ref
| Expression |
1 | | logf1o 24311 |
. . . 4
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log |
2 | | f1of1 6136 |
. . . 4
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → log:(ℂ ∖ {0})–1-1→ran log) |
3 | 1, 2 | ax-mp 5 |
. . 3
⊢
log:(ℂ ∖ {0})–1-1→ran log |
4 | | logcn.d |
. . . 4
⊢ 𝐷 = (ℂ ∖
(-∞(,]0)) |
5 | 4 | logdmss 24388 |
. . 3
⊢ 𝐷 ⊆ (ℂ ∖
{0}) |
6 | | f1ores 6151 |
. . 3
⊢
((log:(ℂ ∖ {0})–1-1→ran log ∧ 𝐷 ⊆ (ℂ ∖ {0})) → (log
↾ 𝐷):𝐷–1-1-onto→(log
“ 𝐷)) |
7 | 3, 5, 6 | mp2an 708 |
. 2
⊢ (log
↾ 𝐷):𝐷–1-1-onto→(log
“ 𝐷) |
8 | | f1ofun 6139 |
. . . . . . 7
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → Fun log) |
9 | 1, 8 | ax-mp 5 |
. . . . . 6
⊢ Fun
log |
10 | | f1of 6137 |
. . . . . . . . 9
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → log:(ℂ ∖ {0})⟶ran log) |
11 | 1, 10 | ax-mp 5 |
. . . . . . . 8
⊢
log:(ℂ ∖ {0})⟶ran log |
12 | 11 | fdmi 6052 |
. . . . . . 7
⊢ dom log =
(ℂ ∖ {0}) |
13 | 5, 12 | sseqtr4i 3638 |
. . . . . 6
⊢ 𝐷 ⊆ dom
log |
14 | | funimass4 6247 |
. . . . . 6
⊢ ((Fun log
∧ 𝐷 ⊆ dom log)
→ ((log “ 𝐷)
⊆ (◡ℑ “
(-π(,)π)) ↔ ∀𝑥 ∈ 𝐷 (log‘𝑥) ∈ (◡ℑ “
(-π(,)π)))) |
15 | 9, 13, 14 | mp2an 708 |
. . . . 5
⊢ ((log
“ 𝐷) ⊆ (◡ℑ “ (-π(,)π)) ↔
∀𝑥 ∈ 𝐷 (log‘𝑥) ∈ (◡ℑ “
(-π(,)π))) |
16 | 4 | ellogdm 24385 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ ℂ ∧ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ+))) |
17 | 16 | simplbi 476 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ) |
18 | 4 | logdmn0 24386 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → 𝑥 ≠ 0) |
19 | 17, 18 | logcld 24317 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (log‘𝑥) ∈ ℂ) |
20 | 19 | imcld 13935 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ∈
ℝ) |
21 | 17, 18 | logimcld 24318 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (-π <
(ℑ‘(log‘𝑥)) ∧ (ℑ‘(log‘𝑥)) ≤ π)) |
22 | 21 | simpld 475 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → -π <
(ℑ‘(log‘𝑥))) |
23 | 4 | logdmnrp 24387 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → ¬ -𝑥 ∈ ℝ+) |
24 | | lognegb 24336 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (-𝑥 ∈ ℝ+
↔ (ℑ‘(log‘𝑥)) = π)) |
25 | 17, 18, 24 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → (-𝑥 ∈ ℝ+ ↔
(ℑ‘(log‘𝑥)) = π)) |
26 | 25 | necon3bbid 2831 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → (¬ -𝑥 ∈ ℝ+ ↔
(ℑ‘(log‘𝑥)) ≠ π)) |
27 | 23, 26 | mpbid 222 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ≠ π) |
28 | 27 | necomd 2849 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → π ≠
(ℑ‘(log‘𝑥))) |
29 | | pire 24210 |
. . . . . . . . . 10
⊢ π
∈ ℝ |
30 | 29 | a1i 11 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → π ∈
ℝ) |
31 | 21 | simprd 479 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ≤ π) |
32 | 20, 30, 31 | leltned 10190 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → ((ℑ‘(log‘𝑥)) < π ↔ π ≠
(ℑ‘(log‘𝑥)))) |
33 | 28, 32 | mpbird 247 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) < π) |
34 | 29 | renegcli 10342 |
. . . . . . . . 9
⊢ -π
∈ ℝ |
35 | 34 | rexri 10097 |
. . . . . . . 8
⊢ -π
∈ ℝ* |
36 | 29 | rexri 10097 |
. . . . . . . 8
⊢ π
∈ ℝ* |
37 | | elioo2 12216 |
. . . . . . . 8
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ*) →
((ℑ‘(log‘𝑥)) ∈ (-π(,)π) ↔
((ℑ‘(log‘𝑥)) ∈ ℝ ∧ -π <
(ℑ‘(log‘𝑥)) ∧ (ℑ‘(log‘𝑥)) < π))) |
38 | 35, 36, 37 | mp2an 708 |
. . . . . . 7
⊢
((ℑ‘(log‘𝑥)) ∈ (-π(,)π) ↔
((ℑ‘(log‘𝑥)) ∈ ℝ ∧ -π <
(ℑ‘(log‘𝑥)) ∧ (ℑ‘(log‘𝑥)) < π)) |
39 | 20, 22, 33, 38 | syl3anbrc 1246 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ∈
(-π(,)π)) |
40 | | imf 13853 |
. . . . . . 7
⊢
ℑ:ℂ⟶ℝ |
41 | | ffn 6045 |
. . . . . . 7
⊢
(ℑ:ℂ⟶ℝ → ℑ Fn
ℂ) |
42 | | elpreima 6337 |
. . . . . . 7
⊢ (ℑ
Fn ℂ → ((log‘𝑥) ∈ (◡ℑ “ (-π(,)π)) ↔
((log‘𝑥) ∈
ℂ ∧ (ℑ‘(log‘𝑥)) ∈ (-π(,)π)))) |
43 | 40, 41, 42 | mp2b 10 |
. . . . . 6
⊢
((log‘𝑥)
∈ (◡ℑ “
(-π(,)π)) ↔ ((log‘𝑥) ∈ ℂ ∧
(ℑ‘(log‘𝑥)) ∈ (-π(,)π))) |
44 | 19, 39, 43 | sylanbrc 698 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (log‘𝑥) ∈ (◡ℑ “
(-π(,)π))) |
45 | 15, 44 | mprgbir 2927 |
. . . 4
⊢ (log
“ 𝐷) ⊆ (◡ℑ “
(-π(,)π)) |
46 | | elpreima 6337 |
. . . . . . 7
⊢ (ℑ
Fn ℂ → (𝑥 ∈
(◡ℑ “ (-π(,)π))
↔ (𝑥 ∈ ℂ
∧ (ℑ‘𝑥)
∈ (-π(,)π)))) |
47 | 40, 41, 46 | mp2b 10 |
. . . . . 6
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) ↔
(𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π))) |
48 | | simpl 473 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → 𝑥
∈ ℂ) |
49 | | eliooord 12233 |
. . . . . . . . . . 11
⊢
((ℑ‘𝑥)
∈ (-π(,)π) → (-π < (ℑ‘𝑥) ∧ (ℑ‘𝑥) < π)) |
50 | 49 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (-π < (ℑ‘𝑥) ∧ (ℑ‘𝑥) < π)) |
51 | 50 | simpld 475 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → -π < (ℑ‘𝑥)) |
52 | 50 | simprd 479 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (ℑ‘𝑥) < π) |
53 | | imcl 13851 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ →
(ℑ‘𝑥) ∈
ℝ) |
54 | 53 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (ℑ‘𝑥) ∈ ℝ) |
55 | | ltle 10126 |
. . . . . . . . . . 11
⊢
(((ℑ‘𝑥)
∈ ℝ ∧ π ∈ ℝ) → ((ℑ‘𝑥) < π →
(ℑ‘𝑥) ≤
π)) |
56 | 54, 29, 55 | sylancl 694 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → ((ℑ‘𝑥) < π → (ℑ‘𝑥) ≤ π)) |
57 | 52, 56 | mpd 15 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (ℑ‘𝑥) ≤ π) |
58 | | ellogrn 24306 |
. . . . . . . . 9
⊢ (𝑥 ∈ ran log ↔ (𝑥 ∈ ℂ ∧ -π <
(ℑ‘𝑥) ∧
(ℑ‘𝑥) ≤
π)) |
59 | 48, 51, 57, 58 | syl3anbrc 1246 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → 𝑥
∈ ran log) |
60 | | logef 24328 |
. . . . . . . 8
⊢ (𝑥 ∈ ran log →
(log‘(exp‘𝑥)) =
𝑥) |
61 | 59, 60 | syl 17 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (log‘(exp‘𝑥)) = 𝑥) |
62 | | efcl 14813 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ →
(exp‘𝑥) ∈
ℂ) |
63 | 62 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (exp‘𝑥) ∈ ℂ) |
64 | 54 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℑ‘𝑥) ∈
ℝ) |
65 | 64 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℑ‘𝑥) ∈
ℂ) |
66 | | picn 24211 |
. . . . . . . . . . . . . 14
⊢ π
∈ ℂ |
67 | 66 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → π ∈
ℂ) |
68 | | pipos 24212 |
. . . . . . . . . . . . . . 15
⊢ 0 <
π |
69 | 29, 68 | gt0ne0ii 10564 |
. . . . . . . . . . . . . 14
⊢ π ≠
0 |
70 | 69 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → π ≠
0) |
71 | 52 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℑ‘𝑥) < π) |
72 | 66 | mulid1i 10042 |
. . . . . . . . . . . . . . . . . 18
⊢ (π
· 1) = π |
73 | 71, 72 | syl6breqr 4695 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℑ‘𝑥) < (π ·
1)) |
74 | | 1re 10039 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℝ |
75 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → 1 ∈
ℝ) |
76 | 29 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → π ∈
ℝ) |
77 | 68 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → 0 <
π) |
78 | | ltdivmul 10898 |
. . . . . . . . . . . . . . . . . 18
⊢
(((ℑ‘𝑥)
∈ ℝ ∧ 1 ∈ ℝ ∧ (π ∈ ℝ ∧ 0 <
π)) → (((ℑ‘𝑥) / π) < 1 ↔ (ℑ‘𝑥) < (π ·
1))) |
79 | 64, 75, 76, 77, 78 | syl112anc 1330 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(((ℑ‘𝑥) / π)
< 1 ↔ (ℑ‘𝑥) < (π · 1))) |
80 | 73, 79 | mpbird 247 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((ℑ‘𝑥) / π)
< 1) |
81 | | 1e0p1 11552 |
. . . . . . . . . . . . . . . 16
⊢ 1 = (0 +
1) |
82 | 80, 81 | syl6breq 4694 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((ℑ‘𝑥) / π)
< (0 + 1)) |
83 | 64 | recoscld 14874 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(cos‘(ℑ‘𝑥)) ∈ ℝ) |
84 | 64 | resincld 14873 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(sin‘(ℑ‘𝑥)) ∈ ℝ) |
85 | 83, 84 | crimd 13972 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(ℑ‘((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥))))) = (sin‘(ℑ‘𝑥))) |
86 | | efeul 14892 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℂ →
(exp‘𝑥) =
((exp‘(ℜ‘𝑥)) · ((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥)))))) |
87 | 86 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (exp‘𝑥) =
((exp‘(ℜ‘𝑥)) · ((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥)))))) |
88 | 87 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → ((exp‘𝑥) /
(exp‘(ℜ‘𝑥))) = (((exp‘(ℜ‘𝑥)) ·
((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥))))) / (exp‘(ℜ‘𝑥)))) |
89 | 83 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(cos‘(ℑ‘𝑥)) ∈ ℂ) |
90 | | ax-icn 9995 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ i ∈
ℂ |
91 | 84 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(sin‘(ℑ‘𝑥)) ∈ ℂ) |
92 | | mulcl 10020 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((i
∈ ℂ ∧ (sin‘(ℑ‘𝑥)) ∈ ℂ) → (i ·
(sin‘(ℑ‘𝑥))) ∈ ℂ) |
93 | 90, 91, 92 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (i ·
(sin‘(ℑ‘𝑥))) ∈ ℂ) |
94 | 89, 93 | addcld 10059 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥)))) ∈ ℂ) |
95 | | recl 13850 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ ℂ →
(ℜ‘𝑥) ∈
ℝ) |
96 | 95 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℜ‘𝑥) ∈
ℝ) |
97 | 96 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℜ‘𝑥) ∈
ℂ) |
98 | | efcl 14813 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((ℜ‘𝑥)
∈ ℂ → (exp‘(ℜ‘𝑥)) ∈ ℂ) |
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(exp‘(ℜ‘𝑥)) ∈ ℂ) |
100 | | efne0 14827 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((ℜ‘𝑥)
∈ ℂ → (exp‘(ℜ‘𝑥)) ≠ 0) |
101 | 97, 100 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(exp‘(ℜ‘𝑥)) ≠ 0) |
102 | 94, 99, 101 | divcan3d 10806 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(((exp‘(ℜ‘𝑥)) · ((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥))))) / (exp‘(ℜ‘𝑥))) =
((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥))))) |
103 | 88, 102 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → ((exp‘𝑥) /
(exp‘(ℜ‘𝑥))) = ((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥))))) |
104 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (exp‘𝑥) ∈
ℝ) |
105 | 96 | reefcld 14818 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(exp‘(ℜ‘𝑥)) ∈ ℝ) |
106 | 104, 105,
101 | redivcld 10853 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → ((exp‘𝑥) /
(exp‘(ℜ‘𝑥))) ∈ ℝ) |
107 | 103, 106 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥)))) ∈ ℝ) |
108 | 107 | reim0d 13965 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(ℑ‘((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥))))) = 0) |
109 | 85, 108 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(sin‘(ℑ‘𝑥)) = 0) |
110 | | sineq0 24273 |
. . . . . . . . . . . . . . . . . 18
⊢
((ℑ‘𝑥)
∈ ℂ → ((sin‘(ℑ‘𝑥)) = 0 ↔ ((ℑ‘𝑥) / π) ∈
ℤ)) |
111 | 65, 110 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((sin‘(ℑ‘𝑥)) = 0 ↔ ((ℑ‘𝑥) / π) ∈
ℤ)) |
112 | 109, 111 | mpbid 222 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((ℑ‘𝑥) / π)
∈ ℤ) |
113 | | 0z 11388 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℤ |
114 | | zleltp1 11428 |
. . . . . . . . . . . . . . . 16
⊢
((((ℑ‘𝑥)
/ π) ∈ ℤ ∧ 0 ∈ ℤ) → (((ℑ‘𝑥) / π) ≤ 0 ↔
((ℑ‘𝑥) / π)
< (0 + 1))) |
115 | 112, 113,
114 | sylancl 694 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(((ℑ‘𝑥) / π)
≤ 0 ↔ ((ℑ‘𝑥) / π) < (0 + 1))) |
116 | 82, 115 | mpbird 247 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((ℑ‘𝑥) / π)
≤ 0) |
117 | | df-neg 10269 |
. . . . . . . . . . . . . . . 16
⊢ -1 = (0
− 1) |
118 | 66 | mulm1i 10475 |
. . . . . . . . . . . . . . . . . 18
⊢ (-1
· π) = -π |
119 | 51 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → -π <
(ℑ‘𝑥)) |
120 | 118, 119 | syl5eqbr 4688 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (-1 · π)
< (ℑ‘𝑥)) |
121 | 74 | renegcli 10342 |
. . . . . . . . . . . . . . . . . . 19
⊢ -1 ∈
ℝ |
122 | 121 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → -1 ∈
ℝ) |
123 | | ltmuldiv 10896 |
. . . . . . . . . . . . . . . . . 18
⊢ ((-1
∈ ℝ ∧ (ℑ‘𝑥) ∈ ℝ ∧ (π ∈ ℝ
∧ 0 < π)) → ((-1 · π) < (ℑ‘𝑥) ↔ -1 <
((ℑ‘𝑥) /
π))) |
124 | 122, 64, 76, 77, 123 | syl112anc 1330 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → ((-1 · π)
< (ℑ‘𝑥)
↔ -1 < ((ℑ‘𝑥) / π))) |
125 | 120, 124 | mpbid 222 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → -1 <
((ℑ‘𝑥) /
π)) |
126 | 117, 125 | syl5eqbrr 4689 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (0 − 1) <
((ℑ‘𝑥) /
π)) |
127 | | zlem1lt 11429 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℤ ∧ ((ℑ‘𝑥) / π) ∈ ℤ) → (0 ≤
((ℑ‘𝑥) / π)
↔ (0 − 1) < ((ℑ‘𝑥) / π))) |
128 | 113, 112,
127 | sylancr 695 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (0 ≤
((ℑ‘𝑥) / π)
↔ (0 − 1) < ((ℑ‘𝑥) / π))) |
129 | 126, 128 | mpbird 247 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → 0 ≤
((ℑ‘𝑥) /
π)) |
130 | 64, 76, 70 | redivcld 10853 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((ℑ‘𝑥) / π)
∈ ℝ) |
131 | | 0re 10040 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
132 | | letri3 10123 |
. . . . . . . . . . . . . . 15
⊢
((((ℑ‘𝑥)
/ π) ∈ ℝ ∧ 0 ∈ ℝ) → (((ℑ‘𝑥) / π) = 0 ↔
(((ℑ‘𝑥) / π)
≤ 0 ∧ 0 ≤ ((ℑ‘𝑥) / π)))) |
133 | 130, 131,
132 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(((ℑ‘𝑥) / π)
= 0 ↔ (((ℑ‘𝑥) / π) ≤ 0 ∧ 0 ≤
((ℑ‘𝑥) /
π)))) |
134 | 116, 129,
133 | mpbir2and 957 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((ℑ‘𝑥) / π)
= 0) |
135 | 65, 67, 70, 134 | diveq0d 10808 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℑ‘𝑥) = 0) |
136 | | reim0b 13859 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → (𝑥 ∈ ℝ ↔
(ℑ‘𝑥) =
0)) |
137 | 136 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (𝑥 ∈ ℝ ↔ (ℑ‘𝑥) = 0)) |
138 | 135, 137 | mpbird 247 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → 𝑥 ∈ ℝ) |
139 | 138 | rpefcld 14835 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (exp‘𝑥) ∈
ℝ+) |
140 | 139 | ex 450 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → ((exp‘𝑥) ∈ ℝ → (exp‘𝑥) ∈
ℝ+)) |
141 | 4 | ellogdm 24385 |
. . . . . . . . 9
⊢
((exp‘𝑥)
∈ 𝐷 ↔
((exp‘𝑥) ∈
ℂ ∧ ((exp‘𝑥) ∈ ℝ → (exp‘𝑥) ∈
ℝ+))) |
142 | 63, 140, 141 | sylanbrc 698 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (exp‘𝑥) ∈ 𝐷) |
143 | | funfvima2 6493 |
. . . . . . . . 9
⊢ ((Fun log
∧ 𝐷 ⊆ dom log)
→ ((exp‘𝑥)
∈ 𝐷 →
(log‘(exp‘𝑥))
∈ (log “ 𝐷))) |
144 | 9, 13, 143 | mp2an 708 |
. . . . . . . 8
⊢
((exp‘𝑥)
∈ 𝐷 →
(log‘(exp‘𝑥))
∈ (log “ 𝐷)) |
145 | 142, 144 | syl 17 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (log‘(exp‘𝑥)) ∈ (log “ 𝐷)) |
146 | 61, 145 | eqeltrrd 2702 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → 𝑥
∈ (log “ 𝐷)) |
147 | 47, 146 | sylbi 207 |
. . . . 5
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) → 𝑥 ∈ (log “ 𝐷)) |
148 | 147 | ssriv 3607 |
. . . 4
⊢ (◡ℑ “ (-π(,)π)) ⊆ (log
“ 𝐷) |
149 | 45, 148 | eqssi 3619 |
. . 3
⊢ (log
“ 𝐷) = (◡ℑ “
(-π(,)π)) |
150 | | f1oeq3 6129 |
. . 3
⊢ ((log
“ 𝐷) = (◡ℑ “ (-π(,)π)) → ((log
↾ 𝐷):𝐷–1-1-onto→(log
“ 𝐷) ↔ (log
↾ 𝐷):𝐷–1-1-onto→(◡ℑ “
(-π(,)π)))) |
151 | 149, 150 | ax-mp 5 |
. 2
⊢ ((log
↾ 𝐷):𝐷–1-1-onto→(log
“ 𝐷) ↔ (log
↾ 𝐷):𝐷–1-1-onto→(◡ℑ “
(-π(,)π))) |
152 | 7, 151 | mpbi 220 |
1
⊢ (log
↾ 𝐷):𝐷–1-1-onto→(◡ℑ “
(-π(,)π)) |