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	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 0 ≤ ( √ ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		resqrtthlem	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ ( √ ‘ 𝐴 ) ) ∧ ( i · ( √ ‘ 𝐴 ) ) ∉ ℝ+ ) )
2	1	simp2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 0 ≤ ( ℜ ‘ ( √ ‘ 𝐴 ) ) )
3		resqrtcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ 𝐴 ) ∈ ℝ )
4	3	rered	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ℜ ‘ ( √ ‘ 𝐴 ) ) = ( √ ‘ 𝐴 ) )
5	2 4	breqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 0 ≤ ( √ ‘ 𝐴 ) )