dvnply2

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

		Ref	Expression
	Assertion	dvnply2	⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂ_fld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑁 ∈ ℕ₀ ) → ( ( ℂ 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 ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ₀ ) → ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( Poly ‘ 𝑆 ) → ( ℂ D ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑛 ) ) ∈ ( Poly ‘ 𝑆 ) ) )
26		dvnp1	⊢ ( ( ℂ ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑_pm ℂ ) ∧ 𝑛 ∈ ℕ₀ ) → ( ( ℂ D^𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ℂ D ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑛 ) ) )
27	13 26	mp3an1	⊢ ( ( 𝐹 ∈ ( ℂ ↑_pm ℂ ) ∧ 𝑛 ∈ ℕ₀ ) → ( ( ℂ D^𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ℂ D ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑛 ) ) )
28	18 27	sylan	⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂ_fld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ₀ ) → ( ( ℂ D^𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ℂ D ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑛 ) ) )
29	28	eleq1d	⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂ_fld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ₀ ) → ( ( ( ℂ D^𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ∈ ( Poly ‘ 𝑆 ) ↔ ( ℂ D ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑛 ) ) ∈ ( Poly ‘ 𝑆 ) ) )
30	25 29	sylibrd	⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂ_fld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ₀ ) → ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( Poly ‘ 𝑆 ) → ( ( ℂ D^𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ∈ ( Poly ‘ 𝑆 ) ) )
31	30	expcom	⊢ ( 𝑛 ∈ ℕ₀ → ( ( 𝑆 ∈ ( SubRing ‘ ℂ_fld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( Poly ‘ 𝑆 ) → ( ( ℂ D^𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ∈ ( Poly ‘ 𝑆 ) ) ) )
32	31	a2d	⊢ ( 𝑛 ∈ ℕ₀ → ( ( ( 𝑆 ∈ ( SubRing ‘ ℂ_fld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝑆 ∈ ( SubRing ‘ ℂ_fld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D^𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ∈ ( Poly ‘ 𝑆 ) ) ) )
33	3 6 9 12 22 32	nn0ind	⊢ ( 𝑁 ∈ ℕ₀ → ( ( 𝑆 ∈ ( SubRing ‘ ℂ_fld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( Poly ‘ 𝑆 ) ) )
34	33	impcom	⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂ_fld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑁 ∈ ℕ₀ ) → ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( Poly ‘ 𝑆 ) )
35	34	3impa	⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂ_fld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑁 ∈ ℕ₀ ) → ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( Poly ‘ 𝑆 ) )

Metamath Proof Explorer

Theorem dvnply2

Proof