| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | logf1o 26607 | . . . 4
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log | 
| 2 |  | f1of1 6846 | . . . 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 26685 | . . 3
⊢ 𝐷 ⊆ (ℂ ∖
{0}) | 
| 6 |  | f1ores 6861 | . . 3
⊢
((log:(ℂ ∖ {0})–1-1→ran log ∧ 𝐷 ⊆ (ℂ ∖ {0})) → (log
↾ 𝐷):𝐷–1-1-onto→(log
“ 𝐷)) | 
| 7 | 3, 5, 6 | mp2an 692 | . 2
⊢ (log
↾ 𝐷):𝐷–1-1-onto→(log
“ 𝐷) | 
| 8 |  | f1ofun 6849 | . . . . . . 7
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → Fun log) | 
| 9 | 1, 8 | ax-mp 5 | . . . . . 6
⊢ Fun
log | 
| 10 |  | f1of 6847 | . . . . . . . . 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 6746 | . . . . . . 7
⊢ dom log =
(ℂ ∖ {0}) | 
| 13 | 5, 12 | sseqtrri 4032 | . . . . . 6
⊢ 𝐷 ⊆ dom
log | 
| 14 |  | funimass4 6972 | . . . . . 6
⊢ ((Fun log
∧ 𝐷 ⊆ dom log)
→ ((log “ 𝐷)
⊆ (◡ℑ “
(-π(,)π)) ↔ ∀𝑥 ∈ 𝐷 (log‘𝑥) ∈ (◡ℑ “
(-π(,)π)))) | 
| 15 | 9, 13, 14 | mp2an 692 | . . . . 5
⊢ ((log
“ 𝐷) ⊆ (◡ℑ “ (-π(,)π)) ↔
∀𝑥 ∈ 𝐷 (log‘𝑥) ∈ (◡ℑ “
(-π(,)π))) | 
| 16 | 4 | ellogdm 26682 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ ℂ ∧ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ+))) | 
| 17 | 16 | simplbi 497 | . . . . . . 7
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ) | 
| 18 | 4 | logdmn0 26683 | . . . . . . 7
⊢ (𝑥 ∈ 𝐷 → 𝑥 ≠ 0) | 
| 19 | 17, 18 | logcld 26613 | . . . . . 6
⊢ (𝑥 ∈ 𝐷 → (log‘𝑥) ∈ ℂ) | 
| 20 | 19 | imcld 15235 | . . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ∈
ℝ) | 
| 21 | 17, 18 | logimcld 26614 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (-π <
(ℑ‘(log‘𝑥)) ∧ (ℑ‘(log‘𝑥)) ≤ π)) | 
| 22 | 21 | simpld 494 | . . . . . . 7
⊢ (𝑥 ∈ 𝐷 → -π <
(ℑ‘(log‘𝑥))) | 
| 23 |  | pire 26501 | . . . . . . . . 9
⊢ π
∈ ℝ | 
| 24 | 23 | a1i 11 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → π ∈
ℝ) | 
| 25 | 21 | simprd 495 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ≤ π) | 
| 26 | 4 | logdmnrp 26684 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → ¬ -𝑥 ∈ ℝ+) | 
| 27 |  | lognegb 26633 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (-𝑥 ∈ ℝ+
↔ (ℑ‘(log‘𝑥)) = π)) | 
| 28 | 17, 18, 27 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → (-𝑥 ∈ ℝ+ ↔
(ℑ‘(log‘𝑥)) = π)) | 
| 29 | 28 | necon3bbid 2977 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → (¬ -𝑥 ∈ ℝ+ ↔
(ℑ‘(log‘𝑥)) ≠ π)) | 
| 30 | 26, 29 | mpbid 232 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ≠ π) | 
| 31 | 30 | necomd 2995 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → π ≠
(ℑ‘(log‘𝑥))) | 
| 32 | 20, 24, 25, 31 | leneltd 11416 | . . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) < π) | 
| 33 | 23 | renegcli 11571 | . . . . . . . . 9
⊢ -π
∈ ℝ | 
| 34 | 33 | rexri 11320 | . . . . . . . 8
⊢ -π
∈ ℝ* | 
| 35 | 23 | rexri 11320 | . . . . . . . 8
⊢ π
∈ ℝ* | 
| 36 |  | elioo2 13429 | . . . . . . . 8
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ*) →
((ℑ‘(log‘𝑥)) ∈ (-π(,)π) ↔
((ℑ‘(log‘𝑥)) ∈ ℝ ∧ -π <
(ℑ‘(log‘𝑥)) ∧ (ℑ‘(log‘𝑥)) < π))) | 
| 37 | 34, 35, 36 | mp2an 692 | . . . . . . 7
⊢
((ℑ‘(log‘𝑥)) ∈ (-π(,)π) ↔
((ℑ‘(log‘𝑥)) ∈ ℝ ∧ -π <
(ℑ‘(log‘𝑥)) ∧ (ℑ‘(log‘𝑥)) < π)) | 
| 38 | 20, 22, 32, 37 | syl3anbrc 1343 | . . . . . 6
⊢ (𝑥 ∈ 𝐷 → (ℑ‘(log‘𝑥)) ∈
(-π(,)π)) | 
| 39 |  | imf 15153 | . . . . . . 7
⊢
ℑ:ℂ⟶ℝ | 
| 40 |  | ffn 6735 | . . . . . . 7
⊢
(ℑ:ℂ⟶ℝ → ℑ Fn
ℂ) | 
| 41 |  | elpreima 7077 | . . . . . . 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 3067 | . . . 4
⊢ (log
“ 𝐷) ⊆ (◡ℑ “
(-π(,)π)) | 
| 45 |  | elpreima 7077 | . . . . . . 7
⊢ (ℑ
Fn ℂ → (𝑥 ∈
(◡ℑ “ (-π(,)π))
↔ (𝑥 ∈ ℂ
∧ (ℑ‘𝑥)
∈ (-π(,)π)))) | 
| 46 | 39, 40, 45 | mp2b 10 | . . . . . 6
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) ↔
(𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π))) | 
| 47 |  | simpl 482 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → 𝑥
∈ ℂ) | 
| 48 |  | eliooord 13447 | . . . . . . . . . . 11
⊢
((ℑ‘𝑥)
∈ (-π(,)π) → (-π < (ℑ‘𝑥) ∧ (ℑ‘𝑥) < π)) | 
| 49 | 48 | adantl 481 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (-π < (ℑ‘𝑥) ∧ (ℑ‘𝑥) < π)) | 
| 50 | 49 | simpld 494 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → -π < (ℑ‘𝑥)) | 
| 51 | 49 | simprd 495 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (ℑ‘𝑥) < π) | 
| 52 |  | imcl 15151 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ →
(ℑ‘𝑥) ∈
ℝ) | 
| 53 | 52 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (ℑ‘𝑥) ∈ ℝ) | 
| 54 |  | ltle 11350 | . . . . . . . . . . 11
⊢
(((ℑ‘𝑥)
∈ ℝ ∧ π ∈ ℝ) → ((ℑ‘𝑥) < π →
(ℑ‘𝑥) ≤
π)) | 
| 55 | 53, 23, 54 | sylancl 586 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → ((ℑ‘𝑥) < π → (ℑ‘𝑥) ≤ π)) | 
| 56 | 51, 55 | mpd 15 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (ℑ‘𝑥) ≤ π) | 
| 57 |  | ellogrn 26602 | . . . . . . . . 9
⊢ (𝑥 ∈ ran log ↔ (𝑥 ∈ ℂ ∧ -π <
(ℑ‘𝑥) ∧
(ℑ‘𝑥) ≤
π)) | 
| 58 | 47, 50, 56, 57 | syl3anbrc 1343 | . . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → 𝑥
∈ ran log) | 
| 59 |  | logef 26624 | . . . . . . . 8
⊢ (𝑥 ∈ ran log →
(log‘(exp‘𝑥)) =
𝑥) | 
| 60 | 58, 59 | syl 17 | . . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (log‘(exp‘𝑥)) = 𝑥) | 
| 61 |  | efcl 16119 | . . . . . . . . . 10
⊢ (𝑥 ∈ ℂ →
(exp‘𝑥) ∈
ℂ) | 
| 62 | 61 | adantr 480 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (exp‘𝑥) ∈ ℂ) | 
| 63 | 53 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℑ‘𝑥) ∈
ℝ) | 
| 64 | 63 | recnd 11290 | . . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℑ‘𝑥) ∈
ℂ) | 
| 65 |  | picn 26502 | . . . . . . . . . . . . . 14
⊢ π
∈ ℂ | 
| 66 | 65 | a1i 11 | . . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → π ∈
ℂ) | 
| 67 |  | pipos 26503 | . . . . . . . . . . . . . . 15
⊢ 0 <
π | 
| 68 | 23, 67 | gt0ne0ii 11800 | . . . . . . . . . . . . . 14
⊢ π ≠
0 | 
| 69 | 68 | a1i 11 | . . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → π ≠
0) | 
| 70 | 51 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℑ‘𝑥) < π) | 
| 71 | 65 | mulridi 11266 | . . . . . . . . . . . . . . . . . 18
⊢ (π
· 1) = π | 
| 72 | 70, 71 | breqtrrdi 5184 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℑ‘𝑥) < (π ·
1)) | 
| 73 |  | 1re 11262 | . . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℝ | 
| 74 | 73 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → 1 ∈
ℝ) | 
| 75 | 23 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → π ∈
ℝ) | 
| 76 | 67 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → 0 <
π) | 
| 77 |  | ltdivmul 12144 | . . . . . . . . . . . . . . . . . 18
⊢
(((ℑ‘𝑥)
∈ ℝ ∧ 1 ∈ ℝ ∧ (π ∈ ℝ ∧ 0 <
π)) → (((ℑ‘𝑥) / π) < 1 ↔ (ℑ‘𝑥) < (π ·
1))) | 
| 78 | 63, 74, 75, 76, 77 | syl112anc 1375 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(((ℑ‘𝑥) / π)
< 1 ↔ (ℑ‘𝑥) < (π · 1))) | 
| 79 | 72, 78 | mpbird 257 | . . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((ℑ‘𝑥) / π)
< 1) | 
| 80 |  | 1e0p1 12777 | . . . . . . . . . . . . . . . 16
⊢ 1 = (0 +
1) | 
| 81 | 79, 80 | breqtrdi 5183 | . . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((ℑ‘𝑥) / π)
< (0 + 1)) | 
| 82 | 63 | recoscld 16181 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(cos‘(ℑ‘𝑥)) ∈ ℝ) | 
| 83 | 63 | resincld 16180 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(sin‘(ℑ‘𝑥)) ∈ ℝ) | 
| 84 | 82, 83 | crimd 15272 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(ℑ‘((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥))))) = (sin‘(ℑ‘𝑥))) | 
| 85 |  | efeul 16199 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℂ →
(exp‘𝑥) =
((exp‘(ℜ‘𝑥)) · ((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥)))))) | 
| 86 | 85 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (exp‘𝑥) =
((exp‘(ℜ‘𝑥)) · ((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥)))))) | 
| 87 | 86 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → ((exp‘𝑥) /
(exp‘(ℜ‘𝑥))) = (((exp‘(ℜ‘𝑥)) ·
((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥))))) / (exp‘(ℜ‘𝑥)))) | 
| 88 | 82 | recnd 11290 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(cos‘(ℑ‘𝑥)) ∈ ℂ) | 
| 89 |  | ax-icn 11215 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ i ∈
ℂ | 
| 90 | 83 | recnd 11290 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(sin‘(ℑ‘𝑥)) ∈ ℂ) | 
| 91 |  | mulcl 11240 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((i
∈ ℂ ∧ (sin‘(ℑ‘𝑥)) ∈ ℂ) → (i ·
(sin‘(ℑ‘𝑥))) ∈ ℂ) | 
| 92 | 89, 90, 91 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (i ·
(sin‘(ℑ‘𝑥))) ∈ ℂ) | 
| 93 | 88, 92 | addcld 11281 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥)))) ∈ ℂ) | 
| 94 |  | recl 15150 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ ℂ →
(ℜ‘𝑥) ∈
ℝ) | 
| 95 | 94 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℜ‘𝑥) ∈
ℝ) | 
| 96 | 95 | recnd 11290 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℜ‘𝑥) ∈
ℂ) | 
| 97 |  | efcl 16119 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((ℜ‘𝑥)
∈ ℂ → (exp‘(ℜ‘𝑥)) ∈ ℂ) | 
| 98 | 96, 97 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(exp‘(ℜ‘𝑥)) ∈ ℂ) | 
| 99 |  | efne0 16134 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((ℜ‘𝑥)
∈ ℂ → (exp‘(ℜ‘𝑥)) ≠ 0) | 
| 100 | 96, 99 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(exp‘(ℜ‘𝑥)) ≠ 0) | 
| 101 | 93, 98, 100 | divcan3d 12049 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(((exp‘(ℜ‘𝑥)) · ((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥))))) / (exp‘(ℜ‘𝑥))) =
((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥))))) | 
| 102 | 87, 101 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → ((exp‘𝑥) /
(exp‘(ℜ‘𝑥))) = ((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥))))) | 
| 103 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (exp‘𝑥) ∈
ℝ) | 
| 104 | 95 | reefcld 16125 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(exp‘(ℜ‘𝑥)) ∈ ℝ) | 
| 105 | 103, 104,
100 | redivcld 12096 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → ((exp‘𝑥) /
(exp‘(ℜ‘𝑥))) ∈ ℝ) | 
| 106 | 102, 105 | eqeltrrd 2841 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥)))) ∈ ℝ) | 
| 107 | 106 | reim0d 15265 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(ℑ‘((cos‘(ℑ‘𝑥)) + (i ·
(sin‘(ℑ‘𝑥))))) = 0) | 
| 108 | 84, 107 | eqtr3d 2778 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(sin‘(ℑ‘𝑥)) = 0) | 
| 109 |  | sineq0 26567 | . . . . . . . . . . . . . . . . . 18
⊢
((ℑ‘𝑥)
∈ ℂ → ((sin‘(ℑ‘𝑥)) = 0 ↔ ((ℑ‘𝑥) / π) ∈
ℤ)) | 
| 110 | 64, 109 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((sin‘(ℑ‘𝑥)) = 0 ↔ ((ℑ‘𝑥) / π) ∈
ℤ)) | 
| 111 | 108, 110 | mpbid 232 | . . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((ℑ‘𝑥) / π)
∈ ℤ) | 
| 112 |  | 0z 12626 | . . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℤ | 
| 113 |  | zleltp1 12670 | . . . . . . . . . . . . . . . 16
⊢
((((ℑ‘𝑥)
/ π) ∈ ℤ ∧ 0 ∈ ℤ) → (((ℑ‘𝑥) / π) ≤ 0 ↔
((ℑ‘𝑥) / π)
< (0 + 1))) | 
| 114 | 111, 112,
113 | sylancl 586 | . . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(((ℑ‘𝑥) / π)
≤ 0 ↔ ((ℑ‘𝑥) / π) < (0 + 1))) | 
| 115 | 81, 114 | mpbird 257 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((ℑ‘𝑥) / π)
≤ 0) | 
| 116 |  | df-neg 11496 | . . . . . . . . . . . . . . . 16
⊢ -1 = (0
− 1) | 
| 117 | 65 | mulm1i 11709 | . . . . . . . . . . . . . . . . . 18
⊢ (-1
· π) = -π | 
| 118 | 50 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → -π <
(ℑ‘𝑥)) | 
| 119 | 117, 118 | eqbrtrid 5177 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (-1 · π)
< (ℑ‘𝑥)) | 
| 120 | 73 | renegcli 11571 | . . . . . . . . . . . . . . . . . . 19
⊢ -1 ∈
ℝ | 
| 121 | 120 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → -1 ∈
ℝ) | 
| 122 |  | ltmuldiv 12142 | . . . . . . . . . . . . . . . . . 18
⊢ ((-1
∈ ℝ ∧ (ℑ‘𝑥) ∈ ℝ ∧ (π ∈ ℝ
∧ 0 < π)) → ((-1 · π) < (ℑ‘𝑥) ↔ -1 <
((ℑ‘𝑥) /
π))) | 
| 123 | 121, 63, 75, 76, 122 | syl112anc 1375 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → ((-1 · π)
< (ℑ‘𝑥)
↔ -1 < ((ℑ‘𝑥) / π))) | 
| 124 | 119, 123 | mpbid 232 | . . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → -1 <
((ℑ‘𝑥) /
π)) | 
| 125 | 116, 124 | eqbrtrrid 5178 | . . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (0 − 1) <
((ℑ‘𝑥) /
π)) | 
| 126 |  | zlem1lt 12671 | . . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℤ ∧ ((ℑ‘𝑥) / π) ∈ ℤ) → (0 ≤
((ℑ‘𝑥) / π)
↔ (0 − 1) < ((ℑ‘𝑥) / π))) | 
| 127 | 112, 111,
126 | sylancr 587 | . . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (0 ≤
((ℑ‘𝑥) / π)
↔ (0 − 1) < ((ℑ‘𝑥) / π))) | 
| 128 | 125, 127 | mpbird 257 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → 0 ≤
((ℑ‘𝑥) /
π)) | 
| 129 | 63, 75, 69 | redivcld 12096 | . . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((ℑ‘𝑥) / π)
∈ ℝ) | 
| 130 |  | 0re 11264 | . . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ | 
| 131 |  | letri3 11347 | . . . . . . . . . . . . . . 15
⊢
((((ℑ‘𝑥)
/ π) ∈ ℝ ∧ 0 ∈ ℝ) → (((ℑ‘𝑥) / π) = 0 ↔
(((ℑ‘𝑥) / π)
≤ 0 ∧ 0 ≤ ((ℑ‘𝑥) / π)))) | 
| 132 | 129, 130,
131 | sylancl 586 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
(((ℑ‘𝑥) / π)
= 0 ↔ (((ℑ‘𝑥) / π) ≤ 0 ∧ 0 ≤
((ℑ‘𝑥) /
π)))) | 
| 133 | 115, 128,
132 | mpbir2and 713 | . . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) →
((ℑ‘𝑥) / π)
= 0) | 
| 134 | 64, 66, 69, 133 | diveq0d 12051 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (ℑ‘𝑥) = 0) | 
| 135 |  | reim0b 15159 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → (𝑥 ∈ ℝ ↔
(ℑ‘𝑥) =
0)) | 
| 136 | 135 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (𝑥 ∈ ℝ ↔ (ℑ‘𝑥) = 0)) | 
| 137 | 134, 136 | mpbird 257 | . . . . . . . . . . 11
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → 𝑥 ∈ ℝ) | 
| 138 | 137 | rpefcld 16142 | . . . . . . . . . 10
⊢ (((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) ∧ (exp‘𝑥) ∈ ℝ) → (exp‘𝑥) ∈
ℝ+) | 
| 139 | 138 | ex 412 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → ((exp‘𝑥) ∈ ℝ → (exp‘𝑥) ∈
ℝ+)) | 
| 140 | 4 | ellogdm 26682 | . . . . . . . . 9
⊢
((exp‘𝑥)
∈ 𝐷 ↔
((exp‘𝑥) ∈
ℂ ∧ ((exp‘𝑥) ∈ ℝ → (exp‘𝑥) ∈
ℝ+))) | 
| 141 | 62, 139, 140 | sylanbrc 583 | . . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧
(ℑ‘𝑥) ∈
(-π(,)π)) → (exp‘𝑥) ∈ 𝐷) | 
| 142 |  | funfvima2 7252 | . . . . . . . . 9
⊢ ((Fun log
∧ 𝐷 ⊆ dom log)
→ ((exp‘𝑥)
∈ 𝐷 →
(log‘(exp‘𝑥))
∈ (log “ 𝐷))) | 
| 143 | 9, 13, 142 | mp2an 692 | . . . . . . . 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 217 | . . . . 5
⊢ (𝑥 ∈ (◡ℑ “ (-π(,)π)) → 𝑥 ∈ (log “ 𝐷)) | 
| 147 | 146 | ssriv 3986 | . . . 4
⊢ (◡ℑ “ (-π(,)π)) ⊆ (log
“ 𝐷) | 
| 148 | 44, 147 | eqssi 3999 | . . 3
⊢ (log
“ 𝐷) = (◡ℑ “
(-π(,)π)) | 
| 149 |  | f1oeq3 6837 | . . 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 230 | 1
⊢ (log
↾ 𝐷):𝐷–1-1-onto→(◡ℑ “
(-π(,)π)) |