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	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		reval	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) = ( ( 𝐴 + ( ∗ ‘ 𝐴 ) ) / 2 ) )
2		cjth	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 + ( ∗ ‘ 𝐴 ) ) ∈ ℝ ∧ ( i · ( 𝐴 − ( ∗ ‘ 𝐴 ) ) ) ∈ ℝ ) )
3	2	simpld	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + ( ∗ ‘ 𝐴 ) ) ∈ ℝ )
4	3	rehalfcld	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 + ( ∗ ‘ 𝐴 ) ) / 2 ) ∈ ℝ )
5	1 4	eqeltrd	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℝ )