Metamath Proof Explorer

Theorem numexp1

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

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

Proof

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