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 
|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( Im ` ( log ` A ) ) e. ( 0 (,) _pi ) )

Proof

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