dvnply2

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

		Ref	Expression
	Assertion	dvnply2	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S) \land N \in ℕ_{0}) \to (ℂ D^{n} F) (N) \in Poly (S)$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ x = 0 \to (ℂ D^{n} F) (x) = (ℂ D^{n} F) (0)$
2	1	eleq1d	$⊢ x = 0 \to ((ℂ D^{n} F) (x) \in Poly (S) \leftrightarrow (ℂ D^{n} F) (0) \in Poly (S))$
3	2	imbi2d	$⊢ x = 0 \to (((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to (ℂ D^{n} F) (x) \in Poly (S)) \leftrightarrow ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to (ℂ D^{n} F) (0) \in Poly (S)))$
4		fveq2	$⊢ x = n \to (ℂ D^{n} F) (x) = (ℂ D^{n} F) (n)$
5	4	eleq1d	$⊢ x = n \to ((ℂ D^{n} F) (x) \in Poly (S) \leftrightarrow (ℂ D^{n} F) (n) \in Poly (S))$
6	5	imbi2d	$⊢ x = n \to (((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to (ℂ D^{n} F) (x) \in Poly (S)) \leftrightarrow ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to (ℂ D^{n} F) (n) \in Poly (S)))$
7		fveq2	$⊢ x = n + 1 \to (ℂ D^{n} F) (x) = (ℂ D^{n} F) (n + 1)$
8	7	eleq1d	$⊢ x = n + 1 \to ((ℂ D^{n} F) (x) \in Poly (S) \leftrightarrow (ℂ D^{n} F) (n + 1) \in Poly (S))$
9	8	imbi2d	$⊢ x = n + 1 \to (((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to (ℂ D^{n} F) (x) \in Poly (S)) \leftrightarrow ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to (ℂ D^{n} F) (n + 1) \in Poly (S)))$
10		fveq2	$⊢ x = N \to (ℂ D^{n} F) (x) = (ℂ D^{n} F) (N)$
11	10	eleq1d	$⊢ x = N \to ((ℂ D^{n} F) (x) \in Poly (S) \leftrightarrow (ℂ D^{n} F) (N) \in Poly (S))$
12	11	imbi2d	$⊢ x = N \to (((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to (ℂ D^{n} F) (x) \in Poly (S)) \leftrightarrow ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to (ℂ D^{n} F) (N) \in Poly (S)))$
13		ssid	$⊢ ℂ \subseteq ℂ$
14		cnex	$⊢ ℂ \in V$
15		plyf	$⊢ F \in Poly (S) \to F : ℂ ⟶ ℂ$
16	15	adantl	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to F : ℂ ⟶ ℂ$
17		fpmg	$⊢ (ℂ \in V \land ℂ \in V \land F : ℂ ⟶ ℂ) \to F \in (ℂ ↑_{𝑝𝑚} ℂ)$
18	14 14 16 17	mp3an12i	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to F \in (ℂ ↑_{𝑝𝑚} ℂ)$
19		dvn0	$⊢ (ℂ \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \to (ℂ D^{n} F) (0) = F$
20	13 18 19	sylancr	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to (ℂ D^{n} F) (0) = F$
21		simpr	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to F \in Poly (S)$
22	20 21	eqeltrd	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to (ℂ D^{n} F) (0) \in Poly (S)$
23		dvply2g	$⊢ (S \in SubRing (ℂ_{fld}) \land (ℂ D^{n} F) (n) \in Poly (S)) \to ℂ D (ℂ D^{n} F) (n) \in Poly (S)$
24	23	ex	$⊢ S \in SubRing (ℂ_{fld}) \to ((ℂ D^{n} F) (n) \in Poly (S) \to ℂ D (ℂ D^{n} F) (n) \in Poly (S))$
25	24	ad2antrr	$⊢ ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \land n \in ℕ_{0}) \to ((ℂ D^{n} F) (n) \in Poly (S) \to ℂ D (ℂ D^{n} F) (n) \in Poly (S))$
26		dvnp1	$⊢ (ℂ \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} ℂ) \land n \in ℕ_{0}) \to (ℂ D^{n} F) (n + 1) = ℂ D (ℂ D^{n} F) (n)$
27	13 26	mp3an1	$⊢ (F \in (ℂ ↑_{𝑝𝑚} ℂ) \land n \in ℕ_{0}) \to (ℂ D^{n} F) (n + 1) = ℂ D (ℂ D^{n} F) (n)$
28	18 27	sylan	$⊢ ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \land n \in ℕ_{0}) \to (ℂ D^{n} F) (n + 1) = ℂ D (ℂ D^{n} F) (n)$
29	28	eleq1d	$⊢ ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \land n \in ℕ_{0}) \to ((ℂ D^{n} F) (n + 1) \in Poly (S) \leftrightarrow ℂ D (ℂ D^{n} F) (n) \in Poly (S))$
30	25 29	sylibrd	$⊢ ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \land n \in ℕ_{0}) \to ((ℂ D^{n} F) (n) \in Poly (S) \to (ℂ D^{n} F) (n + 1) \in Poly (S))$
31	30	expcom	$⊢ n \in ℕ_{0} \to ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to ((ℂ D^{n} F) (n) \in Poly (S) \to (ℂ D^{n} F) (n + 1) \in Poly (S)))$
32	31	a2d	$⊢ n \in ℕ_{0} \to (((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to (ℂ D^{n} F) (n) \in Poly (S)) \to ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to (ℂ D^{n} F) (n + 1) \in Poly (S)))$
33	3 6 9 12 22 32	nn0ind	$⊢ N \in ℕ_{0} \to ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to (ℂ D^{n} F) (N) \in Poly (S))$
34	33	impcom	$⊢ ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \land N \in ℕ_{0}) \to (ℂ D^{n} F) (N) \in Poly (S)$
35	34	3impa	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S) \land N \in ℕ_{0}) \to (ℂ D^{n} F) (N) \in Poly (S)$

Metamath Proof Explorer

Theorem dvnply2

Proof