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 
|- ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( Im ` ( log ` A ) ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )

Proof

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