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 0 N = 0

Proof

Step Hyp Ref Expression
1 eqid 0 = 0
2 0cn 0
3 expeq0 0 N 0 N = 0 0 = 0
4 2 3 mpan N 0 N = 0 0 = 0
5 1 4 mpbiri N 0 N = 0