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 16011

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2114 ↦ cmpt 5181 ‘cfv 6500 (class class class)co 7368 / cdiv 11806 ℕ₀cn0 12413 ↑cexp 13996 !cfa 14208

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5243 ax-nul 5253 ax-pr 5379

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rab 3402 df-v 3444 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4288 df-if 4482 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-br 5101 df-opab 5163 df-mpt 5182 df-id 5527 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-iota 6456 df-fun 6502 df-fv 6508 df-ov 7371

This theorem is referenced by: efcllem 16012 ef0lem 16013 eff 16016 efval2 16019 efcvg 16020 efcvgfsum 16021 reefcl 16022 efcj 16027 efaddlem 16028 eftlcvg 16043 eftlcl 16044 reeftlcl 16045 eftlub 16046 efsep 16047 effsumlt 16048 efgt1p2 16051 efgt1p 16052 eflegeo 16058 eirrlem 16141 subfaclim 35401

W3C validator