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 e. CC -> ( Im ` A ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		imre	|- ( A e. CC -> ( Im ` A ) = ( Re ` ( -u _i x. A ) ) )
2		negicn	|- -u _i e. CC
3		mulcl	|- ( ( -u _i e. CC /\ A e. CC ) -> ( -u _i x. A ) e. CC )
4	2 3	mpan	|- ( A e. CC -> ( -u _i x. A ) e. CC )
5		recl	|- ( ( -u _i x. A ) e. CC -> ( Re ` ( -u _i x. A ) ) e. RR )
6	4 5	syl	|- ( A e. CC -> ( Re ` ( -u _i x. A ) ) e. RR )
7	1 6	eqeltrd	|- ( A e. CC -> ( Im ` A ) e. RR )