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	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to 0\le \sqrt{A}$$

Proof

Step	Hyp	Ref	Expression
1		resqrtthlem	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to \left({\sqrt{A}}^2=A\wedge 0\le \Re \left(\sqrt{A}\right)\wedge \mathrm{i}\sqrt{A}\notin {ℝ}^{+}\right)$$
2	1	simp2d	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to 0\le \Re \left(\sqrt{A}\right)$$
3		resqrtcl	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to \sqrt{A}\in ℝ$$
4	3	rered	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to \Re \left(\sqrt{A}\right)=\sqrt{A}$$
5	2 4	breqtrd	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to 0\le \sqrt{A}$$