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 e. ( Poly ` S ) /\ N e. NN0 ) -> ( ( CC Dn F ) ` N ) e. ( Poly ` CC ) )

Proof

Step Hyp Ref Expression
1 plyssc 
 |-  ( Poly ` S ) C_ ( Poly ` CC )
2 1 sseli 
 |-  ( F e. ( Poly ` S ) -> F e. ( Poly ` CC ) )
3 cnring 
 |-  CCfld e. Ring
4 cnfldbas 
 |-  CC = ( Base ` CCfld )
5 4 subrgid 
 |-  ( CCfld e. Ring -> CC e. ( SubRing ` CCfld ) )
6 3 5 ax-mp 
 |-  CC e. ( SubRing ` CCfld )
7 dvnply2 
 |-  ( ( CC e. ( SubRing ` CCfld ) /\ F e. ( Poly ` CC ) /\ N e. NN0 ) -> ( ( CC Dn F ) ` N ) e. ( Poly ` CC ) )
8 6 7 mp3an1 
 |-  ( ( F e. ( Poly ` CC ) /\ N e. NN0 ) -> ( ( CC Dn F ) ` N ) e. ( Poly ` CC ) )
9 2 8 sylan 
 |-  ( ( F e. ( Poly ` S ) /\ N e. NN0 ) -> ( ( CC Dn F ) ` N ) e. ( Poly ` CC ) )