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 syl5ib
 |-  ( ( -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 ) ) )