eftval - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > eftval		Structured version Visualization version GIF version

Theorem eftval 15714

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.)

**Hypothesis**
Ref	Expression
eftval.1	⊢ 𝐹 = (𝑛 ∈ ℕ₀ ↦ ((𝐴↑𝑛) / (!‘𝑛)))

**Assertion**
Ref	Expression
eftval	⊢ (𝑁 ∈ ℕ₀ → (𝐹‘𝑁) = ((𝐴↑𝑁) / (!‘𝑁)))

Distinct variable groups: 𝐴,𝑛 𝑛,𝑁 Allowed substitution hint: 𝐹(𝑛)

**Proof of Theorem eftval**
Step	Hyp	Ref	Expression
1		oveq2 7263	. . 3 ⊢ (𝑛 = 𝑁 → (𝐴↑𝑛) = (𝐴↑𝑁))
2		fveq2 6756	. . 3 ⊢ (𝑛 = 𝑁 → (!‘𝑛) = (!‘𝑁))
3	1, 2	oveq12d 7273	. 2 ⊢ (𝑛 = 𝑁 → ((𝐴↑𝑛) / (!‘𝑛)) = ((𝐴↑𝑁) / (!‘𝑁)))
4		eftval.1	. 2 ⊢ 𝐹 = (𝑛 ∈ ℕ₀ ↦ ((𝐴↑𝑛) / (!‘𝑛)))
5		ovex 7288	. 2 ⊢ ((𝐴↑𝑁) / (!‘𝑁)) ∈ V
6	3, 4, 5	fvmpt 6857	1 ⊢ (𝑁 ∈ ℕ₀ → (𝐹‘𝑁) = ((𝐴↑𝑁) / (!‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2108 ↦ cmpt 5153 ‘cfv 6418 (class class class)co 7255 / cdiv 11562 ℕ₀cn0 12163 ↑cexp 13710 !cfa 13915

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pr 5347

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ral 3068 df-rex 3069 df-rab 3072 df-v 3424 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-br 5071 df-opab 5133 df-mpt 5154 df-id 5480 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-iota 6376 df-fun 6420 df-fv 6426 df-ov 7258

This theorem is referenced by: efcllem 15715 ef0lem 15716 eff 15719 efval2 15721 efcvg 15722 efcvgfsum 15723 reefcl 15724 efcj 15729 efaddlem 15730 eftlcvg 15743 eftlcl 15744 reeftlcl 15745 eftlub 15746 efsep 15747 effsumlt 15748 efgt1p2 15751 efgt1p 15752 eflegeo 15758 eirrlem 15841 subfaclim 33050

W3C validator