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. ZZ -> ( exp ` N ) = ( _e ^ N ) )

Proof

Step Hyp Ref Expression
1 zcn
 |-  ( N e. ZZ -> N e. CC )
2 1 mulid1d
 |-  ( N e. ZZ -> ( N x. 1 ) = N )
3 2 fveq2d
 |-  ( N e. ZZ -> ( exp ` ( N x. 1 ) ) = ( exp ` N ) )
4 ax-1cn
 |-  1 e. CC
5 efexp
 |-  ( ( 1 e. CC /\ N e. ZZ ) -> ( exp ` ( N x. 1 ) ) = ( ( exp ` 1 ) ^ N ) )
6 4 5 mpan
 |-  ( N e. ZZ -> ( exp ` ( N x. 1 ) ) = ( ( exp ` 1 ) ^ N ) )
7 3 6 eqtr3d
 |-  ( N e. ZZ -> ( exp ` N ) = ( ( exp ` 1 ) ^ N ) )
8 df-e
 |-  _e = ( exp ` 1 )
9 8 oveq1i
 |-  ( _e ^ N ) = ( ( exp ` 1 ) ^ N )
10 7 9 eqtr4di
 |-  ( N e. ZZ -> ( exp ` N ) = ( _e ^ N ) )