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

Metamath Proof Explorer

Theorem cnsqrt00

Description: A square root of a complex number is zero iff its argument is 0. Version of sqrt00 for complex numbers. (Contributed by AV, 26-Jan-2023)

Ref Expression
Assertion cnsqrt00 
|- ( A e. CC -> ( ( sqrt ` A ) = 0 <-> A = 0 ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( ( sqrt ` A ) = 0 -> ( ( sqrt ` A ) ^ 2 ) = ( 0 ^ 2 ) )
2 sqrtth 
 |-  ( A e. CC -> ( ( sqrt ` A ) ^ 2 ) = A )
3 sq0 
 |-  ( 0 ^ 2 ) = 0
4 3 a1i 
 |-  ( A e. CC -> ( 0 ^ 2 ) = 0 )
5 2 4 eqeq12d 
 |-  ( A e. CC -> ( ( ( sqrt ` A ) ^ 2 ) = ( 0 ^ 2 ) <-> A = 0 ) )
6 1 5 imbitrid 
 |-  ( A e. CC -> ( ( sqrt ` A ) = 0 -> A = 0 ) )
7 fveq2 
 |-  ( A = 0 -> ( sqrt ` A ) = ( sqrt ` 0 ) )
8 sqrt0 
 |-  ( sqrt ` 0 ) = 0
9 7 8 eqtrdi 
 |-  ( A = 0 -> ( sqrt ` A ) = 0 )
10 6 9 impbid1 
 |-  ( A e. CC -> ( ( sqrt ` A ) = 0 <-> A = 0 ) )