taylpval - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > taylpval		Structured version Visualization version GIF version

Theorem taylpval 26700

Description: Value of the Taylor polynomial. (Contributed by Mario Carneiro, 31-Dec-2016.)

**Hypotheses**
Ref	Expression
taylpfval.s	⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
taylpfval.f	⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
taylpfval.a	⊢ (𝜑 → 𝐴 ⊆ 𝑆)
taylpfval.n	⊢ (𝜑 → 𝑁 ∈ ℕ₀)
taylpfval.b	⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D^𝑛 𝐹)‘𝑁))
taylpfval.t	⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)
taylpval.x	⊢ (𝜑 → 𝑋 ∈ ℂ)

**Assertion**
Ref	Expression
taylpval	⊢ (𝜑 → (𝑇‘𝑋) = Σ𝑘 ∈ (0...𝑁)(((((𝑆 D^𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘)))

Distinct variable groups: 𝐵,𝑘 𝑘,𝐹 𝑘,𝑁 𝜑,𝑘 𝑆,𝑘 𝑘,𝑋 Allowed substitution hints: 𝐴(𝑘) 𝑇(𝑘)

Proof of Theorem taylpval Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		taylpfval.s	. . 3 ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
2		taylpfval.f	. . 3 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
3		taylpfval.a	. . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝑆)
4		taylpfval.n	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
5		taylpfval.b	. . 3 ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D^𝑛 𝐹)‘𝑁))
6		taylpfval.t	. . 3 ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)
7	1, 2, 3, 4, 5, 6	taylpfval 26698	. 2 ⊢ (𝜑 → 𝑇 = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D^𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))
8		simplr 781	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑘 ∈ (0...𝑁)) → 𝑥 = 𝑋)
9	8	oveq1d 7436	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 − 𝐵) = (𝑋 − 𝐵))
10	9	oveq1d 7436	. . . 4 ⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑥 − 𝐵)↑𝑘) = ((𝑋 − 𝐵)↑𝑘))
11	10	oveq2d 7437	. . 3 ⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑘 ∈ (0...𝑁)) → (((((𝑆 D^𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)) = (((((𝑆 D^𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘)))
12	11	sumeq2dv 15875	. 2 ⊢ ((𝜑 ∧ 𝑥 = 𝑋) → Σ𝑘 ∈ (0...𝑁)(((((𝑆 D^𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)) = Σ𝑘 ∈ (0...𝑁)(((((𝑆 D^𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘)))
13		taylpval.x	. 2 ⊢ (𝜑 → 𝑋 ∈ ℂ)
14		sumex 15861	. . 3 ⊢ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D^𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘)) ∈ V
15	14	a1i 11	. 2 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)(((((𝑆 D^𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘)) ∈ V)
16	7, 12, 13, 15	fvmptd 7002	1 ⊢ (𝜑 → (𝑇‘𝑋) = Σ𝑘 ∈ (0...𝑁)(((((𝑆 D^𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1569 ∈ wcel 2144 Vcvv 3450 ⊆ wss 3895 {cpr 4586 dom cdm 5650 ⟶wf 6535 ‘cfv 6539 (class class class)co 7421 ℂcc 11202 ℝcr 11203 0cc0 11204 · cmul 11209 − cmin 11545 / cdiv 11977 ℕ₀cn0 12610 ...cfz 13643 ↑cexp 14208 !cfa 14421 Σcsu 15859 D^𝑛 cdvn 26190 Tayl ctayl 26686

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752 ax-inf2 9646 ax-cnex 11260 ax-resscn 11261 ax-1cn 11262 ax-icn 11263 ax-addcl 11264 ax-addrcl 11265 ax-mulcl 11266 ax-mulrcl 11267 ax-mulcom 11268 ax-addass 11269 ax-mulass 11270 ax-distr 11271 ax-i2m1 11272 ax-1ne0 11273 ax-1rid 11274 ax-rnegex 11275 ax-rrecex 11276 ax-cnre 11277 ax-pre-lttri 11278 ax-pre-lttrn 11279 ax-pre-ltadd 11280 ax-pre-mulgt0 11281 ax-pre-sup 11282 ax-addf 11283

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-isom 6548 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-om 7879 df-1st 8002 df-2nd 8003 df-supp 8181 df-frecs 8303 df-wrecs 8334 df-recs 8383 df-rdg 8422 df-1o 8480 df-er 8721 df-map 8853 df-pm 8854 df-en 8978 df-dom 8979 df-sdom 8980 df-fin 8981 df-fsupp 9358 df-fi 9407 df-sup 9438 df-inf 9439 df-oi 9508 df-card 10024 df-pnf 11349 df-mnf 11350 df-xr 11351 df-ltxr 11352 df-le 11353 df-sub 11547 df-neg 11548 df-div 11978 df-nn 12340 df-2 12409 df-3 12410 df-4 12411 df-5 12412 df-6 12413 df-7 12414 df-8 12415 df-9 12416 df-n0 12611 df-z 12698 df-dec 12819 df-uz 12970 df-q 13080 df-rp 13125 df-xneg 13245 df-xadd 13246 df-xmul 13247 df-icc 13487 df-fz 13644 df-fzo 13793 df-seq 14149 df-exp 14209 df-fac 14422 df-hash 14479 df-cj 15272 df-re 15273 df-im 15274 df-sqrt 15408 df-abs 15409 df-clim 15661 df-sum 15860 df-struct 17331 df-sets 17348 df-slot 17366 df-ndx 17378 df-base 17394 df-plusg 17447 df-mulr 17448 df-starv 17449 df-tset 17453 df-ple 17454 df-ds 17456 df-unif 17457 df-rest 17599 df-topn 17600 df-0g 17618 df-gsum 17619 df-topgen 17620 df-mgm 18822 df-sgrp 18914 df-mnd 18930 df-grp 19153 df-minusg 19154 df-cntz 19537 df-cmn 20002 df-abl 20003 df-mgp 20367 df-ur 20414 df-ring 20467 df-cring 20468 df-psmet 21676 df-xmet 21677 df-met 21678 df-bl 21679 df-mopn 21680 df-fbas 21681 df-fg 21682 df-cnfld 21685 df-top 23218 df-topon 23235 df-topsp 23257 df-bases 23270 df-cld 23343 df-ntr 23344 df-cls 23345 df-nei 23422 df-lp 23460 df-perf 23461 df-cnp 23552 df-haus 23639 df-fil 24171 df-fm 24263 df-flim 24264 df-flf 24265 df-tsms 24452 df-xms 24645 df-ms 24646 df-limc 26192 df-dv 26193 df-dvn 26194 df-tayl 26688

This theorem is used by: (None)

W3C validator