Metamath Proof Explorer

Theorem logcj

Description: The natural logarithm distributes under conjugation away from the branch cut. (Contributed by Mario Carneiro, 25-Feb-2015)

Ref Expression
Assertion logcj 
|- ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( log ` ( * ` A ) ) = ( * ` ( log ` A ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( A = 0 -> ( Im ` A ) = ( Im ` 0 ) )
2 im0 
 |-  ( Im ` 0 ) = 0
3 1 2 eqtrdi 
 |-  ( A = 0 -> ( Im ` A ) = 0 )
4 3 necon3i 
 |-  ( ( Im ` A ) =/= 0 -> A =/= 0 )
5 logcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. CC )
6 4 5 sylan2 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( log ` A ) e. CC )
7 efcj 
 |-  ( ( log ` A ) e. CC -> ( exp ` ( * ` ( log ` A ) ) ) = ( * ` ( exp ` ( log ` A ) ) ) )
8 6 7 syl 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( exp ` ( * ` ( log ` A ) ) ) = ( * ` ( exp ` ( log ` A ) ) ) )
9 eflog 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = A )
10 4 9 sylan2 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( exp ` ( log ` A ) ) = A )
11 10 fveq2d 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( * ` ( exp ` ( log ` A ) ) ) = ( * ` A ) )
12 8 11 eqtrd 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( exp ` ( * ` ( log ` A ) ) ) = ( * ` A ) )
13 cjcl 
 |-  ( A e. CC -> ( * ` A ) e. CC )
14 13 adantr 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( * ` A ) e. CC )
15 simpr 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( Im ` A ) =/= 0 )
16 15 4 syl 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> A =/= 0 )
17 cjne0 
 |-  ( A e. CC -> ( A =/= 0 <-> ( * ` A ) =/= 0 ) )
18 17 adantr 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( A =/= 0 <-> ( * ` A ) =/= 0 ) )
19 16 18 mpbid 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( * ` A ) =/= 0 )
20 6 cjcld 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( * ` ( log ` A ) ) e. CC )
21 6 imcld 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( Im ` ( log ` A ) ) e. RR )
22 pire 
 |-  _pi e. RR
23 22 a1i 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> _pi e. RR )
24 logimcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ _pi ) )
25 4 24 sylan2 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ _pi ) )
26 25 simprd 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( Im ` ( log ` A ) ) <_ _pi )
27 rpre 
 |-  ( -u A e. RR+ -> -u A e. RR )
28 27 renegcld 
 |-  ( -u A e. RR+ -> -u -u A e. RR )
29 negneg 
 |-  ( A e. CC -> -u -u A = A )
30 29 adantr 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> -u -u A = A )
31 30 eleq1d 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( -u -u A e. RR <-> A e. RR ) )
32 28 31 syl5ib 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( -u A e. RR+ -> A e. RR ) )
33 lognegb 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( -u A e. RR+ <-> ( Im ` ( log ` A ) ) = _pi ) )
34 4 33 sylan2 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( -u A e. RR+ <-> ( Im ` ( log ` A ) ) = _pi ) )
35 reim0b 
 |-  ( A e. CC -> ( A e. RR <-> ( Im ` A ) = 0 ) )
36 35 adantr 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( A e. RR <-> ( Im ` A ) = 0 ) )
37 32 34 36 3imtr3d 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( ( Im ` ( log ` A ) ) = _pi -> ( Im ` A ) = 0 ) )
38 37 necon3d 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( ( Im ` A ) =/= 0 -> ( Im ` ( log ` A ) ) =/= _pi ) )
39 15 38 mpd 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( Im ` ( log ` A ) ) =/= _pi )
40 39 necomd 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> _pi =/= ( Im ` ( log ` A ) ) )
41 21 23 26 40 leneltd 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( Im ` ( log ` A ) ) < _pi )
42 ltneg 
 |-  ( ( ( Im ` ( log ` A ) ) e. RR /\ _pi e. RR ) -> ( ( Im ` ( log ` A ) ) < _pi <-> -u _pi < -u ( Im ` ( log ` A ) ) ) )
43 21 22 42 sylancl 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( ( Im ` ( log ` A ) ) < _pi <-> -u _pi < -u ( Im ` ( log ` A ) ) ) )
44 41 43 mpbid 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> -u _pi < -u ( Im ` ( log ` A ) ) )
45 6 imcjd 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( Im ` ( * ` ( log ` A ) ) ) = -u ( Im ` ( log ` A ) ) )
46 44 45 breqtrrd 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> -u _pi < ( Im ` ( * ` ( log ` A ) ) ) )
47 25 simpld 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> -u _pi < ( Im ` ( log ` A ) ) )
48 22 renegcli 
 |-  -u _pi e. RR
49 ltle 
 |-  ( ( -u _pi e. RR /\ ( Im ` ( log ` A ) ) e. RR ) -> ( -u _pi < ( Im ` ( log ` A ) ) -> -u _pi <_ ( Im ` ( log ` A ) ) ) )
50 48 21 49 sylancr 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( -u _pi < ( Im ` ( log ` A ) ) -> -u _pi <_ ( Im ` ( log ` A ) ) ) )
51 47 50 mpd 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> -u _pi <_ ( Im ` ( log ` A ) ) )
52 lenegcon1 
 |-  ( ( _pi e. RR /\ ( Im ` ( log ` A ) ) e. RR ) -> ( -u _pi <_ ( Im ` ( log ` A ) ) <-> -u ( Im ` ( log ` A ) ) <_ _pi ) )
53 22 21 52 sylancr 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( -u _pi <_ ( Im ` ( log ` A ) ) <-> -u ( Im ` ( log ` A ) ) <_ _pi ) )
54 51 53 mpbid 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> -u ( Im ` ( log ` A ) ) <_ _pi )
55 45 54 eqbrtrd 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( Im ` ( * ` ( log ` A ) ) ) <_ _pi )
56 ellogrn 
 |-  ( ( * ` ( log ` A ) ) e. ran log <-> ( ( * ` ( log ` A ) ) e. CC /\ -u _pi < ( Im ` ( * ` ( log ` A ) ) ) /\ ( Im ` ( * ` ( log ` A ) ) ) <_ _pi ) )
57 20 46 55 56 syl3anbrc 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( * ` ( log ` A ) ) e. ran log )
58 logeftb 
 |-  ( ( ( * ` A ) e. CC /\ ( * ` A ) =/= 0 /\ ( * ` ( log ` A ) ) e. ran log ) -> ( ( log ` ( * ` A ) ) = ( * ` ( log ` A ) ) <-> ( exp ` ( * ` ( log ` A ) ) ) = ( * ` A ) ) )
59 14 19 57 58 syl3anc 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( ( log ` ( * ` A ) ) = ( * ` ( log ` A ) ) <-> ( exp ` ( * ` ( log ` A ) ) ) = ( * ` A ) ) )
60 12 59 mpbird 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( log ` ( * ` A ) ) = ( * ` ( log ` A ) ) )