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