Metamath Proof Explorer


Theorem dvnply2

Description: Polynomials have polynomials as derivatives of all orders. (Contributed by Mario Carneiro, 1-Jan-2017)

Ref Expression
Assertion dvnply2 ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( Poly ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 fveq2 ( 𝑥 = 0 → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑥 ) = ( ( ℂ D𝑛 𝐹 ) ‘ 0 ) )
2 1 eleq1d ( 𝑥 = 0 → ( ( ( ℂ D𝑛 𝐹 ) ‘ 𝑥 ) ∈ ( Poly ‘ 𝑆 ) ↔ ( ( ℂ D𝑛 𝐹 ) ‘ 0 ) ∈ ( Poly ‘ 𝑆 ) ) )
3 2 imbi2d ( 𝑥 = 0 → ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑥 ) ∈ ( Poly ‘ 𝑆 ) ) ↔ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ 0 ) ∈ ( Poly ‘ 𝑆 ) ) ) )
4 fveq2 ( 𝑥 = 𝑛 → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑥 ) = ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) )
5 4 eleq1d ( 𝑥 = 𝑛 → ( ( ( ℂ D𝑛 𝐹 ) ‘ 𝑥 ) ∈ ( Poly ‘ 𝑆 ) ↔ ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( Poly ‘ 𝑆 ) ) )
6 5 imbi2d ( 𝑥 = 𝑛 → ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑥 ) ∈ ( Poly ‘ 𝑆 ) ) ↔ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( Poly ‘ 𝑆 ) ) ) )
7 fveq2 ( 𝑥 = ( 𝑛 + 1 ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑥 ) = ( ( ℂ D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) )
8 7 eleq1d ( 𝑥 = ( 𝑛 + 1 ) → ( ( ( ℂ D𝑛 𝐹 ) ‘ 𝑥 ) ∈ ( Poly ‘ 𝑆 ) ↔ ( ( ℂ D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ∈ ( Poly ‘ 𝑆 ) ) )
9 8 imbi2d ( 𝑥 = ( 𝑛 + 1 ) → ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑥 ) ∈ ( Poly ‘ 𝑆 ) ) ↔ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ∈ ( Poly ‘ 𝑆 ) ) ) )
10 fveq2 ( 𝑥 = 𝑁 → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑥 ) = ( ( ℂ D𝑛 𝐹 ) ‘ 𝑁 ) )
11 10 eleq1d ( 𝑥 = 𝑁 → ( ( ( ℂ D𝑛 𝐹 ) ‘ 𝑥 ) ∈ ( Poly ‘ 𝑆 ) ↔ ( ( ℂ D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( Poly ‘ 𝑆 ) ) )
12 11 imbi2d ( 𝑥 = 𝑁 → ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑥 ) ∈ ( Poly ‘ 𝑆 ) ) ↔ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( Poly ‘ 𝑆 ) ) ) )
13 ssid ℂ ⊆ ℂ
14 cnex ℂ ∈ V
15 plyf ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ )
16 15 adantl ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → 𝐹 : ℂ ⟶ ℂ )
17 fpmg ( ( ℂ ∈ V ∧ ℂ ∈ V ∧ 𝐹 : ℂ ⟶ ℂ ) → 𝐹 ∈ ( ℂ ↑pm ℂ ) )
18 14 14 16 17 mp3an12i ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → 𝐹 ∈ ( ℂ ↑pm ℂ ) )
19 dvn0 ( ( ℂ ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm ℂ ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ 0 ) = 𝐹 )
20 13 18 19 sylancr ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ 0 ) = 𝐹 )
21 simpr ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
22 20 21 eqeltrd ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ 0 ) ∈ ( Poly ‘ 𝑆 ) )
23 dvply2g ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( Poly ‘ 𝑆 ) ) → ( ℂ D ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ) ∈ ( Poly ‘ 𝑆 ) )
24 23 ex ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → ( ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( Poly ‘ 𝑆 ) → ( ℂ D ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ) ∈ ( Poly ‘ 𝑆 ) ) )
25 24 ad2antrr ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( Poly ‘ 𝑆 ) → ( ℂ D ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ) ∈ ( Poly ‘ 𝑆 ) ) )
26 dvnp1 ( ( ℂ ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm ℂ ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ℂ D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ℂ D ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ) )
27 13 26 mp3an1 ( ( 𝐹 ∈ ( ℂ ↑pm ℂ ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ℂ D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ℂ D ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ) )
28 18 27 sylan ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ℂ D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ℂ D ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ) )
29 28 eleq1d ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( ℂ D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ∈ ( Poly ‘ 𝑆 ) ↔ ( ℂ D ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ) ∈ ( Poly ‘ 𝑆 ) ) )
30 25 29 sylibrd ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( Poly ‘ 𝑆 ) → ( ( ℂ D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ∈ ( Poly ‘ 𝑆 ) ) )
31 30 expcom ( 𝑛 ∈ ℕ0 → ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( Poly ‘ 𝑆 ) → ( ( ℂ D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ∈ ( Poly ‘ 𝑆 ) ) ) )
32 31 a2d ( 𝑛 ∈ ℕ0 → ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ∈ ( Poly ‘ 𝑆 ) ) ) )
33 3 6 9 12 22 32 nn0ind ( 𝑁 ∈ ℕ0 → ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( Poly ‘ 𝑆 ) ) )
34 33 impcom ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( Poly ‘ 𝑆 ) )
35 34 3impa ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( Poly ‘ 𝑆 ) )