Metamath Proof Explorer

Theorem logneg2

Description: The logarithm of the negative of a number with positive imaginary part is _i x. _pi less than the original. (Compare logneg .) (Contributed by Mario Carneiro, 3-Apr-2015)

Ref Expression
Assertion logneg2 
|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( log ` -u A ) = ( ( log ` A ) - ( _i x. _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 ax-icn 
 |-  _i e. CC
12 picn 
 |-  _pi e. CC
13 11 12 mulcli 
 |-  ( _i x. _pi ) e. CC
14 efsub 
 |-  ( ( ( log ` A ) e. CC /\ ( _i x. _pi ) e. CC ) -> ( exp ` ( ( log ` A ) - ( _i x. _pi ) ) ) = ( ( exp ` ( log ` A ) ) / ( exp ` ( _i x. _pi ) ) ) )
15 10 13 14 sylancl 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( exp ` ( ( log ` A ) - ( _i x. _pi ) ) ) = ( ( exp ` ( log ` A ) ) / ( exp ` ( _i x. _pi ) ) ) )
16 eflog 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = A )
17 8 16 syldan 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( exp ` ( log ` A ) ) = A )
18 efipi 
 |-  ( exp ` ( _i x. _pi ) ) = -u 1
19 18 a1i 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( exp ` ( _i x. _pi ) ) = -u 1 )
20 17 19 oveq12d 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( ( exp ` ( log ` A ) ) / ( exp ` ( _i x. _pi ) ) ) = ( A / -u 1 ) )
21 ax-1cn 
 |-  1 e. CC
22 ax-1ne0 
 |-  1 =/= 0
23 divneg2 
 |-  ( ( A e. CC /\ 1 e. CC /\ 1 =/= 0 ) -> -u ( A / 1 ) = ( A / -u 1 ) )
24 21 22 23 mp3an23 
 |-  ( A e. CC -> -u ( A / 1 ) = ( A / -u 1 ) )
25 div1 
 |-  ( A e. CC -> ( A / 1 ) = A )
26 25 negeqd 
 |-  ( A e. CC -> -u ( A / 1 ) = -u A )
27 24 26 eqtr3d 
 |-  ( A e. CC -> ( A / -u 1 ) = -u A )
28 27 adantr 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( A / -u 1 ) = -u A )
29 15 20 28 3eqtrd 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( exp ` ( ( log ` A ) - ( _i x. _pi ) ) ) = -u A )
30 29 fveq2d 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( log ` ( exp ` ( ( log ` A ) - ( _i x. _pi ) ) ) ) = ( log ` -u A ) )
31 subcl 
 |-  ( ( ( log ` A ) e. CC /\ ( _i x. _pi ) e. CC ) -> ( ( log ` A ) - ( _i x. _pi ) ) e. CC )
32 10 13 31 sylancl 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( ( log ` A ) - ( _i x. _pi ) ) e. CC )
33 argimgt0 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( Im ` ( log ` A ) ) e. ( 0 (,) _pi ) )
34 eliooord 
 |-  ( ( Im ` ( log ` A ) ) e. ( 0 (,) _pi ) -> ( 0 < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) < _pi ) )
35 33 34 syl 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( 0 < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) < _pi ) )
36 35 simpld 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> 0 < ( Im ` ( log ` A ) ) )
37 imcl 
 |-  ( ( log ` A ) e. CC -> ( Im ` ( log ` A ) ) e. RR )
38 10 37 syl 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( Im ` ( log ` A ) ) e. RR )
39 pire 
 |-  _pi e. RR
40 39 renegcli 
 |-  -u _pi e. RR
41 ltaddpos2 
 |-  ( ( ( Im ` ( log ` A ) ) e. RR /\ -u _pi e. RR ) -> ( 0 < ( Im ` ( log ` A ) ) <-> -u _pi < ( ( Im ` ( log ` A ) ) + -u _pi ) ) )
42 38 40 41 sylancl 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( 0 < ( Im ` ( log ` A ) ) <-> -u _pi < ( ( Im ` ( log ` A ) ) + -u _pi ) ) )
43 36 42 mpbid 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> -u _pi < ( ( Im ` ( log ` A ) ) + -u _pi ) )
44 38 recnd 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( Im ` ( log ` A ) ) e. CC )
45 negsub 
 |-  ( ( ( Im ` ( log ` A ) ) e. CC /\ _pi e. CC ) -> ( ( Im ` ( log ` A ) ) + -u _pi ) = ( ( Im ` ( log ` A ) ) - _pi ) )
