Metamath Proof Explorer

Theorem cjmulge0

Description: A complex number times its conjugate is nonnegative. (Contributed by NM, 26-Mar-2005) (Revised by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion cjmulge0 
|- ( A e. CC -> 0 <_ ( A x. ( * ` A ) ) )

Proof

Step Hyp Ref Expression
1 recl 
 |-  ( A e. CC -> ( Re ` A ) e. RR )
2 1 resqcld 
 |-  ( A e. CC -> ( ( Re ` A ) ^ 2 ) e. RR )
3 imcl 
 |-  ( A e. CC -> ( Im ` A ) e. RR )
4 3 resqcld 
 |-  ( A e. CC -> ( ( Im ` A ) ^ 2 ) e. RR )
5 1 sqge0d 
 |-  ( A e. CC -> 0 <_ ( ( Re ` A ) ^ 2 ) )
6 3 sqge0d 
 |-  ( A e. CC -> 0 <_ ( ( Im ` A ) ^ 2 ) )
7 2 4 5 6 addge0d 
 |-  ( A e. CC -> 0 <_ ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) )
8 cjmulval 
 |-  ( A e. CC -> ( A x. ( * ` A ) ) = ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) )
9 7 8 breqtrrd 
 |-  ( A e. CC -> 0 <_ ( A x. ( * ` A ) ) )