Metamath Proof Explorer

Theorem argcj

Description: The argument of the conjugate 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 argcj 
|- ( ph -> ( Im ` ( log ` ( * ` 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 simpr 
 |-  ( ( ph /\ A e. RR ) -> A e. RR )
5 2 adantr 
 |-  ( ( ph /\ A e. RR ) -> A =/= 0 )
6 3 adantr 
 |-  ( ( ph /\ A e. RR ) -> -. -u A e. RR+ )
7 rpneg 
 |-  ( ( A e. RR /\ A =/= 0 ) -> ( A e. RR+ <-> -. -u A e. RR+ ) )
8 7 biimpar 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ -. -u A e. RR+ ) -> A e. RR+ )
9 4 5 6 8 syl21anc 
 |-  ( ( ph /\ A e. RR ) -> A e. RR+ )
10 9 relogcld 
 |-  ( ( ph /\ A e. RR ) -> ( log ` A ) e. RR )
11 10 reim0d 
 |-  ( ( ph /\ A e. RR ) -> ( Im ` ( log ` A ) ) = 0 )
12 4 cjred 
 |-  ( ( ph /\ A e. RR ) -> ( * ` A ) = A )
13 12 fveq2d 
 |-  ( ( ph /\ A e. RR ) -> ( log ` ( * ` A ) ) = ( log ` A ) )
14 13 fveq2d 
 |-  ( ( ph /\ A e. RR ) -> ( Im ` ( log ` ( * ` A ) ) ) = ( Im ` ( log ` A ) ) )
15 11 negeqd 
 |-  ( ( ph /\ A e. RR ) -> -u ( Im ` ( log ` A ) ) = -u 0 )
16 neg0 
 |-  -u 0 = 0
17 15 16 eqtrdi 
 |-  ( ( ph /\ A e. RR ) -> -u ( Im ` ( log ` A ) ) = 0 )
18 11 14 17 3eqtr4d 
 |-  ( ( ph /\ A e. RR ) -> ( Im ` ( log ` ( * ` A ) ) ) = -u ( Im ` ( log ` A ) ) )
19 1 adantr 
 |-  ( ( ph /\ ( Im ` A ) = 0 ) -> A e. CC )
20 simpr 
 |-  ( ( ph /\ ( Im ` A ) = 0 ) -> ( Im ` A ) = 0 )
21 19 20 reim0bd 
 |-  ( ( ph /\ ( Im ` A ) = 0 ) -> A e. RR )
22 21 ex 
 |-  ( ph -> ( ( Im ` A ) = 0 -> A e. RR ) )
23 22 necon3bd 
 |-  ( ph -> ( -. A e. RR -> ( Im ` A ) =/= 0 ) )
24 23 imp 
 |-  ( ( ph /\ -. A e. RR ) -> ( Im ` A ) =/= 0 )
25 logcj 
 |-  ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( log ` ( * ` A ) ) = ( * ` ( log ` A ) ) )
26 1 24 25 syl2an2r 
 |-  ( ( ph /\ -. A e. RR ) -> ( log ` ( * ` A ) ) = ( * ` ( log ` A ) ) )
27 26 fveq2d 
 |-  ( ( ph /\ -. A e. RR ) -> ( Im ` ( log ` ( * ` A ) ) ) = ( Im ` ( * ` ( log ` A ) ) ) )
28 1 adantr 
 |-  ( ( ph /\ -. A e. RR ) -> A e. CC )
29 2 adantr 
 |-  ( ( ph /\ -. A e. RR ) -> A =/= 0 )
30 28 29 logcld 
 |-  ( ( ph /\ -. A e. RR ) -> ( log ` A ) e. CC )
31 30 imcjd 
 |-  ( ( ph /\ -. A e. RR ) -> ( Im ` ( * ` ( log ` A ) ) ) = -u ( Im ` ( log ` A ) ) )
32 27 31 eqtrd 
 |-  ( ( ph /\ -. A e. RR ) -> ( Im ` ( log ` ( * ` A ) ) ) = -u ( Im ` ( log ` A ) ) )
33 18 32 pm2.61dan 
 |-  ( ph -> ( Im ` ( log ` ( * ` A ) ) ) = -u ( Im ` ( log ` A ) ) )