Metamath Proof Explorer

Theorem argregt0

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

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

Proof

Step Hyp Ref Expression
1 recl 
 |-  ( A e. CC -> ( Re ` A ) e. RR )
2 gt0ne0 
 |-  ( ( ( Re ` A ) e. RR /\ 0 < ( Re ` A ) ) -> ( Re ` A ) =/= 0 )
3 1 2 sylan 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( Re ` A ) =/= 0 )
4 fveq2 
 |-  ( A = 0 -> ( Re ` A ) = ( Re ` 0 ) )
5 re0 
 |-  ( Re ` 0 ) = 0
6 4 5 eqtrdi 
 |-  ( A = 0 -> ( Re ` A ) = 0 )
7 6 necon3i 
 |-  ( ( Re ` A ) =/= 0 -> A =/= 0 )
8 3 7 syl 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> A =/= 0 )
9 logcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. CC )
10 8 9 syldan 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( log ` A ) e. CC )
11 10 imcld 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` A ) ) e. RR )
12 coshalfpi 
 |-  ( cos ` ( _pi / 2 ) ) = 0
13 simpr 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> 0 < ( Re ` A ) )
14 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
15 14 adantr 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( abs ` A ) e. RR )
16 15 recnd 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( abs ` A ) e. CC )
17 16 mul01d 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( ( abs ` A ) x. 0 ) = 0 )
18 simpl 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> A e. CC )
19 absrpcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. RR+ )
20 8 19 syldan 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( abs ` A ) e. RR+ )
21 20 rpne0d 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( abs ` A ) =/= 0 )
22 18 16 21 divcld 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( A / ( abs ` A ) ) e. CC )
23 15 22 remul2d 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( Re ` ( ( abs ` A ) x. ( A / ( abs ` A ) ) ) ) = ( ( abs ` A ) x. ( Re ` ( A / ( abs ` A ) ) ) ) )
24 18 16 21 divcan2d 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( ( abs ` A ) x. ( A / ( abs ` A ) ) ) = A )
25 24 fveq2d 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( Re ` ( ( abs ` A ) x. ( A / ( abs ` A ) ) ) ) = ( Re ` A ) )
26 23 25 eqtr3d 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( ( abs ` A ) x. ( Re ` ( A / ( abs ` A ) ) ) ) = ( Re ` A ) )
27 13 17 26 3brtr4d 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( ( abs ` A ) x. 0 ) < ( ( abs ` A ) x. ( Re ` ( A / ( abs ` A ) ) ) ) )
28 0re 
 |-  0 e. RR
29 28 a1i 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> 0 e. RR )
30 22 recld 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( Re ` ( A / ( abs ` A ) ) ) e. RR )
31 29 30 20 ltmul2d 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( 0 < ( Re ` ( A / ( abs ` A ) ) ) <-> ( ( abs ` A ) x. 0 ) < ( ( abs ` A ) x. ( Re ` ( A / ( abs ` A ) ) ) ) ) )
32 27 31 mpbird 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> 0 < ( Re ` ( A / ( abs ` A ) ) ) )
33 efiarg 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) = ( A / ( abs ` A ) ) )
34 8 33 syldan 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) = ( A / ( abs ` A ) ) )
35 34 fveq2d 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( Re ` ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) ) = ( Re ` ( A / ( abs ` A ) ) ) )
36 32 35 breqtrrd 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> 0 < ( Re ` ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) ) )
37 recosval 
 |-  ( ( Im ` ( log ` A ) ) e. RR -> ( cos ` ( Im ` ( log ` A ) ) ) = ( Re ` ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) ) )
