This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem argrege0

Description: Closure of the argument of a complex number with nonnegative real part. (Contributed by Mario Carneiro, 2-Apr-2015)

Ref Expression
Assertion argrege0 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )

Proof

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 ) ) )