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 0 A n n !
Assertion eftval N 0 F N = A N N !

Proof

Step Hyp Ref Expression
1 eftval.1 F = n 0 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 ! V
6 4 1 5 fvmpt N 0 F N = A N N !