Metamath Proof Explorer

Theorem argimgt0

Description: Closure of the argument of a complex number with positive imaginary part. (Contributed by Mario Carneiro, 25-Feb-2015)

Ref Expression
Assertion argimgt0 ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( 0 (,) π ) )

Proof

Step Hyp Ref Expression
1 imcl ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℝ )
2 gt0ne0 ⊢ ( ( ( ℑ ‘ 𝐴 ) ∈ ℝ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ 𝐴 ) ≠ 0 )
3 1 2 sylan ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ 𝐴 ) ≠ 0 )
4 fveq2 ⊢ ( 𝐴 = 0 → ( ℑ ‘ 𝐴 ) = ( ℑ ‘ 0 ) )
5 im0 ⊢ ( ℑ ‘ 0 ) = 0
6 4 5 eqtrdi ⊢ ( 𝐴 = 0 → ( ℑ ‘ 𝐴 ) = 0 )
7 6 necon3i ⊢ ( ( ℑ ‘ 𝐴 ) ≠ 0 → 𝐴 ≠ 0 )
8 3 7 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → 𝐴 ≠ 0 )
9 logcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ )
10 8 9 syldan ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( log ‘ 𝐴 ) ∈ ℂ )
11 10 imcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ )
12 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → 0 < ( ℑ ‘ 𝐴 ) )
13 abscl ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℝ )
14 13 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( abs ‘ 𝐴 ) ∈ ℝ )
15 14 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( abs ‘ 𝐴 ) ∈ ℂ )
16 15 mul01d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ( abs ‘ 𝐴 ) · 0 ) = 0 )
17 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → 𝐴 ∈ ℂ )
18 absrpcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ+ )
19 8 18 syldan ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( abs ‘ 𝐴 ) ∈ ℝ+ )
20 19 rpne0d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( abs ‘ 𝐴 ) ≠ 0 )
21 17 15 20 divcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( 𝐴 / ( abs ‘ 𝐴 ) ) ∈ ℂ )
22 14 21 immul2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ ( ( abs ‘ 𝐴 ) · ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) = ( ( abs ‘ 𝐴 ) · ( ℑ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) )
23 17 15 20 divcan2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ( abs ‘ 𝐴 ) · ( 𝐴 / ( abs ‘ 𝐴 ) ) ) = 𝐴 )
24 23 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ ( ( abs ‘ 𝐴 ) · ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) = ( ℑ ‘ 𝐴 ) )
25 22 24 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ( abs ‘ 𝐴 ) · ( ℑ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) = ( ℑ ‘ 𝐴 ) )
26 12 16 25 3brtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ( abs ‘ 𝐴 ) · 0 ) < ( ( abs ‘ 𝐴 ) · ( ℑ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) )
27 0re ⊢ 0 ∈ ℝ
28 27 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → 0 ∈ ℝ )
29 21 imcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ∈ ℝ )
30 28 29 19 ltmul2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( 0 < ( ℑ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ↔ ( ( abs ‘ 𝐴 ) · 0 ) < ( ( abs ‘ 𝐴 ) · ( ℑ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) ) )
31 26 30 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → 0 < ( ℑ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) )
32 efiarg ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( 𝐴 / ( abs ‘ 𝐴 ) ) )
33 8 32 syldan ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( 𝐴 / ( abs ‘ 𝐴 ) ) )
34 33 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) = ( ℑ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) )
35 31 34 breqtrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → 0 < ( ℑ ‘ ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) )
36 resinval ⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ → ( sin ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( ℑ ‘ ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) )
37 11 36 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( sin ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( ℑ ‘ ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) )
38 35 37 breqtrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → 0 < ( sin ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
39 11 resincld ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( sin ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℝ )
40 39 lt0neg2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( 0 < ( sin ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ↔ - ( sin ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) < 0 ) )
41 38 40 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → - ( sin ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) < 0 )
42 pire ⊢ π ∈ ℝ
43 readdcl ⊢ ( ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ π ∈ ℝ ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + π ) ∈ ℝ )
44 11 42 43 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + π ) ∈ ℝ )
45 44 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ 0 ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + π ) ∈ ℝ )
46 df-neg ⊢ - π = ( 0 − π )
47 logimcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )
48 8 47 syldan ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )
49 48 simpld ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) )
50 42 renegcli ⊢ - π ∈ ℝ
51 ltle ⊢ ( ( - π ∈ ℝ ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) → - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
52 50 11 51 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) → - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
53 49 52 mpd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) )
54 46 53 eqbrtrrid ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( 0 − π ) ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) )
55 42 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → π ∈ ℝ )
56 28 55 11 lesubaddd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ( 0 − π ) ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ↔ 0 ≤ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + π ) ) )
57 54 56 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → 0 ≤ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + π ) )
58 57 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ 0 ) → 0 ≤ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + π ) )
59 11 28 55 leadd1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ 0 ↔ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + π ) ≤ ( 0 + π ) ) )
60 59 biimpa ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ 0 ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + π ) ≤ ( 0 + π ) )
61 picn ⊢ π ∈ ℂ
62 61 addlidi ⊢ ( 0 + π ) = π
63 60 62 breqtrdi ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ 0 ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + π ) ≤ π )
64 27 42 elicc2i ⊢ ( ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + π ) ∈ ( 0 [,] π ) ↔ ( ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + π ) ∈ ℝ ∧ 0 ≤ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + π ) ∧ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + π ) ≤ π ) )
65 45 58 63 64 syl3anbrc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ 0 ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + π ) ∈ ( 0 [,] π ) )
66 sinq12ge0 ⊢ ( ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + π ) ∈ ( 0 [,] π ) → 0 ≤ ( sin ‘ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + π ) ) )
67 65 66 syl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ 0 ) → 0 ≤ ( sin ‘ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + π ) ) )
68 11 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ )
69 sinppi ⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ → ( sin ‘ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + π ) ) = - ( sin ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
70 68 69 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( sin ‘ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + π ) ) = - ( sin ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
71 70 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ 0 ) → ( sin ‘ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + π ) ) = - ( sin ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
72 67 71 breqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ 0 ) → 0 ≤ - ( sin ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
73 72 ex ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ 0 → 0 ≤ - ( sin ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
74 73 con3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ¬ 0 ≤ - ( sin ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) → ¬ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ 0 ) )
75 39 renegcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → - ( sin ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℝ )
76 ltnle ⊢ ( ( - ( sin ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( - ( sin ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) < 0 ↔ ¬ 0 ≤ - ( sin ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
77 75 27 76 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( - ( sin ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) < 0 ↔ ¬ 0 ≤ - ( sin ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
78 ltnle ⊢ ( ( 0 ∈ ℝ ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ) → ( 0 < ( ℑ ‘ ( log ‘ 𝐴 ) ) ↔ ¬ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ 0 ) )
79 27 11 78 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( 0 < ( ℑ ‘ ( log ‘ 𝐴 ) ) ↔ ¬ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ 0 ) )
80 74 77 79 3imtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( - ( sin ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) < 0 → 0 < ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
81 41 80 mpd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → 0 < ( ℑ ‘ ( log ‘ 𝐴 ) ) )
82 48 simprd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π )
83 rpre ⊢ ( - 𝐴 ∈ ℝ+ → - 𝐴 ∈ ℝ )
84 83 renegcld ⊢ ( - 𝐴 ∈ ℝ+ → - - 𝐴 ∈ ℝ )
85 negneg ⊢ ( 𝐴 ∈ ℂ → - - 𝐴 = 𝐴 )
86 85 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → - - 𝐴 = 𝐴 )
87 86 eleq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( - - 𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ ) )
88 84 87 imbitrid ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( - 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ ) )
89 lognegb ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - 𝐴 ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ 𝐴 ) ) = π ) )
90 8 89 syldan ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( - 𝐴 ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ 𝐴 ) ) = π ) )
91 reim0b ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ∈ ℝ ↔ ( ℑ ‘ 𝐴 ) = 0 ) )
92 91 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( 𝐴 ∈ ℝ ↔ ( ℑ ‘ 𝐴 ) = 0 ) )
93 88 90 92 3imtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) = π → ( ℑ ‘ 𝐴 ) = 0 ) )
94 93 necon3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ( ℑ ‘ 𝐴 ) ≠ 0 → ( ℑ ‘ ( log ‘ 𝐴 ) ) ≠ π ) )
95 3 94 mpd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ≠ π )
96 95 necomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → π ≠ ( ℑ ‘ ( log ‘ 𝐴 ) ) )
97 11 55 82 96 leneltd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) < π )
98 0xr ⊢ 0 ∈ ℝ*
99 42 rexri ⊢ π ∈ ℝ*
100 elioo2 ⊢ ( ( 0 ∈ ℝ* ∧ π ∈ ℝ* ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( 0 (,) π ) ↔ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ 0 < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) < π ) ) )
101 98 99 100 mp2an ⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( 0 (,) π ) ↔ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ 0 < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) < π ) )
102 11 81 97 101 syl3anbrc ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( 0 (,) π ) )