Theorem absimle

Description: The absolute value of a complex number is greater than or equal to the absolute value of its imaginary part. (Contributed by NM, 17-Mar-2005) (Proof shortened by Mario Carneiro, 29-May-2016)

	Ref	Expression
Assertion	absimle	|- ( A e. CC -> ( abs ` ( Im ` A ) ) <_ ( abs ` A ) )

Proof

Step	Hyp	Ref	Expression
1		negicn	|- -u _i e. CC
2	1	a1i	|- ( A e. CC -> -u _i e. CC )
3		id	|- ( A e. CC -> A e. CC )
4	2 3	mulcld	|- ( A e. CC -> ( -u _i x. A ) e. CC )
5		absrele	|- ( ( -u _i x. A ) e. CC -> ( abs ` ( Re ` ( -u _i x. A ) ) ) <_ ( abs ` ( -u _i x. A ) ) )
6	4 5	syl	|- ( A e. CC -> ( abs ` ( Re ` ( -u _i x. A ) ) ) <_ ( abs ` ( -u _i x. A ) ) )
7		imre	|- ( A e. CC -> ( Im ` A ) = ( Re ` ( -u _i x. A ) ) )
8	7	fveq2d	|- ( A e. CC -> ( abs ` ( Im ` A ) ) = ( abs ` ( Re ` ( -u _i x. A ) ) ) )
9		absmul	|- ( ( -u _i e. CC /\ A e. CC ) -> ( abs ` ( -u _i x. A ) ) = ( ( abs ` -u _i ) x. ( abs ` A ) ) )
10	1 9	mpan	|- ( A e. CC -> ( abs ` ( -u _i x. A ) ) = ( ( abs ` -u _i ) x. ( abs ` A ) ) )
11		ax-icn	|- _i e. CC
12		absneg	|- ( _i e. CC -> ( abs ` -u _i ) = ( abs ` _i ) )
13	11 12	ax-mp	|- ( abs ` -u _i ) = ( abs ` _i )
14		absi	|- ( abs ` _i ) = 1
15	13 14	eqtri	|- ( abs ` -u _i ) = 1
16	15	oveq1i	|- ( ( abs ` -u _i ) x. ( abs ` A ) ) = ( 1 x. ( abs ` A ) )
17		abscl	|- ( A e. CC -> ( abs ` A ) e. RR )
18	17	recnd	|- ( A e. CC -> ( abs ` A ) e. CC )
19	18	mulid2d	|- ( A e. CC -> ( 1 x. ( abs ` A ) ) = ( abs ` A ) )
20	16 19	syl5eq	|- ( A e. CC -> ( ( abs ` -u _i ) x. ( abs ` A ) ) = ( abs ` A ) )
21	10 20	eqtr2d	|- ( A e. CC -> ( abs ` A ) = ( abs ` ( -u _i x. A ) ) )
22	6 8 21	3brtr4d	|- ( A e. CC -> ( abs ` ( Im ` A ) ) <_ ( abs ` A ) )