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 ⊢ F ∈ Poly ⁡ S ∧ N ∈ ℕ 0 → ℂ D n F ⁡ N ∈ Poly ⁡ ℂ

Proof

Step Hyp Ref Expression
1 plyssc ⊢ Poly ⁡ S ⊆ Poly ⁡ ℂ
2 1 sseli ⊢ F ∈ Poly ⁡ S → F ∈ 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 ∧ F ∈ Poly ⁡ ℂ ∧ N ∈ ℕ 0 → ℂ D n F ⁡ N ∈ Poly ⁡ ℂ
8 6 7 mp3an1 ⊢ F ∈ Poly ⁡ ℂ ∧ N ∈ ℕ 0 → ℂ D n F ⁡ N ∈ Poly ⁡ ℂ
9 2 8 sylan ⊢ F ∈ Poly ⁡ S ∧ N ∈ ℕ 0 → ℂ D n F ⁡ N ∈ Poly ⁡ ℂ