Theorem imcj

Description: Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005) (Revised by Mario Carneiro, 14-Jul-2014)

	Ref	Expression
Assertion	imcj	$$⊢A\in ℂ\to \Im \left(\bar{A}\right)=-\Im \left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		recl	$$⊢A\in ℂ\to \Re \left(A\right)\in ℝ$$
2	1	recnd	$$⊢A\in ℂ\to \Re \left(A\right)\in ℂ$$
3		ax-icn	$$⊢\mathrm{i}\in ℂ$$
4		imcl	$$⊢A\in ℂ\to \Im \left(A\right)\in ℝ$$
5	4	recnd	$$⊢A\in ℂ\to \Im \left(A\right)\in ℂ$$
6		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge \Im \left(A\right)\in ℂ\right)\to \mathrm{i}\Im \left(A\right)\in ℂ$$
7	3 5 6	sylancr	$$⊢A\in ℂ\to \mathrm{i}\Im \left(A\right)\in ℂ$$
8	2 7	negsubd	$$⊢A\in ℂ\to \Re \left(A\right)+\left(-\mathrm{i}\Im \left(A\right)\right)=\Re \left(A\right)-\mathrm{i}\Im \left(A\right)$$
9		mulneg2	$$⊢\left(\mathrm{i}\in ℂ\wedge \Im \left(A\right)\in ℂ\right)\to \mathrm{i}\left(-\Im \left(A\right)\right)=-\mathrm{i}\Im \left(A\right)$$
10	3 5 9	sylancr	$$⊢A\in ℂ\to \mathrm{i}\left(-\Im \left(A\right)\right)=-\mathrm{i}\Im \left(A\right)$$
11	10	oveq2d	$$⊢A\in ℂ\to \Re \left(A\right)+\mathrm{i}\left(-\Im \left(A\right)\right)=\Re \left(A\right)+\left(-\mathrm{i}\Im \left(A\right)\right)$$
12		remim	$$⊢A\in ℂ\to \bar{A}=\Re \left(A\right)-\mathrm{i}\Im \left(A\right)$$
13	8 11 12	3eqtr4rd	$$⊢A\in ℂ\to \bar{A}=\Re \left(A\right)+\mathrm{i}\left(-\Im \left(A\right)\right)$$
14	13	fveq2d	$$⊢A\in ℂ\to \Im \left(\bar{A}\right)=\Im \left(\Re \left(A\right)+\mathrm{i}\left(-\Im \left(A\right)\right)\right)$$
15	4	renegcld	$$⊢A\in ℂ\to -\Im \left(A\right)\in ℝ$$
16		crim	$$⊢\left(\Re \left(A\right)\in ℝ\wedge -\Im \left(A\right)\in ℝ\right)\to \Im \left(\Re \left(A\right)+\mathrm{i}\left(-\Im \left(A\right)\right)\right)=-\Im \left(A\right)$$
17	1 15 16	syl2anc	$$⊢A\in ℂ\to \Im \left(\Re \left(A\right)+\mathrm{i}\left(-\Im \left(A\right)\right)\right)=-\Im \left(A\right)$$
18	14 17	eqtrd	$$⊢A\in ℂ\to \Im \left(\bar{A}\right)=-\Im \left(A\right)$$