Metamath Proof Explorer


Theorem sqrtge0

Description: The square root function is nonnegative for nonnegative input. (Contributed by NM, 26-May-1999) (Revised by Mario Carneiro, 9-Jul-2013)

Ref Expression
Assertion sqrtge0 A 0 A 0 A

Proof

Step Hyp Ref Expression
1 resqrtthlem A 0 A A 2 = A 0 A i A +
2 1 simp2d A 0 A 0 A
3 resqrtcl A 0 A A
4 3 rered A 0 A A = A
5 2 4 breqtrd A 0 A 0 A