Proof of Theorem argrege0
Step | Hyp | Ref
| Expression |
1 | | logcl 24119 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈
ℂ) |
2 | 1 | 3adant3 1074 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(log‘𝐴) ∈
ℂ) |
3 | 2 | imcld 13783 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(ℑ‘(log‘𝐴)) ∈ ℝ) |
4 | | simp3 1056 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) → 0
≤ (ℜ‘𝐴)) |
5 | | simp1 1054 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
𝐴 ∈
ℂ) |
6 | 5 | abscld 14023 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(abs‘𝐴) ∈
ℝ) |
7 | 6 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(abs‘𝐴) ∈
ℂ) |
8 | 7 | mul01d 10114 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
((abs‘𝐴) · 0)
= 0) |
9 | | absrpcl 13876 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℝ+) |
10 | 9 | 3adant3 1074 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(abs‘𝐴) ∈
ℝ+) |
11 | 10 | rpne0d 11753 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(abs‘𝐴) ≠
0) |
12 | 5, 7, 11 | divcld 10680 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(𝐴 / (abs‘𝐴)) ∈
ℂ) |
13 | 6, 12 | remul2d 13815 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(ℜ‘((abs‘𝐴) · (𝐴 / (abs‘𝐴)))) = ((abs‘𝐴) · (ℜ‘(𝐴 / (abs‘𝐴))))) |
14 | 5, 7, 11 | divcan2d 10682 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
((abs‘𝐴) ·
(𝐴 / (abs‘𝐴))) = 𝐴) |
15 | 14 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(ℜ‘((abs‘𝐴) · (𝐴 / (abs‘𝐴)))) = (ℜ‘𝐴)) |
16 | 13, 15 | eqtr3d 2646 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
((abs‘𝐴) ·
(ℜ‘(𝐴 /
(abs‘𝐴)))) =
(ℜ‘𝐴)) |
17 | 4, 8, 16 | 3brtr4d 4615 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
((abs‘𝐴) · 0)
≤ ((abs‘𝐴)
· (ℜ‘(𝐴 /
(abs‘𝐴))))) |
18 | | 0re 9919 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
19 | 18 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) → 0
∈ ℝ) |
20 | 12 | recld 13782 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(ℜ‘(𝐴 /
(abs‘𝐴))) ∈
ℝ) |
21 | 19, 20, 10 | lemul2d 11792 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) → (0
≤ (ℜ‘(𝐴 /
(abs‘𝐴))) ↔
((abs‘𝐴) · 0)
≤ ((abs‘𝐴)
· (ℜ‘(𝐴 /
(abs‘𝐴)))))) |
22 | 17, 21 | mpbird 246 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) → 0
≤ (ℜ‘(𝐴 /
(abs‘𝐴)))) |
23 | | efiarg 24157 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (exp‘(i
· (ℑ‘(log‘𝐴)))) = (𝐴 / (abs‘𝐴))) |
24 | 23 | 3adant3 1074 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(exp‘(i · (ℑ‘(log‘𝐴)))) = (𝐴 / (abs‘𝐴))) |
25 | 24 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(ℜ‘(exp‘(i · (ℑ‘(log‘𝐴))))) = (ℜ‘(𝐴 / (abs‘𝐴)))) |
26 | 22, 25 | breqtrrd 4611 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) → 0
≤ (ℜ‘(exp‘(i · (ℑ‘(log‘𝐴)))))) |
27 | | recosval 14705 |
. . . . . . 7
⊢
((ℑ‘(log‘𝐴)) ∈ ℝ →
(cos‘(ℑ‘(log‘𝐴))) = (ℜ‘(exp‘(i ·
(ℑ‘(log‘𝐴)))))) |
28 | 3, 27 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(cos‘(ℑ‘(log‘𝐴))) = (ℜ‘(exp‘(i ·
(ℑ‘(log‘𝐴)))))) |
29 | 26, 28 | breqtrrd 4611 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) → 0
≤ (cos‘(ℑ‘(log‘𝐴)))) |
30 | | halfpire 24020 |
. . . . . . . . . 10
⊢ (π /
2) ∈ ℝ |
31 | | pirp 24017 |
. . . . . . . . . . 11
⊢ π
∈ ℝ+ |
32 | | rphalfcl 11734 |
. . . . . . . . . . 11
⊢ (π
∈ ℝ+ → (π / 2) ∈
ℝ+) |
33 | | rpge0 11721 |
. . . . . . . . . . 11
⊢ ((π /
2) ∈ ℝ+ → 0 ≤ (π / 2)) |
34 | 31, 32, 33 | mp2b 10 |
. . . . . . . . . 10
⊢ 0 ≤
(π / 2) |
35 | | pire 24014 |
. . . . . . . . . . 11
⊢ π
∈ ℝ |
36 | | rphalflt 11736 |
. . . . . . . . . . . 12
⊢ (π
∈ ℝ+ → (π / 2) < π) |
37 | 31, 36 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (π /
2) < π |
38 | 30, 35, 37 | ltleii 10039 |
. . . . . . . . . 10
⊢ (π /
2) ≤ π |
39 | 18, 35 | elicc2i 12110 |
. . . . . . . . . 10
⊢ ((π /
2) ∈ (0[,]π) ↔ ((π / 2) ∈ ℝ ∧ 0 ≤ (π / 2)
∧ (π / 2) ≤ π)) |
40 | 30, 34, 38, 39 | mpbir3an 1237 |
. . . . . . . . 9
⊢ (π /
2) ∈ (0[,]π) |
41 | 3 | recnd 9947 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(ℑ‘(log‘𝐴)) ∈ ℂ) |
42 | 41 | abscld 14023 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(abs‘(ℑ‘(log‘𝐴))) ∈ ℝ) |
43 | 41 | absge0d 14031 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) → 0
≤ (abs‘(ℑ‘(log‘𝐴)))) |
44 | | logimcl 24120 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-π <
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π)) |
45 | 44 | 3adant3 1074 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(-π < (ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π)) |
46 | 45 | simpld 474 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
-π < (ℑ‘(log‘𝐴))) |
47 | 35 | renegcli 10221 |
. . . . . . . . . . . . 13
⊢ -π
∈ ℝ |
48 | | ltle 10005 |
. . . . . . . . . . . . 13
⊢ ((-π
∈ ℝ ∧ (ℑ‘(log‘𝐴)) ∈ ℝ) → (-π <
(ℑ‘(log‘𝐴)) → -π ≤
(ℑ‘(log‘𝐴)))) |
49 | 47, 3, 48 | sylancr 694 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(-π < (ℑ‘(log‘𝐴)) → -π ≤
(ℑ‘(log‘𝐴)))) |
50 | 46, 49 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
-π ≤ (ℑ‘(log‘𝐴))) |
51 | 45 | simprd 478 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(ℑ‘(log‘𝐴)) ≤ π) |
52 | | absle 13903 |
. . . . . . . . . . . 12
⊢
(((ℑ‘(log‘𝐴)) ∈ ℝ ∧ π ∈ ℝ)
→ ((abs‘(ℑ‘(log‘𝐴))) ≤ π ↔ (-π ≤
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π))) |
53 | 3, 35, 52 | sylancl 693 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
((abs‘(ℑ‘(log‘𝐴))) ≤ π ↔ (-π ≤
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π))) |
54 | 50, 51, 53 | mpbir2and 959 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(abs‘(ℑ‘(log‘𝐴))) ≤ π) |
55 | 18, 35 | elicc2i 12110 |
. . . . . . . . . 10
⊢
((abs‘(ℑ‘(log‘𝐴))) ∈ (0[,]π) ↔
((abs‘(ℑ‘(log‘𝐴))) ∈ ℝ ∧ 0 ≤
(abs‘(ℑ‘(log‘𝐴))) ∧
(abs‘(ℑ‘(log‘𝐴))) ≤ π)) |
56 | 42, 43, 54, 55 | syl3anbrc 1239 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(abs‘(ℑ‘(log‘𝐴))) ∈ (0[,]π)) |
57 | | cosord 24082 |
. . . . . . . . 9
⊢ (((π /
2) ∈ (0[,]π) ∧ (abs‘(ℑ‘(log‘𝐴))) ∈ (0[,]π)) →
((π / 2) < (abs‘(ℑ‘(log‘𝐴))) ↔
(cos‘(abs‘(ℑ‘(log‘𝐴)))) < (cos‘(π /
2)))) |
58 | 40, 56, 57 | sylancr 694 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
((π / 2) < (abs‘(ℑ‘(log‘𝐴))) ↔
(cos‘(abs‘(ℑ‘(log‘𝐴)))) < (cos‘(π /
2)))) |
59 | | fveq2 6103 |
. . . . . . . . . . 11
⊢
((abs‘(ℑ‘(log‘𝐴))) = (ℑ‘(log‘𝐴)) →
(cos‘(abs‘(ℑ‘(log‘𝐴)))) =
(cos‘(ℑ‘(log‘𝐴)))) |
60 | 59 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
((abs‘(ℑ‘(log‘𝐴))) = (ℑ‘(log‘𝐴)) →
(cos‘(abs‘(ℑ‘(log‘𝐴)))) =
(cos‘(ℑ‘(log‘𝐴))))) |
61 | | cosneg 14716 |
. . . . . . . . . . . 12
⊢
((ℑ‘(log‘𝐴)) ∈ ℂ →
(cos‘-(ℑ‘(log‘𝐴))) =
(cos‘(ℑ‘(log‘𝐴)))) |
62 | 41, 61 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(cos‘-(ℑ‘(log‘𝐴))) =
(cos‘(ℑ‘(log‘𝐴)))) |
63 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢
((abs‘(ℑ‘(log‘𝐴))) = -(ℑ‘(log‘𝐴)) →
(cos‘(abs‘(ℑ‘(log‘𝐴)))) =
(cos‘-(ℑ‘(log‘𝐴)))) |
64 | 63 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢
((abs‘(ℑ‘(log‘𝐴))) = -(ℑ‘(log‘𝐴)) →
((cos‘(abs‘(ℑ‘(log‘𝐴)))) =
(cos‘(ℑ‘(log‘𝐴))) ↔
(cos‘-(ℑ‘(log‘𝐴))) =
(cos‘(ℑ‘(log‘𝐴))))) |
65 | 62, 64 | syl5ibrcom 236 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
((abs‘(ℑ‘(log‘𝐴))) = -(ℑ‘(log‘𝐴)) →
(cos‘(abs‘(ℑ‘(log‘𝐴)))) =
(cos‘(ℑ‘(log‘𝐴))))) |
66 | 3 | absord 14002 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
((abs‘(ℑ‘(log‘𝐴))) = (ℑ‘(log‘𝐴)) ∨
(abs‘(ℑ‘(log‘𝐴))) = -(ℑ‘(log‘𝐴)))) |
67 | 60, 65, 66 | mpjaod 395 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(cos‘(abs‘(ℑ‘(log‘𝐴)))) =
(cos‘(ℑ‘(log‘𝐴)))) |
68 | | coshalfpi 24025 |
. . . . . . . . . 10
⊢
(cos‘(π / 2)) = 0 |
69 | 68 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(cos‘(π / 2)) = 0) |
70 | 67, 69 | breq12d 4596 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
((cos‘(abs‘(ℑ‘(log‘𝐴)))) < (cos‘(π / 2)) ↔
(cos‘(ℑ‘(log‘𝐴))) < 0)) |
71 | 58, 70 | bitrd 267 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
((π / 2) < (abs‘(ℑ‘(log‘𝐴))) ↔
(cos‘(ℑ‘(log‘𝐴))) < 0)) |
72 | 71 | notbid 307 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(¬ (π / 2) < (abs‘(ℑ‘(log‘𝐴))) ↔ ¬
(cos‘(ℑ‘(log‘𝐴))) < 0)) |
73 | | lenlt 9995 |
. . . . . . 7
⊢
(((abs‘(ℑ‘(log‘𝐴))) ∈ ℝ ∧ (π / 2) ∈
ℝ) → ((abs‘(ℑ‘(log‘𝐴))) ≤ (π / 2) ↔ ¬ (π / 2)
< (abs‘(ℑ‘(log‘𝐴))))) |
74 | 42, 30, 73 | sylancl 693 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
((abs‘(ℑ‘(log‘𝐴))) ≤ (π / 2) ↔ ¬ (π / 2)
< (abs‘(ℑ‘(log‘𝐴))))) |
75 | 3 | recoscld 14713 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(cos‘(ℑ‘(log‘𝐴))) ∈ ℝ) |
76 | | lenlt 9995 |
. . . . . . 7
⊢ ((0
∈ ℝ ∧ (cos‘(ℑ‘(log‘𝐴))) ∈ ℝ) → (0 ≤
(cos‘(ℑ‘(log‘𝐴))) ↔ ¬
(cos‘(ℑ‘(log‘𝐴))) < 0)) |
77 | 18, 75, 76 | sylancr 694 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) → (0
≤ (cos‘(ℑ‘(log‘𝐴))) ↔ ¬
(cos‘(ℑ‘(log‘𝐴))) < 0)) |
78 | 72, 74, 77 | 3bitr4d 299 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
((abs‘(ℑ‘(log‘𝐴))) ≤ (π / 2) ↔ 0 ≤
(cos‘(ℑ‘(log‘𝐴))))) |
79 | 29, 78 | mpbird 246 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(abs‘(ℑ‘(log‘𝐴))) ≤ (π / 2)) |
80 | | absle 13903 |
. . . . 5
⊢
(((ℑ‘(log‘𝐴)) ∈ ℝ ∧ (π / 2) ∈
ℝ) → ((abs‘(ℑ‘(log‘𝐴))) ≤ (π / 2) ↔ (-(π / 2) ≤
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ (π /
2)))) |
81 | 3, 30, 80 | sylancl 693 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
((abs‘(ℑ‘(log‘𝐴))) ≤ (π / 2) ↔ (-(π / 2) ≤
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ (π /
2)))) |
82 | 79, 81 | mpbid 221 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(-(π / 2) ≤ (ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ (π /
2))) |
83 | 82 | simpld 474 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
-(π / 2) ≤ (ℑ‘(log‘𝐴))) |
84 | 82 | simprd 478 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(ℑ‘(log‘𝐴)) ≤ (π / 2)) |
85 | 30 | renegcli 10221 |
. . 3
⊢ -(π /
2) ∈ ℝ |
86 | 85, 30 | elicc2i 12110 |
. 2
⊢
((ℑ‘(log‘𝐴)) ∈ (-(π / 2)[,](π / 2)) ↔
((ℑ‘(log‘𝐴)) ∈ ℝ ∧ -(π / 2) ≤
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ (π /
2))) |
87 | 3, 83, 84, 86 | syl3anbrc 1239 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤
(ℜ‘𝐴)) →
(ℑ‘(log‘𝐴)) ∈ (-(π / 2)[,](π /
2))) |