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	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
Assertion	eftval	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐹 ‘ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eftval.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
2		oveq2	⊢ ( 𝑛 = 𝑁 → ( 𝐴 ↑ 𝑛 ) = ( 𝐴 ↑ 𝑁 ) )
3		fveq2	⊢ ( 𝑛 = 𝑁 → ( ! ‘ 𝑛 ) = ( ! ‘ 𝑁 ) )
4	2 3	oveq12d	⊢ ( 𝑛 = 𝑁 → ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) = ( ( 𝐴 ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) )
5		ovex	⊢ ( ( 𝐴 ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) ∈ V
6	4 1 5	fvmpt	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐹 ‘ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) / ( ! ‘ 𝑁 ) ) )