38 11 37 syl 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( cos ` ( Im ` ( log ` A ) ) ) = ( Re ` ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) ) )
39 36 38 breqtrrd 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> 0 < ( cos ` ( Im ` ( log ` A ) ) ) )
40 fveq2 
 |-  ( ( abs ` ( Im ` ( log ` A ) ) ) = ( Im ` ( log ` A ) ) -> ( cos ` ( abs ` ( Im ` ( log ` A ) ) ) ) = ( cos ` ( Im ` ( log ` A ) ) ) )
41 40 a1i 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( ( abs ` ( Im ` ( log ` A ) ) ) = ( Im ` ( log ` A ) ) -> ( cos ` ( abs ` ( Im ` ( log ` A ) ) ) ) = ( cos ` ( Im ` ( log ` A ) ) ) ) )
42 11 recnd 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` A ) ) e. CC )
43 cosneg 
 |-  ( ( Im ` ( log ` A ) ) e. CC -> ( cos ` -u ( Im ` ( log ` A ) ) ) = ( cos ` ( Im ` ( log ` A ) ) ) )
44 42 43 syl 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( cos ` -u ( Im ` ( log ` A ) ) ) = ( cos ` ( Im ` ( log ` A ) ) ) )
45 fveqeq2 
 |-  ( ( abs ` ( Im ` ( log ` A ) ) ) = -u ( Im ` ( log ` A ) ) -> ( ( cos ` ( abs ` ( Im ` ( log ` A ) ) ) ) = ( cos ` ( Im ` ( log ` A ) ) ) <-> ( cos ` -u ( Im ` ( log ` A ) ) ) = ( cos ` ( Im ` ( log ` A ) ) ) ) )
46 44 45 syl5ibrcom 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( ( abs ` ( Im ` ( log ` A ) ) ) = -u ( Im ` ( log ` A ) ) -> ( cos ` ( abs ` ( Im ` ( log ` A ) ) ) ) = ( cos ` ( Im ` ( log ` A ) ) ) ) )
47 11 absord 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( ( abs ` ( Im ` ( log ` A ) ) ) = ( Im ` ( log ` A ) ) \/ ( abs ` ( Im ` ( log ` A ) ) ) = -u ( Im ` ( log ` A ) ) ) )
48 41 46 47 mpjaod 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( cos ` ( abs ` ( Im ` ( log ` A ) ) ) ) = ( cos ` ( Im ` ( log ` A ) ) ) )
49 39 48 breqtrrd 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> 0 < ( cos ` ( abs ` ( Im ` ( log ` A ) ) ) ) )
50 12 49 eqbrtrid 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( cos ` ( _pi / 2 ) ) < ( cos ` ( abs ` ( Im ` ( log ` A ) ) ) ) )
51 42 abscld 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( abs ` ( Im ` ( log ` A ) ) ) e. RR )
52 42 absge0d 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> 0 <_ ( abs ` ( Im ` ( log ` A ) ) ) )
53 logimcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ _pi ) )
54 8 53 syldan 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ _pi ) )
55 54 simpld 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> -u _pi < ( Im ` ( log ` A ) ) )
56 pire 
 |-  _pi e. RR
57 56 renegcli 
 |-  -u _pi e. RR
58 ltle 
 |-  ( ( -u _pi e. RR /\ ( Im ` ( log ` A ) ) e. RR ) -> ( -u _pi < ( Im ` ( log ` A ) ) -> -u _pi <_ ( Im ` ( log ` A ) ) ) )
59 57 11 58 sylancr 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( -u _pi < ( Im ` ( log ` A ) ) -> -u _pi <_ ( Im ` ( log ` A ) ) ) )
60 55 59 mpd 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> -u _pi <_ ( Im ` ( log ` A ) ) )
61 54 simprd 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` A ) ) <_ _pi )
62 absle 
 |-  ( ( ( Im ` ( log ` A ) ) e. RR /\ _pi e. RR ) -> ( ( abs ` ( Im ` ( log ` A ) ) ) <_ _pi <-> ( -u _pi <_ ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ _pi ) ) )
63 11 56 62 sylancl 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( ( abs ` ( Im ` ( log ` A ) ) ) <_ _pi <-> ( -u _pi <_ ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ _pi ) ) )
64 60 61 63 mpbir2and 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( abs ` ( Im ` ( log ` A ) ) ) <_ _pi )
65 28 56 elicc2i 
 |-  ( ( abs ` ( Im ` ( log ` A ) ) ) e. ( 0 [,] _pi ) <-> ( ( abs ` ( Im ` ( log ` A ) ) ) e. RR /\ 0 <_ ( abs ` ( Im ` ( log ` A ) ) ) /\ ( abs ` ( Im ` ( log ` A ) ) ) <_ _pi ) )
