Metamath Proof Explorer


Theorem sqge0i

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

Ref Expression
Hypothesis resqcl.1 A
Assertion sqge0i 0A2

Proof

Step Hyp Ref Expression
1 resqcl.1 A
2 1 msqge0i 0AA
3 1 recni A
4 3 sqvali A2=AA
5 2 4 breqtrri 0A2