Theorem absrele

Description: The absolute value of a complex number is greater than or equal to the absolute value of its real part. (Contributed by NM, 1-Apr-2005)

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

Proof

Step	Hyp	Ref	Expression
1		imcl	|- ( A e. CC -> ( Im ` A ) e. RR )
2	1	sqge0d	|- ( A e. CC -> 0 <_ ( ( Im ` A ) ^ 2 ) )
3		recl	|- ( A e. CC -> ( Re ` A ) e. RR )
4	3	resqcld	|- ( A e. CC -> ( ( Re ` A ) ^ 2 ) e. RR )
5	1	resqcld	|- ( A e. CC -> ( ( Im ` A ) ^ 2 ) e. RR )
6	4 5	addge01d	|- ( A e. CC -> ( 0 <_ ( ( Im ` A ) ^ 2 ) <-> ( ( Re ` A ) ^ 2 ) <_ ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) ) )
7	2 6	mpbid	|- ( A e. CC -> ( ( Re ` A ) ^ 2 ) <_ ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) )
8	3	sqge0d	|- ( A e. CC -> 0 <_ ( ( Re ` A ) ^ 2 ) )
9	4 5	readdcld	|- ( A e. CC -> ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) e. RR )
10	4 5 8 2	addge0d	|- ( A e. CC -> 0 <_ ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) )
11		sqrtle	|- ( ( ( ( ( Re ` A ) ^ 2 ) e. RR /\ 0 <_ ( ( Re ` A ) ^ 2 ) ) /\ ( ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) e. RR /\ 0 <_ ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) ) ) -> ( ( ( Re ` A ) ^ 2 ) <_ ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) <-> ( sqrt ` ( ( Re ` A ) ^ 2 ) ) <_ ( sqrt ` ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) ) ) )
12	4 8 9 10 11	syl22anc	|- ( A e. CC -> ( ( ( Re ` A ) ^ 2 ) <_ ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) <-> ( sqrt ` ( ( Re ` A ) ^ 2 ) ) <_ ( sqrt ` ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) ) ) )
13	7 12	mpbid	|- ( A e. CC -> ( sqrt ` ( ( Re ` A ) ^ 2 ) ) <_ ( sqrt ` ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) ) )
14		absre	|- ( ( Re ` A ) e. RR -> ( abs ` ( Re ` A ) ) = ( sqrt ` ( ( Re ` A ) ^ 2 ) ) )
15	3 14	syl	|- ( A e. CC -> ( abs ` ( Re ` A ) ) = ( sqrt ` ( ( Re ` A ) ^ 2 ) ) )
16		absval2	|- ( A e. CC -> ( abs ` A ) = ( sqrt ` ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) ) )
17	13 15 16	3brtr4d	|- ( A e. CC -> ( abs ` ( Re ` A ) ) <_ ( abs ` A ) )