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

Metamath Proof Explorer

Theorem recl

Description: The real part of a complex number is real. (Contributed by NM, 9-May-1999) (Revised by Mario Carneiro, 6-Nov-2013)

		Ref	Expression
	Assertion	recl	$⊢ A \in ℂ \to ℜ (A) \in ℝ$

Step	Hyp	Ref	Expression
1		reval	$⊢ A \in ℂ \to ℜ (A) = \frac{A + \overline{A}}{2}$
2		cjth	$⊢ A \in ℂ \to (A + \overline{A} \in ℝ \land i (A - \overline{A}) \in ℝ)$
3	2	simpld	$⊢ A \in ℂ \to A + \overline{A} \in ℝ$
4	3	rehalfcld	$⊢ A \in ℂ \to \frac{A + \overline{A}}{2} \in ℝ$
5	1 4	eqeltrd	$⊢ A \in ℂ \to ℜ (A) \in ℝ$