Metamath Proof Explorer

Theorem sqeq0

Description: A complex number is zero iff its square is zero. (Contributed by NM, 11-Mar-2006)

Ref Expression
Assertion sqeq0 
|- ( A e. CC -> ( ( A ^ 2 ) = 0 <-> A = 0 ) )

Proof

Step Hyp Ref Expression
1 2nn 
 |-  2 e. NN
2 expeq0 
 |-  ( ( A e. CC /\ 2 e. NN ) -> ( ( A ^ 2 ) = 0 <-> A = 0 ) )
3 1 2 mpan2 
 |-  ( A e. CC -> ( ( A ^ 2 ) = 0 <-> A = 0 ) )