Description: A number is zero iff its square is zero. (Contributed by NM, 11-Mar-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | sqeq0 | ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 2 ) = 0 ↔ 𝐴 = 0 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2nn | ⊢ 2 ∈ ℕ | |
2 | expeq0 | ⊢ ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℕ ) → ( ( 𝐴 ↑ 2 ) = 0 ↔ 𝐴 = 0 ) ) | |
3 | 1 2 | mpan2 | ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 2 ) = 0 ↔ 𝐴 = 0 ) ) |