Theorem cjreim

Description: The conjugate of a representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005)

	Ref	Expression
Assertion	cjreim	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \overline{A+\mathrm{i}B}=A-\mathrm{i}B$$

Proof

Step	Hyp	Ref	Expression
1		recn	$$⊢A\in ℝ\to A\in ℂ$$
2		ax-icn	$$⊢\mathrm{i}\in ℂ$$
3		recn	$$⊢B\in ℝ\to B\in ℂ$$
4		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge B\in ℂ\right)\to \mathrm{i}B\in ℂ$$
5	2 3 4	sylancr	$$⊢B\in ℝ\to \mathrm{i}B\in ℂ$$
6		cjadd	$$⊢\left(A\in ℂ\wedge \mathrm{i}B\in ℂ\right)\to \overline{A+\mathrm{i}B}=\bar{A}+\overline{\mathrm{i}B}$$
7	1 5 6	syl2an	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \overline{A+\mathrm{i}B}=\bar{A}+\overline{\mathrm{i}B}$$
8		cjre	$$⊢A\in ℝ\to \bar{A}=A$$
9		cjmul	$$⊢\left(\mathrm{i}\in ℂ\wedge B\in ℂ\right)\to \overline{\mathrm{i}B}=\bar{\mathrm{i}}\bar{B}$$
10	2 3 9	sylancr	$$⊢B\in ℝ\to \overline{\mathrm{i}B}=\bar{\mathrm{i}}\bar{B}$$
11		cji	$$⊢\bar{\mathrm{i}}=-\mathrm{i}$$
12	11	a1i	$$⊢B\in ℝ\to \bar{\mathrm{i}}=-\mathrm{i}$$
13		cjre	$$⊢B\in ℝ\to \bar{B}=B$$
14	12 13	oveq12d	$$⊢B\in ℝ\to \bar{\mathrm{i}}\bar{B}=\left(-\mathrm{i}\right)B$$
15		mulneg1	$$⊢\left(\mathrm{i}\in ℂ\wedge B\in ℂ\right)\to \left(-\mathrm{i}\right)B=-\mathrm{i}B$$
16	2 3 15	sylancr	$$⊢B\in ℝ\to \left(-\mathrm{i}\right)B=-\mathrm{i}B$$
17	10 14 16	3eqtrd	$$⊢B\in ℝ\to \overline{\mathrm{i}B}=-\mathrm{i}B$$
18	8 17	oveqan12d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \bar{A}+\overline{\mathrm{i}B}=A+\left(-\mathrm{i}B\right)$$
19		negsub	$$⊢\left(A\in ℂ\wedge \mathrm{i}B\in ℂ\right)\to A+\left(-\mathrm{i}B\right)=A-\mathrm{i}B$$
20	1 5 19	syl2an	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A+\left(-\mathrm{i}B\right)=A-\mathrm{i}B$$
21	7 18 20	3eqtrd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \overline{A+\mathrm{i}B}=A-\mathrm{i}B$$