66 51 52 64 65 syl3anbrc 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( abs ` ( Im ` ( log ` A ) ) ) e. ( 0 [,] _pi ) )
67 halfpire 
 |-  ( _pi / 2 ) e. RR
68 pirp 
 |-  _pi e. RR+
69 rphalfcl 
 |-  ( _pi e. RR+ -> ( _pi / 2 ) e. RR+ )
70 rpge0 
 |-  ( ( _pi / 2 ) e. RR+ -> 0 <_ ( _pi / 2 ) )
71 68 69 70 mp2b 
 |-  0 <_ ( _pi / 2 )
72 rphalflt 
 |-  ( _pi e. RR+ -> ( _pi / 2 ) < _pi )
73 68 72 ax-mp 
 |-  ( _pi / 2 ) < _pi
74 67 56 73 ltleii 
 |-  ( _pi / 2 ) <_ _pi
75 28 56 elicc2i 
 |-  ( ( _pi / 2 ) e. ( 0 [,] _pi ) <-> ( ( _pi / 2 ) e. RR /\ 0 <_ ( _pi / 2 ) /\ ( _pi / 2 ) <_ _pi ) )
76 67 71 74 75 mpbir3an 
 |-  ( _pi / 2 ) e. ( 0 [,] _pi )
77 cosord 
 |-  ( ( ( abs ` ( Im ` ( log ` A ) ) ) e. ( 0 [,] _pi ) /\ ( _pi / 2 ) e. ( 0 [,] _pi ) ) -> ( ( abs ` ( Im ` ( log ` A ) ) ) < ( _pi / 2 ) <-> ( cos ` ( _pi / 2 ) ) < ( cos ` ( abs ` ( Im ` ( log ` A ) ) ) ) ) )
78 66 76 77 sylancl 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( ( abs ` ( Im ` ( log ` A ) ) ) < ( _pi / 2 ) <-> ( cos ` ( _pi / 2 ) ) < ( cos ` ( abs ` ( Im ` ( log ` A ) ) ) ) ) )
79 50 78 mpbird 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( abs ` ( Im ` ( log ` A ) ) ) < ( _pi / 2 ) )
80 abslt 
 |-  ( ( ( Im ` ( log ` A ) ) e. RR /\ ( _pi / 2 ) e. RR ) -> ( ( abs ` ( Im ` ( log ` A ) ) ) < ( _pi / 2 ) <-> ( -u ( _pi / 2 ) < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) < ( _pi / 2 ) ) ) )
81 11 67 80 sylancl 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( ( abs ` ( Im ` ( log ` A ) ) ) < ( _pi / 2 ) <-> ( -u ( _pi / 2 ) < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) < ( _pi / 2 ) ) ) )
82 79 81 mpbid 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( -u ( _pi / 2 ) < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) < ( _pi / 2 ) ) )
83 82 simpld 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> -u ( _pi / 2 ) < ( Im ` ( log ` A ) ) )
84 82 simprd 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` A ) ) < ( _pi / 2 ) )
85 67 renegcli 
 |-  -u ( _pi / 2 ) e. RR
86 85 rexri 
 |-  -u ( _pi / 2 ) e. RR*
87 67 rexri 
 |-  ( _pi / 2 ) e. RR*
88 elioo2 
 |-  ( ( -u ( _pi / 2 ) e. RR* /\ ( _pi / 2 ) e. RR* ) -> ( ( Im ` ( log ` A ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) <-> ( ( Im ` ( log ` A ) ) e. RR /\ -u ( _pi / 2 ) < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) < ( _pi / 2 ) ) ) )
89 86 87 88 mp2an 
 |-  ( ( Im ` ( log ` A ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) <-> ( ( Im ` ( log ` A ) ) e. RR /\ -u ( _pi / 2 ) < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) < ( _pi / 2 ) ) )
90 11 83 84 89 syl3anbrc 
 |-  ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` A ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )