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\in \mathbb{Z}\to {\mathrm{e}}^N={\mathrm{e}}^N$$

Proof

Step	Hyp	Ref	Expression
1		zcn	$$⊢N\in \mathbb{Z}\to N\in ℂ$$
2	1	mulid1d	$$⊢N\in \mathbb{Z}\to \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 1=N$$
3	2	fveq2d	$$⊢N\in \mathbb{Z}\to {\mathrm{e}}^{\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 1}={\mathrm{e}}^N$$
4		ax-1cn	$$⊢1\in ℂ$$
5		efexp	$$⊢\left(1\in ℂ\wedge N\in \mathbb{Z}\right)\to {\mathrm{e}}^{\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 1}={{\mathrm{e}}^1}^N$$
6	4 5	mpan	$$⊢N\in \mathbb{Z}\to {\mathrm{e}}^{\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 1}={{\mathrm{e}}^1}^N$$
7	3 6	eqtr3d	$$⊢N\in \mathbb{Z}\to {\mathrm{e}}^N={{\mathrm{e}}^1}^N$$
8		df-e	$$⊢\mathrm{e}={\mathrm{e}}^1$$
9	8	oveq1i	$$⊢{\mathrm{e}}^N={{\mathrm{e}}^1}^N$$
10	7 9	eqtr4di	$$⊢N\in \mathbb{Z}\to {\mathrm{e}}^N={\mathrm{e}}^N$$