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

Metamath Proof Explorer

Theorem logneg

Description: The natural logarithm of a negative real number. (Contributed by Mario Carneiro, 13-May-2014) (Revised by Mario Carneiro, 3-Apr-2015)

Ref Expression
Assertion logneg 
|- ( A e. RR+ -> ( log ` -u A ) = ( ( log ` A ) + ( _i x. _pi ) ) )

Proof

Step Hyp Ref Expression
1 relogcl 
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
2 1 recnd 
 |-  ( A e. RR+ -> ( log ` A ) e. CC )
3 ax-icn 
 |-  _i e. CC
4 picn 
 |-  _pi e. CC
5 3 4 mulcli 
 |-  ( _i x. _pi ) e. CC
6 efadd 
 |-  ( ( ( log ` A ) e. CC /\ ( _i x. _pi ) e. CC ) -> ( exp ` ( ( log ` A ) + ( _i x. _pi ) ) ) = ( ( exp ` ( log ` A ) ) x. ( exp ` ( _i x. _pi ) ) ) )
7 2 5 6 sylancl 
 |-  ( A e. RR+ -> ( exp ` ( ( log ` A ) + ( _i x. _pi ) ) ) = ( ( exp ` ( log ` A ) ) x. ( exp ` ( _i x. _pi ) ) ) )
8 efipi 
 |-  ( exp ` ( _i x. _pi ) ) = -u 1
9 8 oveq2i 
 |-  ( ( exp ` ( log ` A ) ) x. ( exp ` ( _i x. _pi ) ) ) = ( ( exp ` ( log ` A ) ) x. -u 1 )
10 reeflog 
 |-  ( A e. RR+ -> ( exp ` ( log ` A ) ) = A )
11 10 oveq1d 
 |-  ( A e. RR+ -> ( ( exp ` ( log ` A ) ) x. -u 1 ) = ( A x. -u 1 ) )
12 9 11 eqtrid 
 |-  ( A e. RR+ -> ( ( exp ` ( log ` A ) ) x. ( exp ` ( _i x. _pi ) ) ) = ( A x. -u 1 ) )
13 rpcn 
 |-  ( A e. RR+ -> A e. CC )
14 neg1cn 
 |-  -u 1 e. CC
15 mulcom 
 |-  ( ( A e. CC /\ -u 1 e. CC ) -> ( A x. -u 1 ) = ( -u 1 x. A ) )
16 13 14 15 sylancl 
 |-  ( A e. RR+ -> ( A x. -u 1 ) = ( -u 1 x. A ) )
17 13 mulm1d 
 |-  ( A e. RR+ -> ( -u 1 x. A ) = -u A )
18 16 17 eqtrd 
 |-  ( A e. RR+ -> ( A x. -u 1 ) = -u A )
19 7 12 18 3eqtrd 
 |-  ( A e. RR+ -> ( exp ` ( ( log ` A ) + ( _i x. _pi ) ) ) = -u A )
20 19 fveq2d 
 |-  ( A e. RR+ -> ( log ` ( exp ` ( ( log ` A ) + ( _i x. _pi ) ) ) ) = ( log ` -u A ) )
21 addcl 
 |-  ( ( ( log ` A ) e. CC /\ ( _i x. _pi ) e. CC ) -> ( ( log ` A ) + ( _i x. _pi ) ) e. CC )
22 2 5 21 sylancl 
 |-  ( A e. RR+ -> ( ( log ` A ) + ( _i x. _pi ) ) e. CC )
23 pipos 
 |-  0 < _pi
24 pire 
 |-  _pi e. RR
25 lt0neg2 
 |-  ( _pi e. RR -> ( 0 < _pi <-> -u _pi < 0 ) )
26 24 25 ax-mp 
 |-  ( 0 < _pi <-> -u _pi < 0 )
27 23 26 mpbi 
 |-  -u _pi < 0
28 24 renegcli 
 |-  -u _pi e. RR
29 0re 
 |-  0 e. RR
30 28 29 24 lttri 
 |-  ( ( -u _pi < 0 /\ 0 < _pi ) -> -u _pi < _pi )
31 27 23 30 mp2an 
 |-  -u _pi < _pi
32 crim 
 |-  ( ( ( log ` A ) e. RR /\ _pi e. RR ) -> ( Im ` ( ( log ` A ) + ( _i x. _pi ) ) ) = _pi )
33 1 24 32 sylancl 
 |-  ( A e. RR+ -> ( Im ` ( ( log ` A ) + ( _i x. _pi ) ) ) = _pi )
34 31 33 breqtrrid 
 |-  ( A e. RR+ -> -u _pi < ( Im ` ( ( log ` A ) + ( _i x. _pi ) ) ) )
35 24 leidi 
 |-  _pi <_ _pi
36 33 35 eqbrtrdi 
 |-  ( A e. RR+ -> ( Im ` ( ( log ` A ) + ( _i x. _pi ) ) ) <_ _pi )
37 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 ) )
38 22 34 36 37 syl3anbrc 
 |-  ( A e. RR+ -> ( ( log ` A ) + ( _i x. _pi ) ) e. ran log )
39 logef 
 |-  ( ( ( log ` A ) + ( _i x. _pi ) ) e. ran log -> ( log ` ( exp ` ( ( log ` A ) + ( _i x. _pi ) ) ) ) = ( ( log ` A ) + ( _i x. _pi ) ) )
40 38 39 syl 
 |-  ( A e. RR+ -> ( log ` ( exp ` ( ( log ` A ) + ( _i x. _pi ) ) ) ) = ( ( log ` A ) + ( _i x. _pi ) ) )
41 20 40 eqtr3d 
 |-  ( A e. RR+ -> ( log ` -u A ) = ( ( log ` A ) + ( _i x. _pi ) ) )