dvnply2 - Metamath Proof Explorer

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

Theorem dvnply2 26638

Description: Polynomials have polynomials as derivatives of all orders. (Contributed by Mario Carneiro, 1-Jan-2017.)

**Assertion**
Ref	Expression
dvnply2	⊢ ((𝑆 ∈ (SubRing‘ℂ_fld) ∧ 𝐹 ∈ (Poly‘𝑆) ∧ 𝑁 ∈ ℕ₀) → ((ℂ D^𝑛 𝐹)‘𝑁) ∈ (Poly‘𝑆))

Proof of Theorem dvnply2 Dummy variables 𝑥 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6908	. . . . . 6 ⊢ (𝑥 = 0 → ((ℂ D^𝑛 𝐹)‘𝑥) = ((ℂ D^𝑛 𝐹)‘0))
2	1	eleq1d 2849	. . . . 5 ⊢ (𝑥 = 0 → (((ℂ D^𝑛 𝐹)‘𝑥) ∈ (Poly‘𝑆) ↔ ((ℂ D^𝑛 𝐹)‘0) ∈ (Poly‘𝑆)))
3	2	imbi2d 343	. . . 4 ⊢ (𝑥 = 0 → (((𝑆 ∈ (SubRing‘ℂ_fld) ∧ 𝐹 ∈ (Poly‘𝑆)) → ((ℂ D^𝑛 𝐹)‘𝑥) ∈ (Poly‘𝑆)) ↔ ((𝑆 ∈ (SubRing‘ℂ_fld) ∧ 𝐹 ∈ (Poly‘𝑆)) → ((ℂ D^𝑛 𝐹)‘0) ∈ (Poly‘𝑆))))
4		fveq2 6908	. . . . . 6 ⊢ (𝑥 = 𝑛 → ((ℂ D^𝑛 𝐹)‘𝑥) = ((ℂ D^𝑛 𝐹)‘𝑛))
5	4	eleq1d 2849	. . . . 5 ⊢ (𝑥 = 𝑛 → (((ℂ D^𝑛 𝐹)‘𝑥) ∈ (Poly‘𝑆) ↔ ((ℂ D^𝑛 𝐹)‘𝑛) ∈ (Poly‘𝑆)))
6	5	imbi2d 343	. . . 4 ⊢ (𝑥 = 𝑛 → (((𝑆 ∈ (SubRing‘ℂ_fld) ∧ 𝐹 ∈ (Poly‘𝑆)) → ((ℂ D^𝑛 𝐹)‘𝑥) ∈ (Poly‘𝑆)) ↔ ((𝑆 ∈ (SubRing‘ℂ_fld) ∧ 𝐹 ∈ (Poly‘𝑆)) → ((ℂ D^𝑛 𝐹)‘𝑛) ∈ (Poly‘𝑆))))
7		fveq2 6908	. . . . . 6 ⊢ (𝑥 = (𝑛 + 1) → ((ℂ D^𝑛 𝐹)‘𝑥) = ((ℂ D^𝑛 𝐹)‘(𝑛 + 1)))
8	7	eleq1d 2849	. . . . 5 ⊢ (𝑥 = (𝑛 + 1) → (((ℂ D^𝑛 𝐹)‘𝑥) ∈ (Poly‘𝑆) ↔ ((ℂ D^𝑛 𝐹)‘(𝑛 + 1)) ∈ (Poly‘𝑆)))
9	8	imbi2d 343	. . . 4 ⊢ (𝑥 = (𝑛 + 1) → (((𝑆 ∈ (SubRing‘ℂ_fld) ∧ 𝐹 ∈ (Poly‘𝑆)) → ((ℂ D^𝑛 𝐹)‘𝑥) ∈ (Poly‘𝑆)) ↔ ((𝑆 ∈ (SubRing‘ℂ_fld) ∧ 𝐹 ∈ (Poly‘𝑆)) → ((ℂ D^𝑛 𝐹)‘(𝑛 + 1)) ∈ (Poly‘𝑆))))
10		fveq2 6908	. . . . . 6 ⊢ (𝑥 = 𝑁 → ((ℂ D^𝑛 𝐹)‘𝑥) = ((ℂ D^𝑛 𝐹)‘𝑁))
11	10	eleq1d 2849	. . . . 5 ⊢ (𝑥 = 𝑁 → (((ℂ D^𝑛 𝐹)‘𝑥) ∈ (Poly‘𝑆) ↔ ((ℂ D^𝑛 𝐹)‘𝑁) ∈ (Poly‘𝑆)))
12	11	imbi2d 343	. . . 4 ⊢ (𝑥 = 𝑁 → (((𝑆 ∈ (SubRing‘ℂ_fld) ∧ 𝐹 ∈ (Poly‘𝑆)) → ((ℂ D^𝑛 𝐹)‘𝑥) ∈ (Poly‘𝑆)) ↔ ((𝑆 ∈ (SubRing‘ℂ_fld) ∧ 𝐹 ∈ (Poly‘𝑆)) → ((ℂ D^𝑛 𝐹)‘𝑁) ∈ (Poly‘𝑆))))
13		ssid 3935	. . . . . 6 ⊢ ℂ ⊆ ℂ
14		cnex 11308	. . . . . . 7 ⊢ ℂ ∈ V
15		plyf 26546	. . . . . . . 8 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
16	15	adantl 487	. . . . . . 7 ⊢ ((𝑆 ∈ (SubRing‘ℂ_fld) ∧ 𝐹 ∈ (Poly‘𝑆)) → 𝐹:ℂ⟶ℂ)
17		fpmg 8924	. . . . . . 7 ⊢ ((ℂ ∈ V ∧ ℂ ∈ V ∧ 𝐹:ℂ⟶ℂ) → 𝐹 ∈ (ℂ ↑_pm ℂ))
18	14, 14, 16, 17	mp3an12i 1495	. . . . . 6 ⊢ ((𝑆 ∈ (SubRing‘ℂ_fld) ∧ 𝐹 ∈ (Poly‘𝑆)) → 𝐹 ∈ (ℂ ↑_pm ℂ))
19		dvn0 26274	. . . . . 6 ⊢ ((ℂ ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm ℂ)) → ((ℂ D^𝑛 𝐹)‘0) = 𝐹)
20	13, 18, 19	sylancr 599	. . . . 5 ⊢ ((𝑆 ∈ (SubRing‘ℂ_fld) ∧ 𝐹 ∈ (Poly‘𝑆)) → ((ℂ D^𝑛 𝐹)‘0) = 𝐹)
21		simpr 490	. . . . 5 ⊢ ((𝑆 ∈ (SubRing‘ℂ_fld) ∧ 𝐹 ∈ (Poly‘𝑆)) → 𝐹 ∈ (Poly‘𝑆))
22	20, 21	eqeltrd 2864	. . . 4 ⊢ ((𝑆 ∈ (SubRing‘ℂ_fld) ∧ 𝐹 ∈ (Poly‘𝑆)) → ((ℂ D^𝑛 𝐹)‘0) ∈ (Poly‘𝑆))
23		dvply2g 26636	. . . . . . . . 9 ⊢ ((𝑆 ∈ (SubRing‘ℂ_fld) ∧ ((ℂ D^𝑛 𝐹)‘𝑛) ∈ (Poly‘𝑆)) → (ℂ D ((ℂ D^𝑛 𝐹)‘𝑛)) ∈ (Poly‘𝑆))
24	23	ex 418	. . . . . . . 8 ⊢ (𝑆 ∈ (SubRing‘ℂ_fld) → (((ℂ D^𝑛 𝐹)‘𝑛) ∈ (Poly‘𝑆) → (ℂ D ((ℂ D^𝑛 𝐹)‘𝑛)) ∈ (Poly‘𝑆)))
25	24	ad2antrr 739	. . . . . . 7 ⊢ (((𝑆 ∈ (SubRing‘ℂ_fld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ₀) → (((ℂ D^𝑛 𝐹)‘𝑛) ∈ (Poly‘𝑆) → (ℂ D ((ℂ D^𝑛 𝐹)‘𝑛)) ∈ (Poly‘𝑆)))
26		dvnp1 26275	. . . . . . . . . 10 ⊢ ((ℂ ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm ℂ) ∧ 𝑛 ∈ ℕ₀) → ((ℂ D^𝑛 𝐹)‘(𝑛 + 1)) = (ℂ D ((ℂ D^𝑛 𝐹)‘𝑛)))
27	13, 26	mp3an1 1478	. . . . . . . . 9 ⊢ ((𝐹 ∈ (ℂ ↑_pm ℂ) ∧ 𝑛 ∈ ℕ₀) → ((ℂ D^𝑛 𝐹)‘(𝑛 + 1)) = (ℂ D ((ℂ D^𝑛 𝐹)‘𝑛)))
28	18, 27	sylan 592	. . . . . . . 8 ⊢ (((𝑆 ∈ (SubRing‘ℂ_fld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ₀) → ((ℂ D^𝑛 𝐹)‘(𝑛 + 1)) = (ℂ D ((ℂ D^𝑛 𝐹)‘𝑛)))
29	28	eleq1d 2849	. . . . . . 7 ⊢ (((𝑆 ∈ (SubRing‘ℂ_fld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ₀) → (((ℂ D^𝑛 𝐹)‘(𝑛 + 1)) ∈ (Poly‘𝑆) ↔ (ℂ D ((ℂ D^𝑛 𝐹)‘𝑛)) ∈ (Poly‘𝑆)))
30	25, 29	sylibrd 262	. . . . . 6 ⊢ (((𝑆 ∈ (SubRing‘ℂ_fld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑛 ∈ ℕ₀) → (((ℂ D^𝑛 𝐹)‘𝑛) ∈ (Poly‘𝑆) → ((ℂ D^𝑛 𝐹)‘(𝑛 + 1)) ∈ (Poly‘𝑆)))
31	30	expcom 419	. . . . 5 ⊢ (𝑛 ∈ ℕ₀ → ((𝑆 ∈ (SubRing‘ℂ_fld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (((ℂ D^𝑛 𝐹)‘𝑛) ∈ (Poly‘𝑆) → ((ℂ D^𝑛 𝐹)‘(𝑛 + 1)) ∈ (Poly‘𝑆))))
32	31	a2d 30	. . . 4 ⊢ (𝑛 ∈ ℕ₀ → (((𝑆 ∈ (SubRing‘ℂ_fld) ∧ 𝐹 ∈ (Poly‘𝑆)) → ((ℂ D^𝑛 𝐹)‘𝑛) ∈ (Poly‘𝑆)) → ((𝑆 ∈ (SubRing‘ℂ_fld) ∧ 𝐹 ∈ (Poly‘𝑆)) → ((ℂ D^𝑛 𝐹)‘(𝑛 + 1)) ∈ (Poly‘𝑆))))
33	3, 6, 9, 12, 22, 32	nn0ind 12821	. . 3 ⊢ (𝑁 ∈ ℕ₀ → ((𝑆 ∈ (SubRing‘ℂ_fld) ∧ 𝐹 ∈ (Poly‘𝑆)) → ((ℂ D^𝑛 𝐹)‘𝑁) ∈ (Poly‘𝑆)))
34	33	impcom 413	. 2 ⊢ (((𝑆 ∈ (SubRing‘ℂ_fld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑁 ∈ ℕ₀) → ((ℂ D^𝑛 𝐹)‘𝑁) ∈ (Poly‘𝑆))
35	34	3impa 1127	1 ⊢ ((𝑆 ∈ (SubRing‘ℂ_fld) ∧ 𝐹 ∈ (Poly‘𝑆) ∧ 𝑁 ∈ ℕ₀) → ((ℂ D^𝑛 𝐹)‘𝑁) ∈ (Poly‘𝑆))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 Vcvv 3454 ⊆ wss 3900 ⟶wf 6554 ‘cfv 6558 (class class class)co 7443 ↑_pm cpm 8876 ℂcc 11225 0cc0 11227 1c1 11228 + caddc 11230 ℕ₀cn0 12633 SubRingcsubrg 20851 ℂ_fldccnfld 21708 D cdv 26213 D^𝑛 cdvn 26214 Polycply 26532

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7775 ax-inf2 9669 ax-cnex 11283 ax-resscn 11284 ax-1cn 11285 ax-icn 11286 ax-addcl 11287 ax-addrcl 11288 ax-mulcl 11289 ax-mulrcl 11290 ax-mulcom 11291 ax-addass 11292 ax-mulass 11293 ax-distr 11294 ax-i2m1 11295 ax-1ne0 11296 ax-1rid 11297 ax-rnegex 11298 ax-rrecex 11299 ax-cnre 11300 ax-pre-lttri 11301 ax-pre-lttrn 11302 ax-pre-ltadd 11303 ax-pre-mulgt0 11304 ax-pre-sup 11305 ax-addf 11306

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6322 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6512 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-isom 6567 df-riota 7400 df-ov 7446 df-oprab 7447 df-mpo 7448 df-of 7717 df-om 7902 df-1st 8025 df-2nd 8026 df-supp 8205 df-frecs 8327 df-wrecs 8358 df-recs 8407 df-rdg 8446 df-1o 8504 df-2o 8505 df-er 8745 df-map 8877 df-pm 8878 df-ixp 8954 df-en 9002 df-dom 9003 df-sdom 9004 df-fin 9005 df-fsupp 9382 df-fi 9430 df-sup 9461 df-inf 9462 df-oi 9531 df-card 10047 df-pnf 11372 df-mnf 11373 df-xr 11374 df-ltxr 11375 df-le 11376 df-sub 11570 df-neg 11571 df-div 12001 df-nn 12363 df-2 12432 df-3 12433 df-4 12434 df-5 12435 df-6 12436 df-7 12437 df-8 12438 df-9 12439 df-n0 12634 df-z 12721 df-dec 12842 df-uz 12993 df-q 13103 df-rp 13148 df-xneg 13268 df-xadd 13269 df-xmul 13270 df-icc 13510 df-fz 13667 df-fzo 13816 df-fl 13959 df-seq 14172 df-exp 14232 df-hash 14502 df-cj 15295 df-re 15296 df-im 15297 df-sqrt 15431 df-abs 15432 df-clim 15684 df-rlim 15685 df-sum 15883 df-struct 17354 df-sets 17371 df-slot 17389 df-ndx 17401 df-base 17417 df-ress 17438 df-plusg 17470 df-mulr 17471 df-starv 17472 df-sca 17473 df-vsca 17474 df-ip 17475 df-tset 17476 df-ple 17477 df-ds 17479 df-unif 17480 df-hom 17481 df-cco 17482 df-rest 17622 df-topn 17623 df-0g 17641 df-gsum 17642 df-topgen 17643 df-pt 17644 df-prds 17647 df-xrs 17703 df-qtop 17708 df-imas 17709 df-xps 17711 df-mre 17785 df-mrc 17786 df-acs 17788 df-mgm 18845 df-sgrp 18937 df-mnd 18953 df-submnd 19008 df-grp 19176 df-minusg 19177 df-mulg 19307 df-subg 19362 df-cntz 19561 df-cmn 20026 df-abl 20027 df-mgp 20391 df-rng 20405 df-ur 20438 df-ring 20491 df-cring 20492 df-subrng 20828 df-subrg 20852 df-psmet 21700 df-xmet 21701 df-met 21702 df-bl 21703 df-mopn 21704 df-fbas 21705 df-fg 21706 df-cnfld 21709 df-top 23242 df-topon 23259 df-topsp 23281 df-bases 23294 df-cld 23367 df-ntr 23368 df-cls 23369 df-nei 23446 df-lp 23484 df-perf 23485 df-cn 23575 df-cnp 23576 df-haus 23663 df-tx 23911 df-hmeo 24104 df-fil 24195 df-fm 24287 df-flim 24288 df-flf 24289 df-xms 24669 df-ms 24670 df-tms 24671 df-cncf 25229 df-0p 26021 df-limc 26216 df-dv 26217 df-dvn 26218 df-ply 26536 df-coe 26538 df-dgr 26539

This theorem is used by: dvnply 26639 taylthlem2 26731

W3C validator