Metamath Proof Explorer

Theorem sqrtsq2

Description: Relationship between square root and squares. (Contributed by NM, 31-Jul-1999) (Revised by Mario Carneiro, 29-May-2016)

Ref Expression
Assertion sqrtsq2 
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( sqrt ` A ) = B <-> A = ( B ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 resqrtcl 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( sqrt ` A ) e. RR )
2 sqrtge0 
 |-  ( ( A e. RR /\ 0 <_ A ) -> 0 <_ ( sqrt ` A ) )
3 1 2 jca 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( ( sqrt ` A ) e. RR /\ 0 <_ ( sqrt ` A ) ) )
4 sq11 
 |-  ( ( ( ( sqrt ` A ) e. RR /\ 0 <_ ( sqrt ` A ) ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( ( sqrt ` A ) ^ 2 ) = ( B ^ 2 ) <-> ( sqrt ` A ) = B ) )
5 3 4 sylan 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( ( sqrt ` A ) ^ 2 ) = ( B ^ 2 ) <-> ( sqrt ` A ) = B ) )
6 resqrtth 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( ( sqrt ` A ) ^ 2 ) = A )
7 6 adantr 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( sqrt ` A ) ^ 2 ) = A )
8 7 eqeq1d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( ( sqrt ` A ) ^ 2 ) = ( B ^ 2 ) <-> A = ( B ^ 2 ) ) )
9 5 8 bitr3d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( sqrt ` A ) = B <-> A = ( B ^ 2 ) ) )