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	$$⊢\phi \to A\in ℂ$$
	re0cj.2	$$⊢\phi \to \Re \left(A\right)=0$$
Assertion	re0cj	$$⊢\phi \to \bar{A}=-A$$

Proof

Step	Hyp	Ref	Expression
1		re0cj.1	$$⊢\phi \to A\in ℂ$$
2		re0cj.2	$$⊢\phi \to \Re \left(A\right)=0$$
3	2	oveq1d	$$⊢\phi \to \Re \left(A\right)-\mathrm{i}\Im \left(A\right)=0-\mathrm{i}\Im \left(A\right)$$
4		df-neg	$$⊢-\mathrm{i}\Im \left(A\right)=0-\mathrm{i}\Im \left(A\right)$$
5	3 4	eqtr4di	$$⊢\phi \to \Re \left(A\right)-\mathrm{i}\Im \left(A\right)=-\mathrm{i}\Im \left(A\right)$$
6	1	remimd	$$⊢\phi \to \bar{A}=\Re \left(A\right)-\mathrm{i}\Im \left(A\right)$$
7	1	replimd	$$⊢\phi \to A=\Re \left(A\right)+\mathrm{i}\Im \left(A\right)$$
8	2	oveq1d	$$⊢\phi \to \Re \left(A\right)+\mathrm{i}\Im \left(A\right)=0+\mathrm{i}\Im \left(A\right)$$
9		ax-icn	$$⊢\mathrm{i}\in ℂ$$
10	9	a1i	$$⊢\phi \to \mathrm{i}\in ℂ$$
11	1	imcld	$$⊢\phi \to \Im \left(A\right)\in ℝ$$
12	11	recnd	$$⊢\phi \to \Im \left(A\right)\in ℂ$$
13	10 12	mulcld	$$⊢\phi \to \mathrm{i}\Im \left(A\right)\in ℂ$$
14	13	addlidd	$$⊢\phi \to 0+\mathrm{i}\Im \left(A\right)=\mathrm{i}\Im \left(A\right)$$
15	7 8 14	3eqtrd	$$⊢\phi \to A=\mathrm{i}\Im \left(A\right)$$
16	15	negeqd	$$⊢\phi \to -A=-\mathrm{i}\Im \left(A\right)$$
17	5 6 16	3eqtr4d	$$⊢\phi \to \bar{A}=-A$$