Metamath Proof Explorer

Theorem sqge0

Description: The square of a real is nonnegative. (Contributed by NM, 18-Oct-1999)

Ref Expression
Assertion sqge0 
|- ( A e. RR -> 0 <_ ( A ^ 2 ) )

Proof

Step Hyp Ref Expression
1 msqge0 
 |-  ( A e. RR -> 0 <_ ( A x. A ) )
2 recn 
 |-  ( A e. RR -> A e. CC )
3 sqval 
 |-  ( A e. CC -> ( A ^ 2 ) = ( A x. A ) )
4 2 3 syl 
 |-  ( A e. RR -> ( A ^ 2 ) = ( A x. A ) )
5 1 4 breqtrrd 
 |-  ( A e. RR -> 0 <_ ( A ^ 2 ) )