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 )