Metamath Proof Explorer

Theorem msq0i

Description: A number is zero iff its square is zero (where square is represented using multiplication). (Contributed by NM, 28-Jul-1999)

Ref Expression
Hypothesis msq0i.1 
|- A e. CC
Assertion msq0i 
|- ( ( A x. A ) = 0 <-> A = 0 )

Proof

Step Hyp Ref Expression
1 msq0i.1 
 |-  A e. CC
2 1 1 mul0ori 
 |-  ( ( A x. A ) = 0 <-> ( A = 0 \/ A = 0 ) )
3 oridm 
 |-  ( ( A = 0 \/ A = 0 ) <-> A = 0 )
4 2 3 bitri 
 |-  ( ( A x. A ) = 0 <-> A = 0 )