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 16039

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 7371	. . 3 ⊢ (𝑛 = 𝑁 → (𝐴↑𝑛) = (𝐴↑𝑁))
2		fveq2 6834	. . 3 ⊢ (𝑛 = 𝑁 → (!‘𝑛) = (!‘𝑁))
3	1, 2	oveq12d 7381	. 2 ⊢ (𝑛 = 𝑁 → ((𝐴↑𝑛) / (!‘𝑛)) = ((𝐴↑𝑁) / (!‘𝑁)))
4		eftval.1	. 2 ⊢ 𝐹 = (𝑛 ∈ ℕ₀ ↦ ((𝐴↑𝑛) / (!‘𝑛)))
5		ovex 7396	. 2 ⊢ ((𝐴↑𝑁) / (!‘𝑁)) ∈ V
6	3, 4, 5	fvmpt 6942	1 ⊢ (𝑁 ∈ ℕ₀ → (𝐹‘𝑁) = ((𝐴↑𝑁) / (!‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1547 ∈ wcel 2119 ↦ cmpt 5160 ‘cfv 6492 (class class class)co 7363 / cdiv 11805 ℕ₀cn0 12435 ↑cexp 14021 !cfa 14233

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2712 ax-sep 5225 ax-nul 5235 ax-pr 5369

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2719 df-cleq 2732 df-clel 2815 df-nfc 2889 df-ne 2936 df-ral 3055 df-rex 3065 df-rab 3393 df-v 3434 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4269 df-if 4462 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4846 df-br 5080 df-opab 5142 df-mpt 5161 df-id 5520 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-iota 6448 df-fun 6494 df-fv 6500 df-ov 7366

This theorem is referenced by: efcllem 16040 ef0lem 16041 eff 16044 efval2 16047 efcvg 16048 efcvgfsum 16049 reefcl 16050 efcj 16055 efaddlem 16056 eftlcvg 16071 eftlcl 16072 reeftlcl 16073 eftlub 16074 efsep 16075 effsumlt 16076 efgt1p2 16079 efgt1p 16080 eflegeo 16086 eirrlem 16169 subfaclim 35423

W3C validator