This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in ℝ \land 0 \leq A) \to 0 \leq \sqrt{A}$

Proof

Step	Hyp	Ref	Expression
1		resqrtthlem	$⊢ (A \in ℝ \land 0 \leq A) \to ({\sqrt{A}}^{2} = A \land 0 \leq ℜ (\sqrt{A}) \land i \sqrt{A} \notin ℝ^{+})$
2	1	simp2d	$⊢ (A \in ℝ \land 0 \leq A) \to 0 \leq ℜ (\sqrt{A})$
3		resqrtcl	$⊢ (A \in ℝ \land 0 \leq A) \to \sqrt{A} \in ℝ$
4	3	rered	$⊢ (A \in ℝ \land 0 \leq A) \to ℜ (\sqrt{A}) = \sqrt{A}$
5	2 4	breqtrd	$⊢ (A \in ℝ \land 0 \leq A) \to 0 \leq \sqrt{A}$