Metamath Proof Explorer

Theorem 0expd

Description: Value of zero raised to a positive integer power. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypothesis 0exp.1 
|- ( ph -> N e. NN )
Assertion 0expd 
|- ( ph -> ( 0 ^ N ) = 0 )

Proof

Step Hyp Ref Expression
1 0exp.1 
 |-  ( ph -> N e. NN )
2 0exp 
 |-  ( N e. NN -> ( 0 ^ N ) = 0 )
3 1 2 syl 
 |-  ( ph -> ( 0 ^ N ) = 0 )