Step | Hyp | Ref
| Expression |
1 | | logf1o 25729 |
. . . 4
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log |
2 | | f1of1 6724 |
. . . 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 25806 |
. . 3
⊢ 𝐷 ⊆ (ℂ ∖
{0}) |
6 | | f1ores 6739 |
. . 3
⊢
((log:(ℂ ∖ {0})–1-1→ran log ∧ 𝐷 ⊆ (ℂ ∖ {0})) → (log
↾ 𝐷):𝐷–1-1-onto→(log
“ 𝐷)) |
7 | 3, 5, 6 | mp2an 689 |
. 2
⊢ (log
↾ 𝐷):𝐷–1-1-onto→(log
“ 𝐷) |
8 | | f1ofun 6727 |
. . . . . . 7
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → Fun log) |
9 | 1, 8 | ax-mp 5 |
. . . . . 6
⊢ Fun
log |
10 | | f1of 6725 |
. . . . . . . . 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 6621 |
. . . . . . 7
⊢ dom log =
(ℂ ∖ {0}) |
13 | 5, 12 | sseqtrri 3959 |
. . . . . 6
⊢ 𝐷 ⊆ dom
log |
14 | | funimass4 6843 |
. . . . . 6
⊢ ((Fun log
∧ 𝐷 ⊆ dom log)
→ ((log “ 𝐷)
⊆ (◡ℑ “
(-π(,)π)) ↔ ∀𝑥 ∈ 𝐷 (log‘𝑥) ∈ (◡ℑ “
(-π(,)π)))) |
15 | 9, 13, 14 | mp2an 689 |
. . . . 5
⊢ ((log
“ 𝐷) ⊆ (◡ℑ “ (-π(,)π)) ↔
∀𝑥 ∈ 𝐷 (log‘𝑥) ∈ (◡ℑ “
(-π(,)π))) |
16 | 4 | ellogdm 25803 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ ℂ ∧ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ+))) |
17 | 16 | simplbi 498 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ) |
18 | 4 | logdmn0 25804 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → 𝑥 ≠ 0) |
19 | 17, 18 | logcld 25735 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (log‘𝑥) ∈ ℂ) |
20 | 19 | imcld 14915 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ∈
ℝ) |
21 | 17, 18 | logimcld 25736 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (-π <
(ℑ‘(log‘𝑥)) ∧ (ℑ‘(log‘𝑥)) ≤ π)) |
22 | 21 | simpld 495 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → -π <
(ℑ‘(log‘𝑥))) |
23 | | pire 25624 |
. . . . . . . . 9
⊢ π
∈ ℝ |
24 | 23 | a1i 11 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → π ∈
ℝ) |
25 | 21 | simprd 496 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ≤ π) |
26 | 4 | logdmnrp 25805 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → ¬ -𝑥 ∈ ℝ+) |
27 | | lognegb 25754 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (-𝑥 ∈ ℝ+
↔ (ℑ‘(log‘𝑥)) = π)) |
28 | 17, 18, 27 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → (-𝑥 ∈ ℝ+ ↔
(ℑ‘(log‘𝑥)) = π)) |
29 | 28 | necon3bbid 2982 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → (¬ -𝑥 ∈ ℝ+ ↔
(ℑ‘(log‘𝑥)) ≠ π)) |
30 | 26, 29 | mpbid 231 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ≠ π) |
31 | 30 | necomd 3000 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → π ≠
(ℑ‘(log‘𝑥))) |
32 | 20, 24, 25, 31 | leneltd 11138 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) < π) |
33 | 23 | renegcli 11291 |
. . . . . . . . 9
⊢ -π
∈ ℝ |
34 | 33 | rexri 11042 |
. . . . . . . 8
⊢ -π
∈ ℝ* |
35 | 23 | rexri 11042 |
. . . . . . . 8
⊢ π
∈ ℝ* |
36 | | elioo2 13129 |
. . . . . . . 8
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ*) →
((ℑ‘(log‘𝑥)) ∈ (-π(,)π) ↔
((ℑ‘(log‘𝑥)) ∈ ℝ ∧ -π <
(ℑ‘(log‘𝑥)) ∧ (ℑ‘(log‘𝑥)) < π))) |
37 | 34, 35, 36 | mp2an 689 |
. . . . . . 7
⊢
((ℑ‘(log‘𝑥)) ∈ (-π(,)π) ↔
((ℑ‘(log‘𝑥)) ∈ ℝ ∧ -π <
(ℑ‘(log‘𝑥)) ∧ (ℑ‘(log‘𝑥)) < π)) |
38 | 20, 22, 32, 37 | syl3anbrc 1342 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ∈
(-π(,)π)) |
39 | | imf 14833 |
. . . . . . 7
⊢
ℑ:ℂ⟶ℝ |
40 | | ffn 6609 |
. . . . . . 7
⊢
(ℑ:ℂ⟶ℝ → ℑ Fn
ℂ) |
41 | | elpreima 6944 |
. . . . . . 7
⊢ (ℑ
Fn ℂ → ((log‘𝑥) ∈ (◡ℑ “ (-π(,)π)) ↔
((log‘𝑥) ∈
ℂ ∧ (ℑ‘(log‘𝑥)) ∈ (-π(,)π)))) |
42 | 39, 40, 41 | mp2b 10 |
. . . . . 6
⊢
((log‘𝑥)
∈ (◡ℑ “
(-π(,)π)) ↔ ((log‘𝑥) ∈ ℂ ∧
(ℑ‘(log‘𝑥)) ∈ (-π(,)π))) |
43 | 19, 38, 42 | sylanbrc 583 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (log‘𝑥) ∈ (◡ℑ “
(-π(,)π))) |
44 | 15, 43 | mprgbir 3080 |
. . . 4
⊢ (log
“ 𝐷) ⊆ (◡ℑ “
(-π(,)π)) |
45 | | elpreima 6944 |
. . . . . . 7
⊢ (ℑ
Fn ℂ → (𝑥 ∈
(◡ℑ “ (-π(,)π))
↔ (𝑥 ∈ ℂ
∧ (ℑ‘𝑥)
∈ (-π(,)π)))) |
46 | 39, 40, 45 | mp2b 10 |
. . . . . 6
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) ↔
(𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π))) |
47 | | simpl 483 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → 𝑥
∈ ℂ) |
48 | | eliooord 13147 |
. . . . . . . . . . 11
⊢
((ℑ‘𝑥)
∈ (-π(,)π) → (-π < (ℑ‘𝑥) ∧ (ℑ‘𝑥) < π)) |
49 | 48 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (-π < (ℑ‘𝑥) ∧ (ℑ‘𝑥) < π)) |
50 | 49 | simpld 495 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → -π < (ℑ‘𝑥)) |
51 | 49 | simprd 496 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (ℑ‘𝑥) < π) |
52 | | imcl 14831 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ →
(ℑ‘𝑥) ∈
ℝ) |
53 | 52 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (ℑ‘𝑥) ∈ ℝ) |
54 | | ltle 11072 |
. . . . . . . . . . 11
⊢
(((ℑ‘𝑥)
∈ ℝ ∧ π ∈ ℝ) → ((ℑ‘𝑥) < π →
(ℑ‘𝑥) ≤
π)) |
55 | 53, 23, 54 | sylancl 586 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → ((ℑ‘𝑥) < π → (ℑ‘𝑥) ≤ π)) |
56 | 51, 55 | mpd 15 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (ℑ‘𝑥) ≤ π) |
57 | | ellogrn 25724 |
. . . . . . . . 9
⊢ (𝑥 ∈ ran log ↔ (𝑥 ∈ ℂ ∧ -π <
(ℑ‘𝑥) ∧
(ℑ‘𝑥) ≤
π)) |
58 | 47, 50, 56, 57 | syl3anbrc 1342 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → 𝑥
∈ ran log) |
59 | | logef 25746 |
. . . . . . . 8
⊢ (𝑥 ∈ ran log →
(log‘(exp‘𝑥)) =
𝑥) |
60 | 58, 59 | syl 17 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (log‘(exp‘𝑥)) = 𝑥) |
61 | | efcl 15801 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ →
(exp‘𝑥) ∈
ℂ) |
62 | 61 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (exp‘𝑥) ∈ ℂ) |
63 | 53 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℑ‘𝑥) ∈
ℝ) |
64 | 63 | recnd 11012 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℑ‘𝑥) ∈
ℂ) |
65 | | picn 25625 |
. . . . . . . . . . . . . 14
⊢ π
∈ ℂ |
66 | 65 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → π ∈
ℂ) |
67 | | pipos 25626 |
. . . . . . . . . . . . . . 15
⊢ 0 <
π |
68 | 23, 67 | gt0ne0ii 11520 |
. . . . . . . . . . . . . 14
⊢ π ≠
0 |
69 | 68 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → π ≠
0) |
70 | 51 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℑ‘𝑥) < π) |
71 | 65 | mulid1i 10988 |
. . . . . . . . . . . . . . . . . 18
⊢ (π
· 1) = π |
72 | 70, 71 | breqtrrdi 5117 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℑ‘𝑥) < (π ·
1)) |
73 | | 1re 10984 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℝ |
74 | 73 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → 1 ∈
ℝ) |
75 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → π ∈
ℝ) |
76 | 67 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → 0 <
π) |
77 | | ltdivmul 11859 |
. . . . . . . . . . . . . . . . . 18
⊢
(((ℑ‘𝑥)
∈ ℝ ∧ 1 ∈ ℝ ∧ (π ∈ ℝ ∧ 0 <
π)) → (((ℑ‘𝑥) / π) < 1 ↔ (ℑ‘𝑥) < (π ·
1))) |
78 | 63, 74, 75, 76, 77 | syl112anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(((ℑ‘𝑥) / π)
< 1 ↔ (ℑ‘𝑥) < (π · 1))) |
79 | 72, 78 | mpbird 256 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((ℑ‘𝑥) / π)
< 1) |
80 | | 1e0p1 12488 |
. . . . . . . . . . . . . . . 16
⊢ 1 = (0 +
1) |
81 | 79, 80 | breqtrdi 5116 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((ℑ‘𝑥) / π)
< (0 + 1)) |
82 | 63 | recoscld 15862 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(cos‘(ℑ‘𝑥)) ∈ ℝ) |
83 | 63 | resincld 15861 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(sin‘(ℑ‘𝑥)) ∈ ℝ) |
84 | 82, 83 | crimd 14952 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(ℑ‘((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥))))) = (sin‘(ℑ‘𝑥))) |
85 | | efeul 15880 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℂ →
(exp‘𝑥) =
((exp‘(ℜ‘𝑥)) · ((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥)))))) |
86 | 85 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (exp‘𝑥) =
((exp‘(ℜ‘𝑥)) · ((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥)))))) |
87 | 86 | oveq1d 7299 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → ((exp‘𝑥) /
(exp‘(ℜ‘𝑥))) = (((exp‘(ℜ‘𝑥)) ·
((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥))))) / (exp‘(ℜ‘𝑥)))) |
88 | 82 | recnd 11012 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(cos‘(ℑ‘𝑥)) ∈ ℂ) |
89 | | ax-icn 10939 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ i ∈
ℂ |
90 | 83 | recnd 11012 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(sin‘(ℑ‘𝑥)) ∈ ℂ) |
91 | | mulcl 10964 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((i
∈ ℂ ∧ (sin‘(ℑ‘𝑥)) ∈ ℂ) → (i ·
(sin‘(ℑ‘𝑥))) ∈ ℂ) |
92 | 89, 90, 91 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (i ·
(sin‘(ℑ‘𝑥))) ∈ ℂ) |
93 | 88, 92 | addcld 11003 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥)))) ∈ ℂ) |
94 | | recl 14830 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ ℂ →
(ℜ‘𝑥) ∈
ℝ) |
95 | 94 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℜ‘𝑥) ∈
ℝ) |
96 | 95 | recnd 11012 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℜ‘𝑥) ∈
ℂ) |
97 | | efcl 15801 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((ℜ‘𝑥)
∈ ℂ → (exp‘(ℜ‘𝑥)) ∈ ℂ) |
98 | 96, 97 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(exp‘(ℜ‘𝑥)) ∈ ℂ) |
99 | | efne0 15815 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((ℜ‘𝑥)
∈ ℂ → (exp‘(ℜ‘𝑥)) ≠ 0) |
100 | 96, 99 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(exp‘(ℜ‘𝑥)) ≠ 0) |
101 | 93, 98, 100 | divcan3d 11765 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(((exp‘(ℜ‘𝑥)) · ((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥))))) / (exp‘(ℜ‘𝑥))) =
((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥))))) |
102 | 87, 101 | eqtrd 2779 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → ((exp‘𝑥) /
(exp‘(ℜ‘𝑥))) = ((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥))))) |
103 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (exp‘𝑥) ∈
ℝ) |
104 | 95 | reefcld 15806 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(exp‘(ℜ‘𝑥)) ∈ ℝ) |
105 | 103, 104,
100 | redivcld 11812 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → ((exp‘𝑥) /
(exp‘(ℜ‘𝑥))) ∈ ℝ) |
106 | 102, 105 | eqeltrrd 2841 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥)))) ∈ ℝ) |
107 | 106 | reim0d 14945 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(ℑ‘((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥))))) = 0) |
108 | 84, 107 | eqtr3d 2781 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(sin‘(ℑ‘𝑥)) = 0) |
109 | | sineq0 25689 |
. . . . . . . . . . . . . . . . . 18
⊢
((ℑ‘𝑥)
∈ ℂ → ((sin‘(ℑ‘𝑥)) = 0 ↔ ((ℑ‘𝑥) / π) ∈
ℤ)) |
110 | 64, 109 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((sin‘(ℑ‘𝑥)) = 0 ↔ ((ℑ‘𝑥) / π) ∈
ℤ)) |
111 | 108, 110 | mpbid 231 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((ℑ‘𝑥) / π)
∈ ℤ) |
112 | | 0z 12339 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℤ |
113 | | zleltp1 12380 |
. . . . . . . . . . . . . . . 16
⊢
((((ℑ‘𝑥)
/ π) ∈ ℤ ∧ 0 ∈ ℤ) → (((ℑ‘𝑥) / π) ≤ 0 ↔
((ℑ‘𝑥) / π)
< (0 + 1))) |
114 | 111, 112,
113 | sylancl 586 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(((ℑ‘𝑥) / π)
≤ 0 ↔ ((ℑ‘𝑥) / π) < (0 + 1))) |
115 | 81, 114 | mpbird 256 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((ℑ‘𝑥) / π)
≤ 0) |
116 | | df-neg 11217 |
. . . . . . . . . . . . . . . 16
⊢ -1 = (0
− 1) |
117 | 65 | mulm1i 11429 |
. . . . . . . . . . . . . . . . . 18
⊢ (-1
· π) = -π |
118 | 50 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → -π <
(ℑ‘𝑥)) |
119 | 117, 118 | eqbrtrid 5110 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (-1 · π)
< (ℑ‘𝑥)) |
120 | 73 | renegcli 11291 |
. . . . . . . . . . . . . . . . . . 19
⊢ -1 ∈
ℝ |
121 | 120 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → -1 ∈
ℝ) |
122 | | ltmuldiv 11857 |
. . . . . . . . . . . . . . . . . 18
⊢ ((-1
∈ ℝ ∧ (ℑ‘𝑥) ∈ ℝ ∧ (π ∈ ℝ
∧ 0 < π)) → ((-1 · π) < (ℑ‘𝑥) ↔ -1 <
((ℑ‘𝑥) /
π))) |
123 | 121, 63, 75, 76, 122 | syl112anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → ((-1 · π)
< (ℑ‘𝑥)
↔ -1 < ((ℑ‘𝑥) / π))) |
124 | 119, 123 | mpbid 231 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → -1 <
((ℑ‘𝑥) /
π)) |
125 | 116, 124 | eqbrtrrid 5111 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (0 − 1) <
((ℑ‘𝑥) /
π)) |
126 | | zlem1lt 12381 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℤ ∧ ((ℑ‘𝑥) / π) ∈ ℤ) → (0 ≤
((ℑ‘𝑥) / π)
↔ (0 − 1) < ((ℑ‘𝑥) / π))) |
127 | 112, 111,
126 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (0 ≤
((ℑ‘𝑥) / π)
↔ (0 − 1) < ((ℑ‘𝑥) / π))) |
128 | 125, 127 | mpbird 256 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → 0 ≤
((ℑ‘𝑥) /
π)) |
129 | 63, 75, 69 | redivcld 11812 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((ℑ‘𝑥) / π)
∈ ℝ) |
130 | | 0re 10986 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
131 | | letri3 11069 |
. . . . . . . . . . . . . . 15
⊢
((((ℑ‘𝑥)
/ π) ∈ ℝ ∧ 0 ∈ ℝ) → (((ℑ‘𝑥) / π) = 0 ↔
(((ℑ‘𝑥) / π)
≤ 0 ∧ 0 ≤ ((ℑ‘𝑥) / π)))) |
132 | 129, 130,
131 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(((ℑ‘𝑥) / π)
= 0 ↔ (((ℑ‘𝑥) / π) ≤ 0 ∧ 0 ≤
((ℑ‘𝑥) /
π)))) |
133 | 115, 128,
132 | mpbir2and 710 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((ℑ‘𝑥) / π)
= 0) |
134 | 64, 66, 69, 133 | diveq0d 11767 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℑ‘𝑥) = 0) |
135 | | reim0b 14839 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → (𝑥 ∈ ℝ ↔
(ℑ‘𝑥) =
0)) |
136 | 135 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (𝑥 ∈ ℝ ↔ (ℑ‘𝑥) = 0)) |
137 | 134, 136 | mpbird 256 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → 𝑥 ∈ ℝ) |
138 | 137 | rpefcld 15823 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (exp‘𝑥) ∈
ℝ+) |
139 | 138 | ex 413 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → ((exp‘𝑥) ∈ ℝ → (exp‘𝑥) ∈
ℝ+)) |
140 | 4 | ellogdm 25803 |
. . . . . . . . 9
⊢
((exp‘𝑥)
∈ 𝐷 ↔
((exp‘𝑥) ∈
ℂ ∧ ((exp‘𝑥) ∈ ℝ → (exp‘𝑥) ∈
ℝ+))) |
141 | 62, 139, 140 | sylanbrc 583 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (exp‘𝑥) ∈ 𝐷) |
142 | | funfvima2 7116 |
. . . . . . . . 9
⊢ ((Fun log
∧ 𝐷 ⊆ dom log)
→ ((exp‘𝑥)
∈ 𝐷 →
(log‘(exp‘𝑥))
∈ (log “ 𝐷))) |
143 | 9, 13, 142 | mp2an 689 |
. . . . . . . 8
⊢
((exp‘𝑥)
∈ 𝐷 →
(log‘(exp‘𝑥))
∈ (log “ 𝐷)) |
144 | 141, 143 | syl 17 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (log‘(exp‘𝑥)) ∈ (log “ 𝐷)) |
145 | 60, 144 | eqeltrrd 2841 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → 𝑥
∈ (log “ 𝐷)) |
146 | 46, 145 | sylbi 216 |
. . . . 5
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) → 𝑥 ∈ (log “ 𝐷)) |
147 | 146 | ssriv 3926 |
. . . 4
⊢ (◡ℑ “ (-π(,)π)) ⊆ (log
“ 𝐷) |
148 | 44, 147 | eqssi 3938 |
. . 3
⊢ (log
“ 𝐷) = (◡ℑ “
(-π(,)π)) |
149 | | f1oeq3 6715 |
. . 3
⊢ ((log
“ 𝐷) = (◡ℑ “ (-π(,)π)) → ((log
↾ 𝐷):𝐷–1-1-onto→(log
“ 𝐷) ↔ (log
↾ 𝐷):𝐷–1-1-onto→(◡ℑ “
(-π(,)π)))) |
150 | 148, 149 | ax-mp 5 |
. 2
⊢ ((log
↾ 𝐷):𝐷–1-1-onto→(log
“ 𝐷) ↔ (log
↾ 𝐷):𝐷–1-1-onto→(◡ℑ “
(-π(,)π))) |
151 | 7, 150 | mpbi 229 |
1
⊢ (log
↾ 𝐷):𝐷–1-1-onto→(◡ℑ “
(-π(,)π)) |