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	$$⊢A\in ℂ\to \Im \left(A\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		imre	$$⊢A\in ℂ\to \Im \left(A\right)=\Re \left(\left(-\mathrm{i}\right)A\right)$$
2		negicn	$$⊢-\mathrm{i}\in ℂ$$
3		mulcl	$$⊢\left(-\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \left(-\mathrm{i}\right)A\in ℂ$$
4	2 3	mpan	$$⊢A\in ℂ\to \left(-\mathrm{i}\right)A\in ℂ$$
5		recl	$$⊢\left(-\mathrm{i}\right)A\in ℂ\to \Re \left(\left(-\mathrm{i}\right)A\right)\in ℝ$$
6	4 5	syl	$$⊢A\in ℂ\to \Re \left(\left(-\mathrm{i}\right)A\right)\in ℝ$$
7	1 6	eqeltrd	$$⊢A\in ℂ\to \Im \left(A\right)\in ℝ$$