Theorem cjreim2

Description: The conjugate of the representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005) (Proof shortened by Mario Carneiro, 29-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		cjreim	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \overline{A+\mathrm{i}B}=A-\mathrm{i}B$$
2	1	fveq2d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \overline{\stackrel{‾}{A+\mathrm{i}B}}=\overline{A-\mathrm{i}B}$$
3		simpl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A\in ℝ$$
4	3	recnd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A\in ℂ$$
5		ax-icn	$$⊢\mathrm{i}\in ℂ$$
6	5	a1i	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \mathrm{i}\in ℂ$$
7		simpr	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to B\in ℝ$$
8	7	recnd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to B\in ℂ$$
9	6 8	mulcld	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \mathrm{i}B\in ℂ$$
10	4 9	addcld	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A+\mathrm{i}B\in ℂ$$
11		cjcj	$$⊢A+\mathrm{i}B\in ℂ\to \overline{\stackrel{‾}{A+\mathrm{i}B}}=A+\mathrm{i}B$$
12	10 11	syl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \overline{\stackrel{‾}{A+\mathrm{i}B}}=A+\mathrm{i}B$$
13	2 12	eqtr3d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \overline{A-\mathrm{i}B}=A+\mathrm{i}B$$