Metamath Proof Explorer


Theorem expeq0d

Description: Positive integer exponentiation is 0 iff its base is 0. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses expcld.1
|- ( ph -> A e. CC )
expeq0d.2
|- ( ph -> N e. NN )
expeq0d.3
|- ( ph -> ( A ^ N ) = 0 )
Assertion expeq0d
|- ( ph -> A = 0 )

Proof

Step Hyp Ref Expression
1 expcld.1
 |-  ( ph -> A e. CC )
2 expeq0d.2
 |-  ( ph -> N e. NN )
3 expeq0d.3
 |-  ( ph -> ( A ^ N ) = 0 )
4 expeq0
 |-  ( ( A e. CC /\ N e. NN ) -> ( ( A ^ N ) = 0 <-> A = 0 ) )
5 1 2 4 syl2anc
 |-  ( ph -> ( ( A ^ N ) = 0 <-> A = 0 ) )
6 3 5 mpbid
 |-  ( ph -> A = 0 )