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