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
|- ( ph -> A e. CC )
Assertion msq0d
|- ( ph -> ( ( A x. A ) = 0 <-> A = 0 ) )

Proof

Step Hyp Ref Expression
1 msq0d.1
 |-  ( ph -> A e. CC )
2 mul0or
 |-  ( ( A e. CC /\ A e. CC ) -> ( ( A x. A ) = 0 <-> ( A = 0 \/ A = 0 ) ) )
3 1 1 2 syl2anc
 |-  ( ph -> ( ( A x. A ) = 0 <-> ( A = 0 \/ A = 0 ) ) )
4 oridm
 |-  ( ( A = 0 \/ A = 0 ) <-> A = 0 )
5 3 4 bitrdi
 |-  ( ph -> ( ( A x. A ) = 0 <-> A = 0 ) )