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 15814

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 7303	. . 3 ⊢ (𝑛 = 𝑁 → (𝐴↑𝑛) = (𝐴↑𝑁))
2		fveq2 6792	. . 3 ⊢ (𝑛 = 𝑁 → (!‘𝑛) = (!‘𝑁))
3	1, 2	oveq12d 7313	. 2 ⊢ (𝑛 = 𝑁 → ((𝐴↑𝑛) / (!‘𝑛)) = ((𝐴↑𝑁) / (!‘𝑁)))
4		eftval.1	. 2 ⊢ 𝐹 = (𝑛 ∈ ℕ₀ ↦ ((𝐴↑𝑛) / (!‘𝑛)))
5		ovex 7328	. 2 ⊢ ((𝐴↑𝑁) / (!‘𝑁)) ∈ V
6	3, 4, 5	fvmpt 6895	1 ⊢ (𝑁 ∈ ℕ₀ → (𝐹‘𝑁) = ((𝐴↑𝑁) / (!‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1537 ∈ wcel 2101 ↦ cmpt 5160 ‘cfv 6447 (class class class)co 7295 / cdiv 11660 ℕ₀cn0 12261 ↑cexp 13810 !cfa 14015

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2103 ax-9 2111 ax-10 2132 ax-11 2149 ax-12 2166 ax-ext 2704 ax-sep 5226 ax-nul 5233 ax-pr 5355

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2063 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2884 df-ne 2939 df-ral 3060 df-rex 3069 df-rab 3224 df-v 3436 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-nul 4260 df-if 4463 df-sn 4565 df-pr 4567 df-op 4571 df-uni 4842 df-br 5078 df-opab 5140 df-mpt 5161 df-id 5491 df-xp 5597 df-rel 5598 df-cnv 5599 df-co 5600 df-dm 5601 df-iota 6399 df-fun 6449 df-fv 6455 df-ov 7298

This theorem is referenced by: efcllem 15815 ef0lem 15816 eff 15819 efval2 15821 efcvg 15822 efcvgfsum 15823 reefcl 15824 efcj 15829 efaddlem 15830 eftlcvg 15843 eftlcl 15844 reeftlcl 15845 eftlub 15846 efsep 15847 effsumlt 15848 efgt1p2 15851 efgt1p 15852 eflegeo 15858 eirrlem 15941 subfaclim 33178

W3C validator