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

Metamath Proof Explorer

Theorem arginv

Description: The argument of the inverse of a complex number A . (Contributed by Thierry Arnoux, 5-Nov-2025)

Ref Expression
Hypotheses efiargd.1 
|- ( ph -> A e. CC )
efiargd.2 
|- ( ph -> A =/= 0 )
arginv.1 
|- ( ph -> -. -u A e. RR+ )
Assertion arginv 
|- ( ph -> ( Im ` ( log ` ( 1 / A ) ) ) = -u ( Im ` ( log ` A ) ) )

Proof

Step Hyp Ref Expression
1 efiargd.1 
 |-  ( ph -> A e. CC )
2 efiargd.2 
 |-  ( ph -> A =/= 0 )
3 arginv.1 
 |-  ( ph -> -. -u A e. RR+ )
4 1 2 logcld 
 |-  ( ph -> ( log ` A ) e. CC )
5 1 2 reccld 
 |-  ( ph -> ( 1 / A ) e. CC )
6 1 2 recne0d 
 |-  ( ph -> ( 1 / A ) =/= 0 )
7 5 6 logcld 
 |-  ( ph -> ( log ` ( 1 / A ) ) e. CC )
8 lognegb 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( -u A e. RR+ <-> ( Im ` ( log ` A ) ) = _pi ) )
9 8 necon3bbid 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( -. -u A e. RR+ <-> ( Im ` ( log ` A ) ) =/= _pi ) )
10 9 biimpa 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ -. -u A e. RR+ ) -> ( Im ` ( log ` A ) ) =/= _pi )
11 1 2 3 10 syl21anc 
 |-  ( ph -> ( Im ` ( log ` A ) ) =/= _pi )
12 logrec 
 |-  ( ( A e. CC /\ A =/= 0 /\ ( Im ` ( log ` A ) ) =/= _pi ) -> ( log ` A ) = -u ( log ` ( 1 / A ) ) )
13 1 2 11 12 syl3anc 
 |-  ( ph -> ( log ` A ) = -u ( log ` ( 1 / A ) ) )
14 negcon2 
 |-  ( ( ( log ` A ) e. CC /\ ( log ` ( 1 / A ) ) e. CC ) -> ( ( log ` A ) = -u ( log ` ( 1 / A ) ) <-> ( log ` ( 1 / A ) ) = -u ( log ` A ) ) )
15 14 biimpa 
 |-  ( ( ( ( log ` A ) e. CC /\ ( log ` ( 1 / A ) ) e. CC ) /\ ( log ` A ) = -u ( log ` ( 1 / A ) ) ) -> ( log ` ( 1 / A ) ) = -u ( log ` A ) )
16 4 7 13 15 syl21anc 
 |-  ( ph -> ( log ` ( 1 / A ) ) = -u ( log ` A ) )
17 16 fveq2d 
 |-  ( ph -> ( Im ` ( log ` ( 1 / A ) ) ) = ( Im ` -u ( log ` A ) ) )
18 4 imnegd 
 |-  ( ph -> ( Im ` -u ( log ` A ) ) = -u ( Im ` ( log ` A ) ) )
19 17 18 eqtrd 
 |-  ( ph -> ( Im ` ( log ` ( 1 / A ) ) ) = -u ( Im ` ( log ` A ) ) )