Metamath Proof Explorer


Theorem msq0d

Description: A number is zero iff its square is zero (where square is represented using multiplication). (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypothesis msq0d.1 φ A
Assertion msq0d φ A A = 0 A = 0

Proof

Step Hyp Ref Expression
1 msq0d.1 φ A
2 mul0or A A A A = 0 A = 0 A = 0
3 1 1 2 syl2anc φ A A = 0 A = 0 A = 0
4 oridm A = 0 A = 0 A = 0
5 3 4 bitrdi φ A A = 0 A = 0