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 ) )