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

Metamath Proof Explorer

Theorem re0cj

Description: The conjugate of a pure imaginary number is its negative. (Contributed by Thierry Arnoux, 25-Jun-2025)

Ref Expression
Hypotheses re0cj.1 
|- ( ph -> A e. CC )
re0cj.2 
|- ( ph -> ( Re ` A ) = 0 )
Assertion re0cj 
|- ( ph -> ( * ` A ) = -u A )

Proof

Step Hyp Ref Expression
1 re0cj.1 
 |-  ( ph -> A e. CC )
2 re0cj.2 
 |-  ( ph -> ( Re ` A ) = 0 )
3 2 oveq1d 
 |-  ( ph -> ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) = ( 0 - ( _i x. ( Im ` A ) ) ) )
4 df-neg 
 |-  -u ( _i x. ( Im ` A ) ) = ( 0 - ( _i x. ( Im ` A ) ) )
5 3 4 eqtr4di 
 |-  ( ph -> ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) = -u ( _i x. ( Im ` A ) ) )
6 1 remimd 
 |-  ( ph -> ( * ` A ) = ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) )
7 1 replimd 
 |-  ( ph -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )
8 2 oveq1d 
 |-  ( ph -> ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) = ( 0 + ( _i x. ( Im ` A ) ) ) )
9 ax-icn 
 |-  _i e. CC
10 9 a1i 
 |-  ( ph -> _i e. CC )
11 1 imcld 
 |-  ( ph -> ( Im ` A ) e. RR )
12 11 recnd 
 |-  ( ph -> ( Im ` A ) e. CC )
13 10 12 mulcld 
 |-  ( ph -> ( _i x. ( Im ` A ) ) e. CC )
14 13 addlidd 
 |-  ( ph -> ( 0 + ( _i x. ( Im ` A ) ) ) = ( _i x. ( Im ` A ) ) )
15 7 8 14 3eqtrd 
 |-  ( ph -> A = ( _i x. ( Im ` A ) ) )
16 15 negeqd 
 |-  ( ph -> -u A = -u ( _i x. ( Im ` A ) ) )
17 5 6 16 3eqtr4d 
 |-  ( ph -> ( * ` A ) = -u A )