Description: A square of a real is nonnegative. (Contributed by NM, 18-Oct-1999)
Ref | Expression | ||
---|---|---|---|
Assertion | sqge0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | msqge0 | |
|
2 | recn | |
|
3 | sqval | |
|
4 | 2 3 | syl | |
5 | 1 4 | breqtrrd | |