| Step |
Hyp |
Ref |
Expression |
| 1 |
|
logcl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ ) |
| 2 |
1
|
3adant3 |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( log ‘ 𝐴 ) ∈ ℂ ) |
| 3 |
2
|
imcld |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ) |
| 4 |
|
simp3 |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → 0 ≤ ( ℜ ‘ 𝐴 ) ) |
| 5 |
|
simp1 |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → 𝐴 ∈ ℂ ) |
| 6 |
5
|
abscld |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( abs ‘ 𝐴 ) ∈ ℝ ) |
| 7 |
6
|
recnd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( abs ‘ 𝐴 ) ∈ ℂ ) |
| 8 |
7
|
mul01d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ 𝐴 ) · 0 ) = 0 ) |
| 9 |
|
absrpcl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ+ ) |
| 10 |
9
|
3adant3 |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( abs ‘ 𝐴 ) ∈ ℝ+ ) |
| 11 |
10
|
rpne0d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( abs ‘ 𝐴 ) ≠ 0 ) |
| 12 |
5 7 11
|
divcld |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( 𝐴 / ( abs ‘ 𝐴 ) ) ∈ ℂ ) |
| 13 |
6 12
|
remul2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ ( ( abs ‘ 𝐴 ) · ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) = ( ( abs ‘ 𝐴 ) · ( ℜ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) ) |
| 14 |
5 7 11
|
divcan2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ 𝐴 ) · ( 𝐴 / ( abs ‘ 𝐴 ) ) ) = 𝐴 ) |
| 15 |
14
|
fveq2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ ( ( abs ‘ 𝐴 ) · ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) = ( ℜ ‘ 𝐴 ) ) |
| 16 |
13 15
|
eqtr3d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ 𝐴 ) · ( ℜ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) = ( ℜ ‘ 𝐴 ) ) |
| 17 |
4 8 16
|
3brtr4d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ 𝐴 ) · 0 ) ≤ ( ( abs ‘ 𝐴 ) · ( ℜ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) ) |
| 18 |
|
0re |
⊢ 0 ∈ ℝ |
| 19 |
18
|
a1i |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → 0 ∈ ℝ ) |
| 20 |
12
|
recld |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ∈ ℝ ) |
| 21 |
19 20 10
|
lemul2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( 0 ≤ ( ℜ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ↔ ( ( abs ‘ 𝐴 ) · 0 ) ≤ ( ( abs ‘ 𝐴 ) · ( ℜ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) ) ) |
| 22 |
17 21
|
mpbird |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → 0 ≤ ( ℜ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) |
| 23 |
|
efiarg |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( 𝐴 / ( abs ‘ 𝐴 ) ) ) |
| 24 |
23
|
3adant3 |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( 𝐴 / ( abs ‘ 𝐴 ) ) ) |
| 25 |
24
|
fveq2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) = ( ℜ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) |
| 26 |
22 25
|
breqtrrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → 0 ≤ ( ℜ ‘ ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) ) |
| 27 |
|
recosval |
⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ → ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( ℜ ‘ ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) ) |
| 28 |
3 27
|
syl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( ℜ ‘ ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) ) |
| 29 |
26 28
|
breqtrrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → 0 ≤ ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) |
| 30 |
|
halfpire |
⊢ ( π / 2 ) ∈ ℝ |
| 31 |
|
pirp |
⊢ π ∈ ℝ+ |
| 32 |
|
rphalfcl |
⊢ ( π ∈ ℝ+ → ( π / 2 ) ∈ ℝ+ ) |
| 33 |
|
rpge0 |
⊢ ( ( π / 2 ) ∈ ℝ+ → 0 ≤ ( π / 2 ) ) |
| 34 |
31 32 33
|
mp2b |
⊢ 0 ≤ ( π / 2 ) |
| 35 |
|
pire |
⊢ π ∈ ℝ |
| 36 |
|
rphalflt |
⊢ ( π ∈ ℝ+ → ( π / 2 ) < π ) |
| 37 |
31 36
|
ax-mp |
⊢ ( π / 2 ) < π |
| 38 |
30 35 37
|
ltleii |
⊢ ( π / 2 ) ≤ π |
| 39 |
18 35
|
elicc2i |
⊢ ( ( π / 2 ) ∈ ( 0 [,] π ) ↔ ( ( π / 2 ) ∈ ℝ ∧ 0 ≤ ( π / 2 ) ∧ ( π / 2 ) ≤ π ) ) |
| 40 |
30 34 38 39
|
mpbir3an |
⊢ ( π / 2 ) ∈ ( 0 [,] π ) |
| 41 |
3
|
recnd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ ) |
| 42 |
41
|
abscld |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℝ ) |
| 43 |
41
|
absge0d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → 0 ≤ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) |
| 44 |
|
logimcl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) ) |
| 45 |
44
|
3adant3 |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) ) |
| 46 |
45
|
simpld |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ) |
| 47 |
35
|
renegcli |
⊢ - π ∈ ℝ |
| 48 |
|
ltle |
⊢ ( ( - π ∈ ℝ ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) → - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) |
| 49 |
47 3 48
|
sylancr |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) → - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) |
| 50 |
46 49
|
mpd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) |
| 51 |
45
|
simprd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) |
| 52 |
|
absle |
⊢ ( ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ π ∈ ℝ ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ π ↔ ( - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) ) ) |
| 53 |
3 35 52
|
sylancl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ π ↔ ( - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) ) ) |
| 54 |
50 51 53
|
mpbir2and |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ π ) |
| 55 |
18 35
|
elicc2i |
⊢ ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ( 0 [,] π ) ↔ ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∧ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ π ) ) |
| 56 |
42 43 54 55
|
syl3anbrc |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ( 0 [,] π ) ) |
| 57 |
|
cosord |
⊢ ( ( ( π / 2 ) ∈ ( 0 [,] π ) ∧ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ( 0 [,] π ) ) → ( ( π / 2 ) < ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ↔ ( cos ‘ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) < ( cos ‘ ( π / 2 ) ) ) ) |
| 58 |
40 56 57
|
sylancr |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( π / 2 ) < ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ↔ ( cos ‘ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) < ( cos ‘ ( π / 2 ) ) ) ) |
| 59 |
|
fveq2 |
⊢ ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( ℑ ‘ ( log ‘ 𝐴 ) ) → ( cos ‘ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) |
| 60 |
59
|
a1i |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( ℑ ‘ ( log ‘ 𝐴 ) ) → ( cos ‘ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) |
| 61 |
|
cosneg |
⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ → ( cos ‘ - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) |
| 62 |
41 61
|
syl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( cos ‘ - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) |
| 63 |
|
fveqeq2 |
⊢ ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = - ( ℑ ‘ ( log ‘ 𝐴 ) ) → ( ( cos ‘ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ↔ ( cos ‘ - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) |
| 64 |
62 63
|
syl5ibrcom |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = - ( ℑ ‘ ( log ‘ 𝐴 ) ) → ( cos ‘ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) |
| 65 |
3
|
absord |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( ℑ ‘ ( log ‘ 𝐴 ) ) ∨ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) |
| 66 |
60 64 65
|
mpjaod |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( cos ‘ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) |
| 67 |
|
coshalfpi |
⊢ ( cos ‘ ( π / 2 ) ) = 0 |
| 68 |
67
|
a1i |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( cos ‘ ( π / 2 ) ) = 0 ) |
| 69 |
66 68
|
breq12d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( cos ‘ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) < ( cos ‘ ( π / 2 ) ) ↔ ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) < 0 ) ) |
| 70 |
58 69
|
bitrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( π / 2 ) < ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ↔ ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) < 0 ) ) |
| 71 |
70
|
notbid |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ¬ ( π / 2 ) < ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ↔ ¬ ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) < 0 ) ) |
| 72 |
|
lenlt |
⊢ ( ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ ( π / 2 ) ↔ ¬ ( π / 2 ) < ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) |
| 73 |
42 30 72
|
sylancl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ ( π / 2 ) ↔ ¬ ( π / 2 ) < ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) |
| 74 |
3
|
recoscld |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℝ ) |
| 75 |
|
lenlt |
⊢ ( ( 0 ∈ ℝ ∧ ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℝ ) → ( 0 ≤ ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ↔ ¬ ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) < 0 ) ) |
| 76 |
18 74 75
|
sylancr |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( 0 ≤ ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ↔ ¬ ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) < 0 ) ) |
| 77 |
71 73 76
|
3bitr4d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ ( π / 2 ) ↔ 0 ≤ ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) |
| 78 |
29 77
|
mpbird |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ ( π / 2 ) ) |
| 79 |
|
absle |
⊢ ( ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ ( π / 2 ) ↔ ( - ( π / 2 ) ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ ( π / 2 ) ) ) ) |
| 80 |
3 30 79
|
sylancl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ ( π / 2 ) ↔ ( - ( π / 2 ) ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ ( π / 2 ) ) ) ) |
| 81 |
78 80
|
mpbid |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( - ( π / 2 ) ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ ( π / 2 ) ) ) |
| 82 |
81
|
simpld |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → - ( π / 2 ) ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) |
| 83 |
81
|
simprd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ ( π / 2 ) ) |
| 84 |
30
|
renegcli |
⊢ - ( π / 2 ) ∈ ℝ |
| 85 |
84 30
|
elicc2i |
⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ↔ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ - ( π / 2 ) ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ ( π / 2 ) ) ) |
| 86 |
3 82 83 85
|
syl3anbrc |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ) |