Theorem sqrtgt0

Description: The square root function is positive for positive input. (Contributed by Mario Carneiro, 10-Jul-2013) (Revised by Mario Carneiro, 6-Sep-2013)

	Ref	Expression
Assertion	sqrtgt0	|- ( ( A e. RR /\ 0 < A ) -> 0 < ( sqrt ` A ) )

Proof

Step	Hyp	Ref	Expression
1		0re	|- 0 e. RR
2		ltle	|- ( ( 0 e. RR /\ A e. RR ) -> ( 0 < A -> 0 <_ A ) )
3	1 2	mpan	|- ( A e. RR -> ( 0 < A -> 0 <_ A ) )
4	3	imp	|- ( ( A e. RR /\ 0 < A ) -> 0 <_ A )
5		resqrtcl	|- ( ( A e. RR /\ 0 <_ A ) -> ( sqrt ` A ) e. RR )
6	4 5	syldan	|- ( ( A e. RR /\ 0 < A ) -> ( sqrt ` A ) e. RR )
7		sqrtge0	|- ( ( A e. RR /\ 0 <_ A ) -> 0 <_ ( sqrt ` A ) )
8	4 7	syldan	|- ( ( A e. RR /\ 0 < A ) -> 0 <_ ( sqrt ` A ) )
9		gt0ne0	|- ( ( A e. RR /\ 0 < A ) -> A =/= 0 )
10		sq0i	|- ( ( sqrt ` A ) = 0 -> ( ( sqrt ` A ) ^ 2 ) = 0 )
11		resqrtth	|- ( ( A e. RR /\ 0 <_ A ) -> ( ( sqrt ` A ) ^ 2 ) = A )
12	4 11	syldan	|- ( ( A e. RR /\ 0 < A ) -> ( ( sqrt ` A ) ^ 2 ) = A )
13	12	eqeq1d	|- ( ( A e. RR /\ 0 < A ) -> ( ( ( sqrt ` A ) ^ 2 ) = 0 <-> A = 0 ) )
14	10 13	imbitrid	|- ( ( A e. RR /\ 0 < A ) -> ( ( sqrt ` A ) = 0 -> A = 0 ) )
15	14	necon3d	|- ( ( A e. RR /\ 0 < A ) -> ( A =/= 0 -> ( sqrt ` A ) =/= 0 ) )
16	9 15	mpd	|- ( ( A e. RR /\ 0 < A ) -> ( sqrt ` A ) =/= 0 )
17	6 8 16	ne0gt0d	|- ( ( A e. RR /\ 0 < A ) -> 0 < ( sqrt ` A ) )