Theorem dvnply

Description: Polynomials have polynomials as derivatives of all orders. (Contributed by Stefan O'Rear, 15-Nov-2014) (Revised by Mario Carneiro, 1-Jan-2017)

	Ref	Expression
Assertion	dvnply	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( Poly ‘ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		plyssc	⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
2	1	sseli	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
3		cnring	⊢ ℂfld ∈ Ring
4		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
5	4	subrgid	⊢ ( ℂfld ∈ Ring → ℂ ∈ ( SubRing ‘ ℂfld ) )
6	3 5	ax-mp	⊢ ℂ ∈ ( SubRing ‘ ℂfld )
7		dvnply2	⊢ ( ( ℂ ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( Poly ‘ ℂ ) )
8	6 7	mp3an1	⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( Poly ‘ ℂ ) )
9	2 8	sylan	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( Poly ‘ ℂ ) )