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	⊢ ( 𝐴 ∈ ℂ → ( ( √ ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( ( √ ‘ 𝐴 ) = 0 → ( ( √ ‘ 𝐴 ) ↑ 2 ) = ( 0 ↑ 2 ) )
2		sqrtth	⊢ ( 𝐴 ∈ ℂ → ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 )
3		sq0	⊢ ( 0 ↑ 2 ) = 0
4	3	a1i	⊢ ( 𝐴 ∈ ℂ → ( 0 ↑ 2 ) = 0 )
5	2 4	eqeq12d	⊢ ( 𝐴 ∈ ℂ → ( ( ( √ ‘ 𝐴 ) ↑ 2 ) = ( 0 ↑ 2 ) ↔ 𝐴 = 0 ) )
6	1 5	imbitrid	⊢ ( 𝐴 ∈ ℂ → ( ( √ ‘ 𝐴 ) = 0 → 𝐴 = 0 ) )
7		fveq2	⊢ ( 𝐴 = 0 → ( √ ‘ 𝐴 ) = ( √ ‘ 0 ) )
8		sqrt0	⊢ ( √ ‘ 0 ) = 0
9	7 8	eqtrdi	⊢ ( 𝐴 = 0 → ( √ ‘ 𝐴 ) = 0 )
10	6 9	impbid1	⊢ ( 𝐴 ∈ ℂ → ( ( √ ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) )