Metamath Proof Explorer

Theorem sqrt00

Description: A square root is zero iff its argument is 0. (Contributed by NM, 27-Jul-1999) (Proof shortened by Mario Carneiro, 29-May-2016)

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

Proof

Step Hyp Ref Expression
1 sqrt0 
 |-  ( sqrt ` 0 ) = 0
2 1 eqeq2i 
 |-  ( ( sqrt ` A ) = ( sqrt ` 0 ) <-> ( sqrt ` A ) = 0 )
3 0re 
 |-  0 e. RR
4 0le0 
 |-  0 <_ 0
5 sqrt11 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( 0 e. RR /\ 0 <_ 0 ) ) -> ( ( sqrt ` A ) = ( sqrt ` 0 ) <-> A = 0 ) )
6 3 4 5 mpanr12 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( ( sqrt ` A ) = ( sqrt ` 0 ) <-> A = 0 ) )
7 2 6 bitr3id 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( ( sqrt ` A ) = 0 <-> A = 0 ) )