Theorem imcl

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

	Ref	Expression
Assertion	imcl	⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		imre	⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) = ( ℜ ‘ ( - i · 𝐴 ) ) )
2		negicn	⊢ - i ∈ ℂ
3		mulcl	⊢ ( ( - i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · 𝐴 ) ∈ ℂ )
4	2 3	mpan	⊢ ( 𝐴 ∈ ℂ → ( - i · 𝐴 ) ∈ ℂ )
5		recl	⊢ ( ( - i · 𝐴 ) ∈ ℂ → ( ℜ ‘ ( - i · 𝐴 ) ) ∈ ℝ )
6	4 5	syl	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ ( - i · 𝐴 ) ) ∈ ℝ )
7	1 6	eqeltrd	⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℝ )