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	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	re0cj.2	⊢ ( 𝜑 → ( ℜ ‘ 𝐴 ) = 0 )
Assertion	re0cj	⊢ ( 𝜑 → ( ∗ ‘ 𝐴 ) = - 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		re0cj.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		re0cj.2	⊢ ( 𝜑 → ( ℜ ‘ 𝐴 ) = 0 )
3	2	oveq1d	⊢ ( 𝜑 → ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) = ( 0 − ( i · ( ℑ ‘ 𝐴 ) ) ) )
4		df-neg	⊢ - ( i · ( ℑ ‘ 𝐴 ) ) = ( 0 − ( i · ( ℑ ‘ 𝐴 ) ) )
5	3 4	eqtr4di	⊢ ( 𝜑 → ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) = - ( i · ( ℑ ‘ 𝐴 ) ) )
6	1	remimd	⊢ ( 𝜑 → ( ∗ ‘ 𝐴 ) = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) )
7	1	replimd	⊢ ( 𝜑 → 𝐴 = ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
8	2	oveq1d	⊢ ( 𝜑 → ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) = ( 0 + ( i · ( ℑ ‘ 𝐴 ) ) ) )
9		ax-icn	⊢ i ∈ ℂ
10	9	a1i	⊢ ( 𝜑 → i ∈ ℂ )
11	1	imcld	⊢ ( 𝜑 → ( ℑ ‘ 𝐴 ) ∈ ℝ )
12	11	recnd	⊢ ( 𝜑 → ( ℑ ‘ 𝐴 ) ∈ ℂ )
13	10 12	mulcld	⊢ ( 𝜑 → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
14	13	addlidd	⊢ ( 𝜑 → ( 0 + ( i · ( ℑ ‘ 𝐴 ) ) ) = ( i · ( ℑ ‘ 𝐴 ) ) )
15	7 8 14	3eqtrd	⊢ ( 𝜑 → 𝐴 = ( i · ( ℑ ‘ 𝐴 ) ) )
16	15	negeqd	⊢ ( 𝜑 → - 𝐴 = - ( i · ( ℑ ‘ 𝐴 ) ) )
17	5 6 16	3eqtr4d	⊢ ( 𝜑 → ( ∗ ‘ 𝐴 ) = - 𝐴 )