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 ( 𝐴 ∈ ℂ → ( ( √ ‘ 𝐴 ) = 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 syl5ib ( 𝐴 ∈ ℂ → ( ( √ ‘ 𝐴 ) = 0 → 𝐴 = 0 ) )
7 fveq2 ( 𝐴 = 0 → ( √ ‘ 𝐴 ) = ( √ ‘ 0 ) )
8 sqrt0 ( √ ‘ 0 ) = 0
9 7 8 eqtrdi ( 𝐴 = 0 → ( √ ‘ 𝐴 ) = 0 )
10 6 9 impbid1 ( 𝐴 ∈ ℂ → ( ( √ ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) )