Database
REAL AND COMPLEX NUMBERS
Elementary integer functions
Integer powers
sqeq0
Next ⟩
sqdiv
Metamath Proof Explorer
Ascii
Unicode
Theorem
sqeq0
Description:
A number is zero iff its square is zero.
(Contributed by
NM
, 11-Mar-2006)
Ref
Expression
Assertion
sqeq0
⊢
A
∈
ℂ
→
A
2
=
0
↔
A
=
0
Proof
Step
Hyp
Ref
Expression
1
2nn
⊢
2
∈
ℕ
2
expeq0
⊢
A
∈
ℂ
∧
2
∈
ℕ
→
A
2
=
0
↔
A
=
0
3
1
2
mpan2
⊢
A
∈
ℂ
→
A
2
=
0
↔
A
=
0