Metamath Proof Explorer

Theorem 0exp

Description: Value of zero raised to a positive integer power. (Contributed by NM, 19-Aug-2004)

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

Proof

Step Hyp Ref Expression
1 eqid 
 |-  0 = 0
2 0cn 
 |-  0 e. CC
3 expeq0 
 |-  ( ( 0 e. CC /\ N e. NN ) -> ( ( 0 ^ N ) = 0 <-> 0 = 0 ) )
4 2 3 mpan 
 |-  ( N e. NN -> ( ( 0 ^ N ) = 0 <-> 0 = 0 ) )
5 1 4 mpbiri 
 |-  ( N e. NN -> ( 0 ^ N ) = 0 )