This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!})$
	Assertion	eftval	$⊢ N \in ℕ_{0} \to F (N) = \frac{A^{N}}{N!}$

Proof

Step	Hyp	Ref	Expression
1		eftval.1	$⊢ F = (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!})$
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 V$
6	4 1 5	fvmpt	$⊢ N \in ℕ_{0} \to F (N) = \frac{A^{N}}{N!}$