Metamath Proof Explorer


Theorem sqeq0i

Description: A number is zero iff its square is zero. (Contributed by NM, 2-Oct-1999)

Ref Expression
Hypothesis sqval.1 A
Assertion sqeq0i A 2 = 0 A = 0

Proof

Step Hyp Ref Expression
1 sqval.1 A
2 sqeq0 A A 2 = 0 A = 0
3 1 2 ax-mp A 2 = 0 A = 0