This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (A \in ℝ \land B \in ℝ) \to \overline{A - i B} = A + i B$

Proof

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