Metamath Proof Explorer

Theorem numexp0

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

Ref Expression
Hypothesis numexp.1 
|- A e. NN0
Assertion numexp0 
|- ( A ^ 0 ) = 1

Proof

Step Hyp Ref Expression
1 numexp.1 
 |-  A e. NN0
2 1 nn0cni 
 |-  A e. CC
3 exp0 
 |-  ( A e. CC -> ( A ^ 0 ) = 1 )
4 2 3 ax-mp 
 |-  ( A ^ 0 ) = 1