Metamath Proof Explorer


Theorem msqge0i

Description: A square is nonnegative. (Contributed by NM, 14-May-1999) (Proof shortened by Andrew Salmon, 19-Nov-2011)

Ref Expression
Hypothesis lt2.1
|- A e. RR
Assertion msqge0i
|- 0 <_ ( A x. A )

Proof

Step Hyp Ref Expression
1 lt2.1
 |-  A e. RR
2 msqge0
 |-  ( A e. RR -> 0 <_ ( A x. A ) )
3 1 2 ax-mp
 |-  0 <_ ( A x. A )