Metamath Proof Explorer

Theorem addcj

Description: A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of Gleason p. 133. (Contributed by NM, 21-Jan-2007) (Revised by Mario Carneiro, 14-Jul-2014)

		Ref	Expression
	Assertion	addcj	$⊢ A \in ℂ \to A + \overline{A} = 2 ℜ (A)$

Proof

Step	Hyp	Ref	Expression
1		reval	$⊢ A \in ℂ \to ℜ (A) = \frac{A + \overline{A}}{2}$
2	1	oveq2d	$⊢ A \in ℂ \to 2 ℜ (A) = 2 (\frac{A + \overline{A}}{2})$
3		cjcl	$⊢ A \in ℂ \to \overline{A} \in ℂ$
4		addcl	$⊢ (A \in ℂ \land \overline{A} \in ℂ) \to A + \overline{A} \in ℂ$
5	3 4	mpdan	$⊢ A \in ℂ \to A + \overline{A} \in ℂ$
6		2cn	$⊢ 2 \in ℂ$
7		2ne0	$⊢ 2 \neq 0$
8		divcan2	$⊢ (A + \overline{A} \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to 2 (\frac{A + \overline{A}}{2}) = A + \overline{A}$
9	6 7 8	mp3an23	$⊢ A + \overline{A} \in ℂ \to 2 (\frac{A + \overline{A}}{2}) = A + \overline{A}$
10	5 9	syl	$⊢ A \in ℂ \to 2 (\frac{A + \overline{A}}{2}) = A + \overline{A}$
11	2 10	eqtr2d	$⊢ A \in ℂ \to A + \overline{A} = 2 ℜ (A)$