Theorem eftval

Description: The value of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 21-Aug-2007) (Revised by Mario Carneiro, 28-Apr-2014)

	Ref	Expression
Hypothesis	eftval.1	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)$$
Assertion	eftval	$$⊢N\in {\mathbb{N}}_0\to F\left(N\right)=\frac{A^N}{N!}$$

Proof

Step	Hyp	Ref	Expression
1		eftval.1	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)$$
2		oveq2	$$⊢n=N\to A^n=A^N$$
3		fveq2	$$⊢n=N\to n!=N!$$
4	2 3	oveq12d	$$⊢n=N\to \frac{A^n}{n!}=\frac{A^N}{N!}$$
5		ovex	$$⊢\frac{A^N}{N!}\in \mathrm{V}$$
6	4 1 5	fvmpt	$$⊢N\in {\mathbb{N}}_0\to F\left(N\right)=\frac{A^N}{N!}$$