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