Metamath Proof Explorer


Theorem efzval

Description: Value of the exponential function for integers. Special case of efval . Equation 30 of Rudin p. 164. (Contributed by Steve Rodriguez, 15-Sep-2006) (Revised by Mario Carneiro, 5-Jun-2014)

Ref Expression
Assertion efzval N e N = e N

Proof

Step Hyp Ref Expression
1 zcn N N
2 1 mulid1d N N 1 = N
3 2 fveq2d N e N 1 = e N
4 ax-1cn 1
5 efexp 1 N e N 1 = e 1 N
6 4 5 mpan N e N 1 = e 1 N
7 3 6 eqtr3d N e N = e 1 N
8 df-e e = e 1
9 8 oveq1i e N = e 1 N
10 7 9 eqtr4di N e N = e N