This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )