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 A = 0 A = 0

Proof

Step Hyp Ref Expression
1 oveq1 A = 0 A 2 = 0 2
2 sqrtth A A 2 = A
3 sq0 0 2 = 0
4 3 a1i A 0 2 = 0
5 2 4 eqeq12d A A 2 = 0 2 A = 0
6 1 5 syl5ib A A = 0 A = 0
7 fveq2 A = 0 A = 0
8 sqrt0 0 = 0
9 7 8 eqtrdi A = 0 A = 0
10 6 9 impbid1 A A = 0 A = 0