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

Metamath Proof Explorer

Theorem argimlt0

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

Ref Expression
Assertion argimlt0 
|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` A ) ) e. ( -u _pi (,) 0 ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` A ) < 0 )
2 1 lt0ne0d 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` A ) =/= 0 )
3 fveq2 
 |-  ( A = 0 -> ( Im ` A ) = ( Im ` 0 ) )
4 im0 
 |-  ( Im ` 0 ) = 0
5 3 4 eqtrdi 
 |-  ( A = 0 -> ( Im ` A ) = 0 )
6 5 necon3i 
 |-  ( ( Im ` A ) =/= 0 -> A =/= 0 )
7 2 6 syl 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> A =/= 0 )
8 logcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. CC )
9 7 8 syldan 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( log ` A ) e. CC )
10 9 imcld 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` A ) ) e. RR )
11 logcj 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( log ` ( * ` A ) ) = ( * ` ( log ` A ) ) )
12 2 11 syldan 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( log ` ( * ` A ) ) = ( * ` ( log ` A ) ) )
13 12 fveq2d 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` ( * ` A ) ) ) = ( Im ` ( * ` ( log ` A ) ) ) )
14 9 imcjd 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` ( * ` ( log ` A ) ) ) = -u ( Im ` ( log ` A ) ) )
15 13 14 eqtrd 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` ( * ` A ) ) ) = -u ( Im ` ( log ` A ) ) )
16 cjcl 
 |-  ( A e. CC -> ( * ` A ) e. CC )
17 imcl 
 |-  ( A e. CC -> ( Im ` A ) e. RR )
18 17 adantr 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` A ) e. RR )
19 18 lt0neg1d 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( ( Im ` A ) < 0 <-> 0 < -u ( Im ` A ) ) )
20 1 19 mpbid 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> 0 < -u ( Im ` A ) )
21 imcj 
 |-  ( A e. CC -> ( Im ` ( * ` A ) ) = -u ( Im ` A ) )
22 21 adantr 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` ( * ` A ) ) = -u ( Im ` A ) )
23 20 22 breqtrrd 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> 0 < ( Im ` ( * ` A ) ) )
24 argimgt0 
 |-  ( ( ( * ` A ) e. CC /\ 0 < ( Im ` ( * ` A ) ) ) -> ( Im ` ( log ` ( * ` A ) ) ) e. ( 0 (,) _pi ) )
25 16 23 24 syl2an2r 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` ( * ` A ) ) ) e. ( 0 (,) _pi ) )
26 eliooord 
 |-  ( ( Im ` ( log ` ( * ` A ) ) ) e. ( 0 (,) _pi ) -> ( 0 < ( Im ` ( log ` ( * ` A ) ) ) /\ ( Im ` ( log ` ( * ` A ) ) ) < _pi ) )
27 25 26 syl 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( 0 < ( Im ` ( log ` ( * ` A ) ) ) /\ ( Im ` ( log ` ( * ` A ) ) ) < _pi ) )
28 27 simprd 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` ( * ` A ) ) ) < _pi )
29 15 28 eqbrtrrd 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> -u ( Im ` ( log ` A ) ) < _pi )
30 pire 
 |-  _pi e. RR
31 ltnegcon1 
 |-  ( ( ( Im ` ( log ` A ) ) e. RR /\ _pi e. RR ) -> ( -u ( Im ` ( log ` A ) ) < _pi <-> -u _pi < ( Im ` ( log ` A ) ) ) )
32 10 30 31 sylancl 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( -u ( Im ` ( log ` A ) ) < _pi <-> -u _pi < ( Im ` ( log ` A ) ) ) )
33 29 32 mpbid 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> -u _pi < ( Im ` ( log ` A ) ) )
34 27 simpld 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> 0 < ( Im ` ( log ` ( * ` A ) ) ) )
35 34 15 breqtrd 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> 0 < -u ( Im ` ( log ` A ) ) )
36 10 lt0neg1d 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( ( Im ` ( log ` A ) ) < 0 <-> 0 < -u ( Im ` ( log ` A ) ) ) )
37 35 36 mpbird 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` A ) ) < 0 )
38 30 renegcli 
 |-  -u _pi e. RR
39 38 rexri 
 |-  -u _pi e. RR*
40 0xr 
 |-  0 e. RR*
41 elioo2 
 |-  ( ( -u _pi e. RR* /\ 0 e. RR* ) -> ( ( Im ` ( log ` A ) ) e. ( -u _pi (,) 0 ) <-> ( ( Im ` ( log ` A ) ) e. RR /\ -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) < 0 ) ) )
42 39 40 41 mp2an 
 |-  ( ( Im ` ( log ` A ) ) e. ( -u _pi (,) 0 ) <-> ( ( Im ` ( log ` A ) ) e. RR /\ -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) < 0 ) )
43 10 33 37 42 syl3anbrc 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` A ) ) e. ( -u _pi (,) 0 ) )