Theorem recoscl

Description: The cosine of a real number is real. (Contributed by NM, 30-Apr-2005)

	Ref	Expression
Assertion	recoscl	⊢ ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		recosval	⊢ ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) = ( ℜ ‘ ( exp ‘ ( i · 𝐴 ) ) ) )
2		ax-icn	⊢ i ∈ ℂ
3		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
4		mulcl	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
5	2 3 4	sylancr	⊢ ( 𝐴 ∈ ℝ → ( i · 𝐴 ) ∈ ℂ )
6		efcl	⊢ ( ( i · 𝐴 ) ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ )
7	5 6	syl	⊢ ( 𝐴 ∈ ℝ → ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ )
8	7	recld	⊢ ( 𝐴 ∈ ℝ → ( ℜ ‘ ( exp ‘ ( i · 𝐴 ) ) ) ∈ ℝ )
9	1 8	eqeltrd	⊢ ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) ∈ ℝ )