46 44 12 45 sylancl 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( ( Im ` ( log ` A ) ) + -u _pi ) = ( ( Im ` ( log ` A ) ) - _pi ) )
47 43 46 breqtrd 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> -u _pi < ( ( Im ` ( log ` A ) ) - _pi ) )
48 imsub 
 |-  ( ( ( log ` A ) e. CC /\ ( _i x. _pi ) e. CC ) -> ( Im ` ( ( log ` A ) - ( _i x. _pi ) ) ) = ( ( Im ` ( log ` A ) ) - ( Im ` ( _i x. _pi ) ) ) )
49 10 13 48 sylancl 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( Im ` ( ( log ` A ) - ( _i x. _pi ) ) ) = ( ( Im ` ( log ` A ) ) - ( Im ` ( _i x. _pi ) ) ) )
50 reim 
 |-  ( _pi e. CC -> ( Re ` _pi ) = ( Im ` ( _i x. _pi ) ) )
51 12 50 ax-mp 
 |-  ( Re ` _pi ) = ( Im ` ( _i x. _pi ) )
52 rere 
 |-  ( _pi e. RR -> ( Re ` _pi ) = _pi )
53 39 52 ax-mp 
 |-  ( Re ` _pi ) = _pi
54 51 53 eqtr3i 
 |-  ( Im ` ( _i x. _pi ) ) = _pi
55 54 oveq2i 
 |-  ( ( Im ` ( log ` A ) ) - ( Im ` ( _i x. _pi ) ) ) = ( ( Im ` ( log ` A ) ) - _pi )
56 49 55 eqtrdi 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( Im ` ( ( log ` A ) - ( _i x. _pi ) ) ) = ( ( Im ` ( log ` A ) ) - _pi ) )
57 47 56 breqtrrd 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> -u _pi < ( Im ` ( ( log ` A ) - ( _i x. _pi ) ) ) )
58 resubcl 
 |-  ( ( ( Im ` ( log ` A ) ) e. RR /\ _pi e. RR ) -> ( ( Im ` ( log ` A ) ) - _pi ) e. RR )
59 38 39 58 sylancl 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( ( Im ` ( log ` A ) ) - _pi ) e. RR )
60 39 a1i 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> _pi e. RR )
61 0re 
 |-  0 e. RR
62 pipos 
 |-  0 < _pi
63 61 39 62 ltleii 
 |-  0 <_ _pi
64 subge02 
 |-  ( ( ( Im ` ( log ` A ) ) e. RR /\ _pi e. RR ) -> ( 0 <_ _pi <-> ( ( Im ` ( log ` A ) ) - _pi ) <_ ( Im ` ( log ` A ) ) ) )
65 38 39 64 sylancl 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( 0 <_ _pi <-> ( ( Im ` ( log ` A ) ) - _pi ) <_ ( Im ` ( log ` A ) ) ) )
66 63 65 mpbii 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( ( Im ` ( log ` A ) ) - _pi ) <_ ( Im ` ( log ` A ) ) )
67 logimcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ _pi ) )
68 8 67 syldan 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ _pi ) )
69 68 simprd 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( Im ` ( log ` A ) ) <_ _pi )
70 59 38 60 66 69 letrd 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( ( Im ` ( log ` A ) ) - _pi ) <_ _pi )
71 56 70 eqbrtrd 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( Im ` ( ( log ` A ) - ( _i x. _pi ) ) ) <_ _pi )
72 ellogrn 
 |-  ( ( ( log ` A ) - ( _i x. _pi ) ) e. ran log <-> ( ( ( log ` A ) - ( _i x. _pi ) ) e. CC /\ -u _pi < ( Im ` ( ( log ` A ) - ( _i x. _pi ) ) ) /\ ( Im ` ( ( log ` A ) - ( _i x. _pi ) ) ) <_ _pi ) )
73 32 57 71 72 syl3anbrc 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( ( log ` A ) - ( _i x. _pi ) ) e. ran log )
74 logef 
 |-  ( ( ( log ` A ) - ( _i x. _pi ) ) e. ran log -> ( log ` ( exp ` ( ( log ` A ) - ( _i x. _pi ) ) ) ) = ( ( log ` A ) - ( _i x. _pi ) ) )
75 73 74 syl 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( log ` ( exp ` ( ( log ` A ) - ( _i x. _pi ) ) ) ) = ( ( log ` A ) - ( _i x. _pi ) ) )
76 30 75 eqtr3d 
 |-  ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( log ` -u A ) = ( ( log ` A ) - ( _i x. _pi ) ) )