Step | Hyp | Ref
| Expression |
1 | | logf1o 24356 |
. . . 4
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log |
2 | | f1of1 6174 |
. . . 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 24433 |
. . 3
⊢ 𝐷 ⊆ (ℂ ∖
{0}) |
6 | | f1ores 6189 |
. . 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 6177 |
. . . . . . 7
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → Fun log) |
9 | 1, 8 | ax-mp 5 |
. . . . . 6
⊢ Fun
log |
10 | | f1of 6175 |
. . . . . . . . 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 6090 |
. . . . . . 7
⊢ dom log =
(ℂ ∖ {0}) |
13 | 5, 12 | sseqtr4i 3671 |
. . . . . 6
⊢ 𝐷 ⊆ dom
log |
14 | | funimass4 6286 |
. . . . . 6
⊢ ((Fun log
∧ 𝐷 ⊆ dom log)
→ ((log “ 𝐷)
⊆ (◡ℑ “
(-π(,)π)) ↔ ∀𝑥 ∈ 𝐷 (log‘𝑥) ∈ (◡ℑ “
(-π(,)π)))) |
15 | 9, 13, 14 | mp2an 708 |
. . . . 5
⊢ ((log
“ 𝐷) ⊆ (◡ℑ “ (-π(,)π)) ↔
∀𝑥 ∈ 𝐷 (log‘𝑥) ∈ (◡ℑ “
(-π(,)π))) |
16 | 4 | ellogdm 24430 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ ℂ ∧ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ+))) |
17 | 16 | simplbi 475 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ) |
18 | 4 | logdmn0 24431 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → 𝑥 ≠ 0) |
19 | 17, 18 | logcld 24362 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (log‘𝑥) ∈ ℂ) |
20 | 19 | imcld 13979 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ∈
ℝ) |
21 | 17, 18 | logimcld 24363 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (-π <
(ℑ‘(log‘𝑥)) ∧ (ℑ‘(log‘𝑥)) ≤ π)) |
22 | 21 | simpld 474 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → -π <
(ℑ‘(log‘𝑥))) |
23 | 4 | logdmnrp 24432 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → ¬ -𝑥 ∈ ℝ+) |
24 | | lognegb 24381 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (-𝑥 ∈ ℝ+
↔ (ℑ‘(log‘𝑥)) = π)) |
25 | 17, 18, 24 | syl2anc 694 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → (-𝑥 ∈ ℝ+ ↔
(ℑ‘(log‘𝑥)) = π)) |
26 | 25 | necon3bbid 2860 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → (¬ -𝑥 ∈ ℝ+ ↔
(ℑ‘(log‘𝑥)) ≠ π)) |
27 | 23, 26 | mpbid 222 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ≠ π) |
28 | 27 | necomd 2878 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → π ≠
(ℑ‘(log‘𝑥))) |
29 | | pire 24255 |
. . . . . . . . . 10
⊢ π
∈ ℝ |
30 | 29 | a1i 11 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → π ∈
ℝ) |
31 | 21 | simprd 478 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ≤ π) |
32 | 20, 30, 31 | leltned 10228 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → ((ℑ‘(log‘𝑥)) < π ↔ π ≠
(ℑ‘(log‘𝑥)))) |
33 | 28, 32 | mpbird 247 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) < π) |
34 | 29 | renegcli 10380 |
. . . . . . . . 9
⊢ -π
∈ ℝ |
35 | 34 | rexri 10135 |
. . . . . . . 8
⊢ -π
∈ ℝ* |
36 | 29 | rexri 10135 |
. . . . . . . 8
⊢ π
∈ ℝ* |
37 | | elioo2 12254 |
. . . . . . . 8
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ*) →
((ℑ‘(log‘𝑥)) ∈ (-π(,)π) ↔
((ℑ‘(log‘𝑥)) ∈ ℝ ∧ -π <
(ℑ‘(log‘𝑥)) ∧ (ℑ‘(log‘𝑥)) < π))) |
38 | 35, 36, 37 | mp2an 708 |
. . . . . . 7
⊢
((ℑ‘(log‘𝑥)) ∈ (-π(,)π) ↔
((ℑ‘(log‘𝑥)) ∈ ℝ ∧ -π <
(ℑ‘(log‘𝑥)) ∧ (ℑ‘(log‘𝑥)) < π)) |
39 | 20, 22, 33, 38 | syl3anbrc 1265 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ∈
(-π(,)π)) |
40 | | imf 13897 |
. . . . . . 7
⊢
ℑ:ℂ⟶ℝ |
41 | | ffn 6083 |
. . . . . . 7
⊢
(ℑ:ℂ⟶ℝ → ℑ Fn
ℂ) |
42 | | elpreima 6377 |
. . . . . . 7
⊢ (ℑ
Fn ℂ → ((log‘𝑥) ∈ (◡ℑ “ (-π(,)π)) ↔
((log‘𝑥) ∈
ℂ ∧ (ℑ‘(log‘𝑥)) ∈ (-π(,)π)))) |
43 | 40, 41, 42 | mp2b 10 |
. . . . . 6
⊢
((log‘𝑥)
∈ (◡ℑ “
(-π(,)π)) ↔ ((log‘𝑥) ∈ ℂ ∧
(ℑ‘(log‘𝑥)) ∈ (-π(,)π))) |
44 | 19, 39, 43 | sylanbrc 699 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (log‘𝑥) ∈ (◡ℑ “
(-π(,)π))) |
45 | 15, 44 | mprgbir 2956 |
. . . 4
⊢ (log
“ 𝐷) ⊆ (◡ℑ “
(-π(,)π)) |
46 | | elpreima 6377 |
. . . . . . 7
⊢ (ℑ
Fn ℂ → (𝑥 ∈
(◡ℑ “ (-π(,)π))
↔ (𝑥 ∈ ℂ
∧ (ℑ‘𝑥)
∈ (-π(,)π)))) |
47 | 40, 41, 46 | mp2b 10 |
. . . . . 6
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) ↔
(𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π))) |
48 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → 𝑥
∈ ℂ) |
49 | | eliooord 12271 |
. . . . . . . . . . 11
⊢
((ℑ‘𝑥)
∈ (-π(,)π) → (-π < (ℑ‘𝑥) ∧ (ℑ‘𝑥) < π)) |
50 | 49 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (-π < (ℑ‘𝑥) ∧ (ℑ‘𝑥) < π)) |
51 | 50 | simpld 474 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → -π < (ℑ‘𝑥)) |
52 | 50 | simprd 478 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (ℑ‘𝑥) < π) |
53 | | imcl 13895 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ →
(ℑ‘𝑥) ∈
ℝ) |
54 | 53 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (ℑ‘𝑥) ∈ ℝ) |
55 | | ltle 10164 |
. . . . . . . . . . 11
⊢
(((ℑ‘𝑥)
∈ ℝ ∧ π ∈ ℝ) → ((ℑ‘𝑥) < π →
(ℑ‘𝑥) ≤
π)) |
56 | 54, 29, 55 | sylancl 695 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → ((ℑ‘𝑥) < π → (ℑ‘𝑥) ≤ π)) |
57 | 52, 56 | mpd 15 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (ℑ‘𝑥) ≤ π) |
58 | | ellogrn 24351 |
. . . . . . . . 9
⊢ (𝑥 ∈ ran log ↔ (𝑥 ∈ ℂ ∧ -π <
(ℑ‘𝑥) ∧
(ℑ‘𝑥) ≤
π)) |
59 | 48, 51, 57, 58 | syl3anbrc 1265 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → 𝑥
∈ ran log) |
60 | | logef 24373 |
. . . . . . . 8
⊢ (𝑥 ∈ ran log →
(log‘(exp‘𝑥)) =
𝑥) |
61 | 59, 60 | syl 17 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (log‘(exp‘𝑥)) = 𝑥) |
62 | | efcl 14857 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ →
(exp‘𝑥) ∈
ℂ) |
63 | 62 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (exp‘𝑥) ∈ ℂ) |
64 | 54 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℑ‘𝑥) ∈
ℝ) |
65 | 64 | recnd 10106 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℑ‘𝑥) ∈
ℂ) |
66 | | picn 24256 |
. . . . . . . . . . . . . 14
⊢ π
∈ ℂ |
67 | 66 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → π ∈
ℂ) |
68 | | pipos 24257 |
. . . . . . . . . . . . . . 15
⊢ 0 <
π |
69 | 29, 68 | gt0ne0ii 10602 |
. . . . . . . . . . . . . 14
⊢ π ≠
0 |
70 | 69 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → π ≠
0) |
71 | 52 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℑ‘𝑥) < π) |
72 | 66 | mulid1i 10080 |
. . . . . . . . . . . . . . . . . 18
⊢ (π
· 1) = π |
73 | 71, 72 | syl6breqr 4727 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℑ‘𝑥) < (π ·
1)) |
74 | | 1re 10077 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℝ |
75 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → 1 ∈
ℝ) |
76 | 29 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → π ∈
ℝ) |
77 | 68 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → 0 <
π) |
78 | | ltdivmul 10936 |
. . . . . . . . . . . . . . . . . 18
⊢
(((ℑ‘𝑥)
∈ ℝ ∧ 1 ∈ ℝ ∧ (π ∈ ℝ ∧ 0 <
π)) → (((ℑ‘𝑥) / π) < 1 ↔ (ℑ‘𝑥) < (π ·
1))) |
79 | 64, 75, 76, 77, 78 | syl112anc 1370 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(((ℑ‘𝑥) / π)
< 1 ↔ (ℑ‘𝑥) < (π · 1))) |
80 | 73, 79 | mpbird 247 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((ℑ‘𝑥) / π)
< 1) |
81 | | 1e0p1 11590 |
. . . . . . . . . . . . . . . 16
⊢ 1 = (0 +
1) |
82 | 80, 81 | syl6breq 4726 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((ℑ‘𝑥) / π)
< (0 + 1)) |
83 | 64 | recoscld 14918 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(cos‘(ℑ‘𝑥)) ∈ ℝ) |
84 | 64 | resincld 14917 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(sin‘(ℑ‘𝑥)) ∈ ℝ) |
85 | 83, 84 | crimd 14016 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(ℑ‘((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥))))) = (sin‘(ℑ‘𝑥))) |
86 | | efeul 14936 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℂ →
(exp‘𝑥) =
((exp‘(ℜ‘𝑥)) · ((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥)))))) |
87 | 86 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (exp‘𝑥) =
((exp‘(ℜ‘𝑥)) · ((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥)))))) |
88 | 87 | oveq1d 6705 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → ((exp‘𝑥) /
(exp‘(ℜ‘𝑥))) = (((exp‘(ℜ‘𝑥)) ·
((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥))))) / (exp‘(ℜ‘𝑥)))) |
89 | 83 | recnd 10106 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(cos‘(ℑ‘𝑥)) ∈ ℂ) |
90 | | ax-icn 10033 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ i ∈
ℂ |
91 | 84 | recnd 10106 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(sin‘(ℑ‘𝑥)) ∈ ℂ) |
92 | | mulcl 10058 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((i
∈ ℂ ∧ (sin‘(ℑ‘𝑥)) ∈ ℂ) → (i ·
(sin‘(ℑ‘𝑥))) ∈ ℂ) |
93 | 90, 91, 92 | sylancr 696 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (i ·
(sin‘(ℑ‘𝑥))) ∈ ℂ) |
94 | 89, 93 | addcld 10097 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥)))) ∈ ℂ) |
95 | | recl 13894 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ ℂ →
(ℜ‘𝑥) ∈
ℝ) |
96 | 95 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℜ‘𝑥) ∈
ℝ) |
97 | 96 | recnd 10106 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℜ‘𝑥) ∈
ℂ) |
98 | | efcl 14857 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((ℜ‘𝑥)
∈ ℂ → (exp‘(ℜ‘𝑥)) ∈ ℂ) |
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(exp‘(ℜ‘𝑥)) ∈ ℂ) |
100 | | efne0 14871 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((ℜ‘𝑥)
∈ ℂ → (exp‘(ℜ‘𝑥)) ≠ 0) |
101 | 97, 100 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(exp‘(ℜ‘𝑥)) ≠ 0) |
102 | 94, 99, 101 | divcan3d 10844 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(((exp‘(ℜ‘𝑥)) · ((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥))))) / (exp‘(ℜ‘𝑥))) =
((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥))))) |
103 | 88, 102 | eqtrd 2685 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → ((exp‘𝑥) /
(exp‘(ℜ‘𝑥))) = ((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥))))) |
104 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (exp‘𝑥) ∈
ℝ) |
105 | 96 | reefcld 14862 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(exp‘(ℜ‘𝑥)) ∈ ℝ) |
106 | 104, 105,
101 | redivcld 10891 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → ((exp‘𝑥) /
(exp‘(ℜ‘𝑥))) ∈ ℝ) |
107 | 103, 106 | eqeltrrd 2731 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥)))) ∈ ℝ) |
108 | 107 | reim0d 14009 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(ℑ‘((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥))))) = 0) |
109 | 85, 108 | eqtr3d 2687 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(sin‘(ℑ‘𝑥)) = 0) |
110 | | sineq0 24318 |
. . . . . . . . . . . . . . . . . 18
⊢
((ℑ‘𝑥)
∈ ℂ → ((sin‘(ℑ‘𝑥)) = 0 ↔ ((ℑ‘𝑥) / π) ∈
ℤ)) |
111 | 65, 110 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((sin‘(ℑ‘𝑥)) = 0 ↔ ((ℑ‘𝑥) / π) ∈
ℤ)) |
112 | 109, 111 | mpbid 222 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((ℑ‘𝑥) / π)
∈ ℤ) |
113 | | 0z 11426 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℤ |
114 | | zleltp1 11466 |
. . . . . . . . . . . . . . . 16
⊢
((((ℑ‘𝑥)
/ π) ∈ ℤ ∧ 0 ∈ ℤ) → (((ℑ‘𝑥) / π) ≤ 0 ↔
((ℑ‘𝑥) / π)
< (0 + 1))) |
115 | 112, 113,
114 | sylancl 695 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(((ℑ‘𝑥) / π)
≤ 0 ↔ ((ℑ‘𝑥) / π) < (0 + 1))) |
116 | 82, 115 | mpbird 247 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((ℑ‘𝑥) / π)
≤ 0) |
117 | | df-neg 10307 |
. . . . . . . . . . . . . . . 16
⊢ -1 = (0
− 1) |
118 | 66 | mulm1i 10513 |
. . . . . . . . . . . . . . . . . 18
⊢ (-1
· π) = -π |
119 | 51 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → -π <
(ℑ‘𝑥)) |
120 | 118, 119 | syl5eqbr 4720 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (-1 · π)
< (ℑ‘𝑥)) |
121 | 74 | renegcli 10380 |
. . . . . . . . . . . . . . . . . . 19
⊢ -1 ∈
ℝ |
122 | 121 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → -1 ∈
ℝ) |
123 | | ltmuldiv 10934 |
. . . . . . . . . . . . . . . . . 18
⊢ ((-1
∈ ℝ ∧ (ℑ‘𝑥) ∈ ℝ ∧ (π ∈ ℝ
∧ 0 < π)) → ((-1 · π) < (ℑ‘𝑥) ↔ -1 <
((ℑ‘𝑥) /
π))) |
124 | 122, 64, 76, 77, 123 | syl112anc 1370 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → ((-1 · π)
< (ℑ‘𝑥)
↔ -1 < ((ℑ‘𝑥) / π))) |
125 | 120, 124 | mpbid 222 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → -1 <
((ℑ‘𝑥) /
π)) |
126 | 117, 125 | syl5eqbrr 4721 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (0 − 1) <
((ℑ‘𝑥) /
π)) |
127 | | zlem1lt 11467 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℤ ∧ ((ℑ‘𝑥) / π) ∈ ℤ) → (0 ≤
((ℑ‘𝑥) / π)
↔ (0 − 1) < ((ℑ‘𝑥) / π))) |
128 | 113, 112,
127 | sylancr 696 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (0 ≤
((ℑ‘𝑥) / π)
↔ (0 − 1) < ((ℑ‘𝑥) / π))) |
129 | 126, 128 | mpbird 247 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → 0 ≤
((ℑ‘𝑥) /
π)) |
130 | 64, 76, 70 | redivcld 10891 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((ℑ‘𝑥) / π)
∈ ℝ) |
131 | | 0re 10078 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
132 | | letri3 10161 |
. . . . . . . . . . . . . . 15
⊢
((((ℑ‘𝑥)
/ π) ∈ ℝ ∧ 0 ∈ ℝ) → (((ℑ‘𝑥) / π) = 0 ↔
(((ℑ‘𝑥) / π)
≤ 0 ∧ 0 ≤ ((ℑ‘𝑥) / π)))) |
133 | 130, 131,
132 | sylancl 695 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(((ℑ‘𝑥) / π)
= 0 ↔ (((ℑ‘𝑥) / π) ≤ 0 ∧ 0 ≤
((ℑ‘𝑥) /
π)))) |
134 | 116, 129,
133 | mpbir2and 977 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((ℑ‘𝑥) / π)
= 0) |
135 | 65, 67, 70, 134 | diveq0d 10846 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℑ‘𝑥) = 0) |
136 | | reim0b 13903 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → (𝑥 ∈ ℝ ↔
(ℑ‘𝑥) =
0)) |
137 | 136 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (𝑥 ∈ ℝ ↔ (ℑ‘𝑥) = 0)) |
138 | 135, 137 | mpbird 247 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → 𝑥 ∈ ℝ) |
139 | 138 | rpefcld 14879 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (exp‘𝑥) ∈
ℝ+) |
140 | 139 | ex 449 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → ((exp‘𝑥) ∈ ℝ → (exp‘𝑥) ∈
ℝ+)) |
141 | 4 | ellogdm 24430 |
. . . . . . . . 9
⊢
((exp‘𝑥)
∈ 𝐷 ↔
((exp‘𝑥) ∈
ℂ ∧ ((exp‘𝑥) ∈ ℝ → (exp‘𝑥) ∈
ℝ+))) |
142 | 63, 140, 141 | sylanbrc 699 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (exp‘𝑥) ∈ 𝐷) |
143 | | funfvima2 6533 |
. . . . . . . . 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 2731 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → 𝑥
∈ (log “ 𝐷)) |
147 | 47, 146 | sylbi 207 |
. . . . 5
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) → 𝑥 ∈ (log “ 𝐷)) |
148 | 147 | ssriv 3640 |
. . . 4
⊢ (◡ℑ “ (-π(,)π)) ⊆ (log
“ 𝐷) |
149 | 45, 148 | eqssi 3652 |
. . 3
⊢ (log
“ 𝐷) = (◡ℑ “
(-π(,)π)) |
150 | | f1oeq3 6167 |
. . 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→(◡ℑ “
(-π(,)π)) |