Metamath Proof Explorer


Theorem numexp0

Description: Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015)

Ref Expression
Hypothesis numexp.1 A 0
Assertion numexp0 A 0 = 1

Proof

Step Hyp Ref Expression
1 numexp.1 A 0
2 1 nn0cni A
3 exp0 A A 0 = 1
4 2 3 ax-mp A 0 = 1