Metamath Proof Explorer


Theorem sqge0

Description: A 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 ) )