Metamath Proof Explorer

Theorem sqne0

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

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

Proof

Step Hyp Ref Expression
1 sqeq0 
 |-  ( A e. CC -> ( ( A ^ 2 ) = 0 <-> A = 0 ) )
2 1 necon3bid 
 |-  ( A e. CC -> ( ( A ^ 2 ) =/= 0 <-> A =/= 0 ) )