| 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 ) ) |