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 e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
Assertion	eftval	|- ( N e. NN0 -> ( F ` N ) = ( ( A ^ N ) / ( ! ` N ) ) )

Proof

Step	Hyp	Ref	Expression
1		eftval.1	|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
2		oveq2	|- ( n = N -> ( A ^ n ) = ( A ^ N ) )
3		fveq2	|- ( n = N -> ( ! ` n ) = ( ! ` N ) )
4	2 3	oveq12d	|- ( n = N -> ( ( A ^ n ) / ( ! ` n ) ) = ( ( A ^ N ) / ( ! ` N ) ) )
5		ovex	|- ( ( A ^ N ) / ( ! ` N ) ) e. _V
6	4 1 5	fvmpt	|- ( N e. NN0 -> ( F ` N ) = ( ( A ^ N ) / ( ! ` N ) ) )