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

Metamath Proof Explorer

Theorem logrec

Description: Logarithm of a reciprocal changes sign. (Contributed by Saveliy Skresanov, 28-Dec-2016)

Ref Expression
Assertion logrec 
|- ( ( A e. CC /\ A =/= 0 /\ ( Im ` ( log ` A ) ) =/= _pi ) -> ( log ` A ) = -u ( log ` ( 1 / A ) ) )

Proof

Step Hyp Ref Expression
1 reccl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( 1 / A ) e. CC )
2 recne0 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( 1 / A ) =/= 0 )
3 eflog 
 |-  ( ( ( 1 / A ) e. CC /\ ( 1 / A ) =/= 0 ) -> ( exp ` ( log ` ( 1 / A ) ) ) = ( 1 / A ) )
4 1 2 3 syl2anc 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` ( 1 / A ) ) ) = ( 1 / A ) )
5 4 eqcomd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( 1 / A ) = ( exp ` ( log ` ( 1 / A ) ) ) )
6 5 oveq2d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( 1 / ( 1 / A ) ) = ( 1 / ( exp ` ( log ` ( 1 / A ) ) ) ) )
7 eflog 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = A )
8 recrec 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( 1 / ( 1 / A ) ) = A )
9 7 8 eqtr4d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = ( 1 / ( 1 / A ) ) )
10 1 2 logcld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` ( 1 / A ) ) e. CC )
11 efneg 
 |-  ( ( log ` ( 1 / A ) ) e. CC -> ( exp ` -u ( log ` ( 1 / A ) ) ) = ( 1 / ( exp ` ( log ` ( 1 / A ) ) ) ) )
12 10 11 syl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` -u ( log ` ( 1 / A ) ) ) = ( 1 / ( exp ` ( log ` ( 1 / A ) ) ) ) )
13 6 9 12 3eqtr4d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = ( exp ` -u ( log ` ( 1 / A ) ) ) )
14 13 3adant3 
 |-  ( ( A e. CC /\ A =/= 0 /\ ( Im ` ( log ` A ) ) =/= _pi ) -> ( exp ` ( log ` A ) ) = ( exp ` -u ( log ` ( 1 / A ) ) ) )
15 14 fveq2d 
 |-  ( ( A e. CC /\ A =/= 0 /\ ( Im ` ( log ` A ) ) =/= _pi ) -> ( log ` ( exp ` ( log ` A ) ) ) = ( log ` ( exp ` -u ( log ` ( 1 / A ) ) ) ) )
16 logrncl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. ran log )
17 16 3adant3 
 |-  ( ( A e. CC /\ A =/= 0 /\ ( Im ` ( log ` A ) ) =/= _pi ) -> ( log ` A ) e. ran log )
18 logef 
 |-  ( ( log ` A ) e. ran log -> ( log ` ( exp ` ( log ` A ) ) ) = ( log ` A ) )
19 17 18 syl 
 |-  ( ( A e. CC /\ A =/= 0 /\ ( Im ` ( log ` A ) ) =/= _pi ) -> ( log ` ( exp ` ( log ` A ) ) ) = ( log ` A ) )
20 df-ne 
 |-  ( ( Im ` ( log ` A ) ) =/= _pi <-> -. ( Im ` ( log ` A ) ) = _pi )
21 lognegb 
 |-  ( ( ( 1 / A ) e. CC /\ ( 1 / A ) =/= 0 ) -> ( -u ( 1 / A ) e. RR+ <-> ( Im ` ( log ` ( 1 / A ) ) ) = _pi ) )
22 1 2 21 syl2anc 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( -u ( 1 / A ) e. RR+ <-> ( Im ` ( log ` ( 1 / A ) ) ) = _pi ) )
23 22 biimprd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( Im ` ( log ` ( 1 / A ) ) ) = _pi -> -u ( 1 / A ) e. RR+ ) )
24 ax-1cn 
 |-  1 e. CC
25 divneg2 
 |-  ( ( 1 e. CC /\ A e. CC /\ A =/= 0 ) -> -u ( 1 / A ) = ( 1 / -u A ) )
26 24 25 mp3an1 
 |-  ( ( A e. CC /\ A =/= 0 ) -> -u ( 1 / A ) = ( 1 / -u A ) )
27 26 eleq1d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( -u ( 1 / A ) e. RR+ <-> ( 1 / -u A ) e. RR+ ) )
28 23 27 sylibd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( Im ` ( log ` ( 1 / A ) ) ) = _pi -> ( 1 / -u A ) e. RR+ ) )
29 negcl 
 |-  ( A e. CC -> -u A e. CC )
30 negeq0 
 |-  ( A e. CC -> ( A = 0 <-> -u A = 0 ) )
31 30 necon3bid 
 |-  ( A e. CC -> ( A =/= 0 <-> -u A =/= 0 ) )
32 31 biimpa 
 |-  ( ( A e. CC /\ A =/= 0 ) -> -u A =/= 0 )
33 rpreccl 
 |-  ( ( 1 / -u A ) e. RR+ -> ( 1 / ( 1 / -u A ) ) e. RR+ )
34 recrec 
 |-  ( ( -u A e. CC /\ -u A =/= 0 ) -> ( 1 / ( 1 / -u A ) ) = -u A )
35 34 eleq1d 
 |-  ( ( -u A e. CC /\ -u A =/= 0 ) -> ( ( 1 / ( 1 / -u A ) ) e. RR+ <-> -u A e. RR+ ) )
36 33 35 imbitrid 
 |-  ( ( -u A e. CC /\ -u A =/= 0 ) -> ( ( 1 / -u A ) e. RR+ -> -u A e. RR+ ) )
37 29 32 36 syl2an2r 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( 1 / -u A ) e. RR+ -> -u A e. RR+ ) )
38 28 37 syld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( Im ` ( log ` ( 1 / A ) ) ) = _pi -> -u A e. RR+ ) )
39 lognegb 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( -u A e. RR+ <-> ( Im ` ( log ` A ) ) = _pi ) )
40 38 39 sylibd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( Im ` ( log ` ( 1 / A ) ) ) = _pi -> ( Im ` ( log ` A ) ) = _pi ) )
41 40 con3d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( -. ( Im ` ( log ` A ) ) = _pi -> -. ( Im ` ( log ` ( 1 / A ) ) ) = _pi ) )
42 41 3impia 
 |-  ( ( A e. CC /\ A =/= 0 /\ -. ( Im ` ( log ` A ) ) = _pi ) -> -. ( Im ` ( log ` ( 1 / A ) ) ) = _pi )
43 20 42 syl3an3b 
 |-  ( ( A e. CC /\ A =/= 0 /\ ( Im ` ( log ` A ) ) =/= _pi ) -> -. ( Im ` ( log ` ( 1 / A ) ) ) = _pi )
44 logrncl 
 |-  ( ( ( 1 / A ) e. CC /\ ( 1 / A ) =/= 0 ) -> ( log ` ( 1 / A ) ) e. ran log )
45 1 2 44 syl2anc 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` ( 1 / A ) ) e. ran log )
46 logreclem 
 |-  ( ( ( log ` ( 1 / A ) ) e. ran log /\ -. ( Im ` ( log ` ( 1 / A ) ) ) = _pi ) -> -u ( log ` ( 1 / A ) ) e. ran log )
47 45 46 stoic3 
 |-  ( ( A e. CC /\ A =/= 0 /\ -. ( Im ` ( log ` ( 1 / A ) ) ) = _pi ) -> -u ( log ` ( 1 / A ) ) e. ran log )
48 43 47 syld3an3 
 |-  ( ( A e. CC /\ A =/= 0 /\ ( Im ` ( log ` A ) ) =/= _pi ) -> -u ( log ` ( 1 / A ) ) e. ran log )
49 logef 
 |-  ( -u ( log ` ( 1 / A ) ) e. ran log -> ( log ` ( exp ` -u ( log ` ( 1 / A ) ) ) ) = -u ( log ` ( 1 / A ) ) )
50 48 49 syl 
 |-  ( ( A e. CC /\ A =/= 0 /\ ( Im ` ( log ` A ) ) =/= _pi ) -> ( log ` ( exp ` -u ( log ` ( 1 / A ) ) ) ) = -u ( log ` ( 1 / A ) ) )
51 15 19 50 3eqtr3d 
 |-  ( ( A e. CC /\ A =/= 0 /\ ( Im ` ( log ` A ) ) =/= _pi ) -> ( log ` A ) = -u ( log ` ( 1 / A ) ) )