Metamath Proof Explorer
Description: The square root of a nonnegative real is nonnegative. (Contributed by NM, 26-May-1999) (Revised by Mario Carneiro, 6-Sep-2013)
|
|
Ref |
Expression |
|
Hypothesis |
sqrtthi.1 |
⊢ 𝐴 ∈ ℝ |
|
Assertion |
sqrtge0i |
⊢ ( 0 ≤ 𝐴 → 0 ≤ ( √ ‘ 𝐴 ) ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
sqrtthi.1 |
⊢ 𝐴 ∈ ℝ |
2 |
|
sqrtge0 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 0 ≤ ( √ ‘ 𝐴 ) ) |
3 |
1 2
|
mpan |
⊢ ( 0 ≤ 𝐴 → 0 ≤ ( √ ‘ 𝐴 ) ) |