Metamath Proof Explorer


Theorem sqge0

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

Ref Expression
Assertion sqge0 A0A2

Proof

Step Hyp Ref Expression
1 msqge0 A0AA
2 recn AA
3 sqval AA2=AA
4 2 3 syl AA2=AA
5 1 4 breqtrrd A0A2