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