Metamath Proof Explorer

Theorem expne0

Description: A positive integer power is nonzero if and only if its base is nonzero. (Contributed by NM, 6-May-2005)

Ref Expression
Assertion expne0 
|- ( ( A e. CC /\ N e. NN ) -> ( ( A ^ N ) =/= 0 <-> A =/= 0 ) )

Proof

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