Theorem sqrtgt0ii

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	|- A e. RR
	sqrpclii.2	|- 0 < A
Assertion	sqrtgt0ii	|- 0 < ( sqrt ` A )

Proof

Step	Hyp	Ref	Expression
1		sqrtthi.1	|- A e. RR
2		sqrpclii.2	|- 0 < A
3	1	sqrtgt0i	|- ( 0 < A -> 0 < ( sqrt ` A ) )
4	2 3	ax-mp	|- 0 < ( sqrt ` A )