Description: The square root of a positive real is a real. (Contributed by Mario Carneiro, 6-Sep-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sqrtthi.1 | |- A e. RR |
|
sqrpclii.2 | |- 0 < A |
||
Assertion | sqrtpclii | |- ( sqrt ` A ) e. RR |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sqrtthi.1 | |- A e. RR |
|
2 | sqrpclii.2 | |- 0 < A |
|
3 | 0re | |- 0 e. RR |
|
4 | 3 1 2 | ltleii | |- 0 <_ A |
5 | 1 | sqrtcli | |- ( 0 <_ A -> ( sqrt ` A ) e. RR ) |
6 | 4 5 | ax-mp | |- ( sqrt ` A ) e. RR |