![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eftval | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
eftval.1 | ⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) |
Ref | Expression |
---|---|
eftval | ⊢ (𝑁 ∈ ℕ0 → (𝐹‘𝑁) = ((𝐴↑𝑁) / (!‘𝑁))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq2 6930 | . . 3 ⊢ (𝑛 = 𝑁 → (𝐴↑𝑛) = (𝐴↑𝑁)) | |
2 | fveq2 6446 | . . 3 ⊢ (𝑛 = 𝑁 → (!‘𝑛) = (!‘𝑁)) | |
3 | 1, 2 | oveq12d 6940 | . 2 ⊢ (𝑛 = 𝑁 → ((𝐴↑𝑛) / (!‘𝑛)) = ((𝐴↑𝑁) / (!‘𝑁))) |
4 | eftval.1 | . 2 ⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) | |
5 | ovex 6954 | . 2 ⊢ ((𝐴↑𝑁) / (!‘𝑁)) ∈ V | |
6 | 3, 4, 5 | fvmpt 6542 | 1 ⊢ (𝑁 ∈ ℕ0 → (𝐹‘𝑁) = ((𝐴↑𝑁) / (!‘𝑁))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1601 ∈ wcel 2107 ↦ cmpt 4965 ‘cfv 6135 (class class class)co 6922 / cdiv 11032 ℕ0cn0 11642 ↑cexp 13178 !cfa 13378 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5017 ax-nul 5025 ax-pr 5138 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-sbc 3653 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4672 df-br 4887 df-opab 4949 df-mpt 4966 df-id 5261 df-xp 5361 df-rel 5362 df-cnv 5363 df-co 5364 df-dm 5365 df-iota 6099 df-fun 6137 df-fv 6143 df-ov 6925 |
This theorem is referenced by: efcllem 15210 ef0lem 15211 eff 15214 efval2 15216 efcvg 15217 efcvgfsum 15218 reefcl 15219 efcj 15224 efaddlem 15225 eftlcvg 15238 eftlcl 15239 reeftlcl 15240 eftlub 15241 efsep 15242 effsumlt 15243 efgt1p2 15246 efgt1p 15247 eflegeo 15253 eirrlem 15336 subfaclim 31769 |
Copyright terms: Public domain | W3C validator |