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 \Re \left(A\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		reval	$$⊢A\in ℂ\to \Re \left(A\right)=\frac{A+\bar{A}}{2}$$
2		cjth	$$⊢A\in ℂ\to \left(A+\bar{A}\in ℝ\wedge \mathrm{i}\left(A-\bar{A}\right)\in ℝ\right)$$
3	2	simpld	$$⊢A\in ℂ\to A+\bar{A}\in ℝ$$
4	3	rehalfcld	$$⊢A\in ℂ\to \frac{A+\bar{A}}{2}\in ℝ$$
5	1 4	eqeltrd	$$⊢A\in ℂ\to \Re \left(A\right)\in ℝ$$