This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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