Proof of Theorem logimul
Step | Hyp | Ref
| Expression |
1 | | logcl 25722 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈
ℂ) |
2 | 1 | 3adant3 1131 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(log‘𝐴) ∈
ℂ) |
3 | | ax-icn 10931 |
. . . . . 6
⊢ i ∈
ℂ |
4 | | halfpire 25619 |
. . . . . . 7
⊢ (π /
2) ∈ ℝ |
5 | 4 | recni 10990 |
. . . . . 6
⊢ (π /
2) ∈ ℂ |
6 | 3, 5 | mulcli 10983 |
. . . . 5
⊢ (i
· (π / 2)) ∈ ℂ |
7 | | efadd 15801 |
. . . . 5
⊢
(((log‘𝐴)
∈ ℂ ∧ (i · (π / 2)) ∈ ℂ) →
(exp‘((log‘𝐴) +
(i · (π / 2)))) = ((exp‘(log‘𝐴)) · (exp‘(i · (π /
2))))) |
8 | 2, 6, 7 | sylancl 586 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(exp‘((log‘𝐴) +
(i · (π / 2)))) = ((exp‘(log‘𝐴)) · (exp‘(i · (π /
2))))) |
9 | | eflog 25730 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(exp‘(log‘𝐴)) =
𝐴) |
10 | 9 | 3adant3 1131 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(exp‘(log‘𝐴)) =
𝐴) |
11 | | efhalfpi 25626 |
. . . . . 6
⊢
(exp‘(i · (π / 2))) = i |
12 | 11 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(exp‘(i · (π / 2))) = i) |
13 | 10, 12 | oveq12d 7289 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
((exp‘(log‘𝐴))
· (exp‘(i · (π / 2)))) = (𝐴 · i)) |
14 | | simp1 1135 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
𝐴 ∈
ℂ) |
15 | | mulcom 10958 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ i ∈
ℂ) → (𝐴 ·
i) = (i · 𝐴)) |
16 | 14, 3, 15 | sylancl 586 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(𝐴 · i) = (i
· 𝐴)) |
17 | 8, 13, 16 | 3eqtrd 2784 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(exp‘((log‘𝐴) +
(i · (π / 2)))) = (i · 𝐴)) |
18 | 17 | fveq2d 6775 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(log‘(exp‘((log‘𝐴) + (i · (π / 2))))) =
(log‘(i · 𝐴))) |
19 | | addcl 10954 |
. . . . 5
⊢
(((log‘𝐴)
∈ ℂ ∧ (i · (π / 2)) ∈ ℂ) →
((log‘𝐴) + (i
· (π / 2))) ∈ ℂ) |
20 | 2, 6, 19 | sylancl 586 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
((log‘𝐴) + (i
· (π / 2))) ∈ ℂ) |
21 | | pire 25613 |
. . . . . . . 8
⊢ π
∈ ℝ |
22 | 21 | renegcli 11282 |
. . . . . . 7
⊢ -π
∈ ℝ |
23 | 22 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
-π ∈ ℝ) |
24 | 2 | imcld 14904 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(ℑ‘(log‘𝐴)) ∈ ℝ) |
25 | | readdcl 10955 |
. . . . . . 7
⊢
(((ℑ‘(log‘𝐴)) ∈ ℝ ∧ (π / 2) ∈
ℝ) → ((ℑ‘(log‘𝐴)) + (π / 2)) ∈
ℝ) |
26 | 24, 4, 25 | sylancl 586 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
((ℑ‘(log‘𝐴)) + (π / 2)) ∈
ℝ) |
27 | | logimcl 25723 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-π <
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π)) |
28 | 27 | 3adant3 1131 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(-π < (ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π)) |
29 | 28 | simpld 495 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
-π < (ℑ‘(log‘𝐴))) |
30 | | pirp 25616 |
. . . . . . . 8
⊢ π
∈ ℝ+ |
31 | | rphalfcl 12756 |
. . . . . . . 8
⊢ (π
∈ ℝ+ → (π / 2) ∈
ℝ+) |
32 | 30, 31 | ax-mp 5 |
. . . . . . 7
⊢ (π /
2) ∈ ℝ+ |
33 | | ltaddrp 12766 |
. . . . . . 7
⊢
(((ℑ‘(log‘𝐴)) ∈ ℝ ∧ (π / 2) ∈
ℝ+) → (ℑ‘(log‘𝐴)) < ((ℑ‘(log‘𝐴)) + (π /
2))) |
34 | 24, 32, 33 | sylancl 586 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(ℑ‘(log‘𝐴)) < ((ℑ‘(log‘𝐴)) + (π /
2))) |
35 | 23, 24, 26, 29, 34 | lttrd 11136 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
-π < ((ℑ‘(log‘𝐴)) + (π / 2))) |
36 | | imadd 14843 |
. . . . . . 7
⊢
(((log‘𝐴)
∈ ℂ ∧ (i · (π / 2)) ∈ ℂ) →
(ℑ‘((log‘𝐴) + (i · (π / 2)))) =
((ℑ‘(log‘𝐴)) + (ℑ‘(i · (π /
2))))) |
37 | 2, 6, 36 | sylancl 586 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(ℑ‘((log‘𝐴) + (i · (π / 2)))) =
((ℑ‘(log‘𝐴)) + (ℑ‘(i · (π /
2))))) |
38 | | reim 14818 |
. . . . . . . . 9
⊢ ((π /
2) ∈ ℂ → (ℜ‘(π / 2)) = (ℑ‘(i ·
(π / 2)))) |
39 | 5, 38 | ax-mp 5 |
. . . . . . . 8
⊢
(ℜ‘(π / 2)) = (ℑ‘(i · (π /
2))) |
40 | | rere 14831 |
. . . . . . . . 9
⊢ ((π /
2) ∈ ℝ → (ℜ‘(π / 2)) = (π /
2)) |
41 | 4, 40 | ax-mp 5 |
. . . . . . . 8
⊢
(ℜ‘(π / 2)) = (π / 2) |
42 | 39, 41 | eqtr3i 2770 |
. . . . . . 7
⊢
(ℑ‘(i · (π / 2))) = (π / 2) |
43 | 42 | oveq2i 7282 |
. . . . . 6
⊢
((ℑ‘(log‘𝐴)) + (ℑ‘(i · (π /
2)))) = ((ℑ‘(log‘𝐴)) + (π / 2)) |
44 | 37, 43 | eqtrdi 2796 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(ℑ‘((log‘𝐴) + (i · (π / 2)))) =
((ℑ‘(log‘𝐴)) + (π / 2))) |
45 | 35, 44 | breqtrrd 5107 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
-π < (ℑ‘((log‘𝐴) + (i · (π /
2))))) |
46 | | argrege0 25764 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(ℑ‘(log‘𝐴)) ∈ (-(π / 2)[,](π /
2))) |
47 | 4 | renegcli 11282 |
. . . . . . . . . 10
⊢ -(π /
2) ∈ ℝ |
48 | 47, 4 | elicc2i 13144 |
. . . . . . . . 9
⊢
((ℑ‘(log‘𝐴)) ∈ (-(π / 2)[,](π / 2)) ↔
((ℑ‘(log‘𝐴)) ∈ ℝ ∧ -(π / 2) ≤
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ (π /
2))) |
49 | 48 | simp3bi 1146 |
. . . . . . . 8
⊢
((ℑ‘(log‘𝐴)) ∈ (-(π / 2)[,](π / 2)) →
(ℑ‘(log‘𝐴)) ≤ (π / 2)) |
50 | 46, 49 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(ℑ‘(log‘𝐴)) ≤ (π / 2)) |
51 | 21 | recni 10990 |
. . . . . . . 8
⊢ π
∈ ℂ |
52 | | pidiv2halves 25622 |
. . . . . . . 8
⊢ ((π /
2) + (π / 2)) = π |
53 | 51, 5, 5, 52 | subaddrii 11310 |
. . . . . . 7
⊢ (π
− (π / 2)) = (π / 2) |
54 | 50, 53 | breqtrrdi 5121 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(ℑ‘(log‘𝐴)) ≤ (π − (π /
2))) |
55 | 4 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(π / 2) ∈ ℝ) |
56 | 21 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
π ∈ ℝ) |
57 | | leaddsub 11451 |
. . . . . . 7
⊢
(((ℑ‘(log‘𝐴)) ∈ ℝ ∧ (π / 2) ∈
ℝ ∧ π ∈ ℝ) → (((ℑ‘(log‘𝐴)) + (π / 2)) ≤ π
↔ (ℑ‘(log‘𝐴)) ≤ (π − (π /
2)))) |
58 | 24, 55, 56, 57 | syl3anc 1370 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(((ℑ‘(log‘𝐴)) + (π / 2)) ≤ π ↔
(ℑ‘(log‘𝐴)) ≤ (π − (π /
2)))) |
59 | 54, 58 | mpbird 256 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
((ℑ‘(log‘𝐴)) + (π / 2)) ≤ π) |
60 | 44, 59 | eqbrtrd 5101 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(ℑ‘((log‘𝐴) + (i · (π / 2)))) ≤
π) |
61 | | ellogrn 25713 |
. . . 4
⊢
(((log‘𝐴) + (i
· (π / 2))) ∈ ran log ↔ (((log‘𝐴) + (i · (π / 2))) ∈ ℂ
∧ -π < (ℑ‘((log‘𝐴) + (i · (π / 2)))) ∧
(ℑ‘((log‘𝐴) + (i · (π / 2)))) ≤
π)) |
62 | 20, 45, 60, 61 | syl3anbrc 1342 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
((log‘𝐴) + (i
· (π / 2))) ∈ ran log) |
63 | | logef 25735 |
. . 3
⊢
(((log‘𝐴) + (i
· (π / 2))) ∈ ran log →
(log‘(exp‘((log‘𝐴) + (i · (π / 2))))) =
((log‘𝐴) + (i
· (π / 2)))) |
64 | 62, 63 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(log‘(exp‘((log‘𝐴) + (i · (π / 2))))) =
((log‘𝐴) + (i
· (π / 2)))) |
65 | 18, 64 | eqtr3d 2782 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(log‘(i · 𝐴))
= ((log‘𝐴) + (i
· (π / 2)))) |