Metamath Proof Explorer


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 ‘ ℂ ) )