Metamath Proof Explorer


Theorem sqrtpclii

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

Proof

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