Description: The square root of a positive real is positive. (Contributed by NM, 26-May-1999) (Revised by Mario Carneiro, 6-Sep-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sqrtthi.1 | |
|
sqrpclii.2 | |
||
Assertion | sqrtgt0ii | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sqrtthi.1 | |
|
2 | sqrpclii.2 | |
|
3 | 1 | sqrtgt0i | |
4 | 2 3 | ax-mp | |