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 16001

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2109 ↦ cmpt 5176 ‘cfv 6486 (class class class)co 7353 / cdiv 11795 ℕ₀cn0 12402 ↑cexp 13986 !cfa 14198

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5238 ax-nul 5248 ax-pr 5374

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rab 3397 df-v 3440 df-dif 3908 df-un 3910 df-ss 3922 df-nul 4287 df-if 4479 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4862 df-br 5096 df-opab 5158 df-mpt 5177 df-id 5518 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-iota 6442 df-fun 6488 df-fv 6494 df-ov 7356

This theorem is referenced by: efcllem 16002 ef0lem 16003 eff 16006 efval2 16009 efcvg 16010 efcvgfsum 16011 reefcl 16012 efcj 16017 efaddlem 16018 eftlcvg 16033 eftlcl 16034 reeftlcl 16035 eftlub 16036 efsep 16037 effsumlt 16038 efgt1p2 16041 efgt1p 16042 eflegeo 16048 eirrlem 16131 subfaclim 35160

W3C validator