dvply1

Description: Derivative of a polynomial, explicit sum version. (Contributed by Stefan O'Rear, 13-Nov-2014) (Revised by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Hypotheses	dvply1.f	$⊢ φ \to F = (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k})$
	dvply1.g	$⊢ φ \to G = (z \in ℂ ⟼ \sum_{k = 0}^{N - 1} B (k) z^{k})$
	dvply1.a	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
	dvply1.b	$⊢ B = (k \in ℕ_{0} ⟼ (k + 1) A (k + 1))$
	dvply1.n	$⊢ φ \to N \in ℕ_{0}$
Assertion	dvply1	$⊢ φ \to ℂ D F = G$

Proof

Step	Hyp	Ref	Expression
1		dvply1.f	$⊢ φ \to F = (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k})$
2		dvply1.g	$⊢ φ \to G = (z \in ℂ ⟼ \sum_{k = 0}^{N - 1} B (k) z^{k})$
3		dvply1.a	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
4		dvply1.b	$⊢ B = (k \in ℕ_{0} ⟼ (k + 1) A (k + 1))$
5		dvply1.n	$⊢ φ \to N \in ℕ_{0}$
6	1	oveq2d	$⊢ φ \to ℂ D F = \frac{d (z \in ℂ⟼ \sum_{k = 0}^{N} A (k) z^{k})}{d_{ℂ} z}$
7		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
8	7	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
9	8	toponrestid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
10		cnelprrecn	$⊢ ℂ \in \{ℝ, ℂ\}$
11	10	a1i	$⊢ φ \to ℂ \in \{ℝ, ℂ\}$
12	7	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
13		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
14	13	topopn	$⊢ TopOpen (ℂ_{fld}) \in Top \to ℂ \in TopOpen (ℂ_{fld})$
15	12 14	mp1i	$⊢ φ \to ℂ \in TopOpen (ℂ_{fld})$
16		fzfid	$⊢ φ \to (0 \dots N) \in Fin$
17		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
18		ffvelcdm	$⊢ (A : ℕ_{0} ⟶ ℂ \land k \in ℕ_{0}) \to A (k) \in ℂ$
19	3 17 18	syl2an	$⊢ (φ \land k \in (0 \dots N)) \to A (k) \in ℂ$
20	19	adantr	$⊢ ((φ \land k \in (0 \dots N)) \land z \in ℂ) \to A (k) \in ℂ$
21		simpr	$⊢ ((φ \land k \in (0 \dots N)) \land z \in ℂ) \to z \in ℂ$
22	17	ad2antlr	$⊢ ((φ \land k \in (0 \dots N)) \land z \in ℂ) \to k \in ℕ_{0}$
23	21 22	expcld	$⊢ ((φ \land k \in (0 \dots N)) \land z \in ℂ) \to z^{k} \in ℂ$
24	20 23	mulcld	$⊢ ((φ \land k \in (0 \dots N)) \land z \in ℂ) \to A (k) z^{k} \in ℂ$
25	24	3impa	$⊢ (φ \land k \in (0 \dots N) \land z \in ℂ) \to A (k) z^{k} \in ℂ$
26	19	3adant3	$⊢ (φ \land k \in (0 \dots N) \land z \in ℂ) \to A (k) \in ℂ$
27		0cnd	$⊢ ((φ \land k \in (0 \dots N) \land z \in ℂ) \land k = 0) \to 0 \in ℂ$
28		simpl2	$⊢ ((φ \land k \in (0 \dots N) \land z \in ℂ) \land \neg k = 0) \to k \in (0 \dots N)$
29	28 17	syl	$⊢ ((φ \land k \in (0 \dots N) \land z \in ℂ) \land \neg k = 0) \to k \in ℕ_{0}$
30	29	nn0cnd	$⊢ ((φ \land k \in (0 \dots N) \land z \in ℂ) \land \neg k = 0) \to k \in ℂ$
31		simpl3	$⊢ ((φ \land k \in (0 \dots N) \land z \in ℂ) \land \neg k = 0) \to z \in ℂ$
32		simpr	$⊢ ((φ \land k \in (0 \dots N) \land z \in ℂ) \land \neg k = 0) \to \neg k = 0$
33		elnn0	$⊢ k \in ℕ_{0} \leftrightarrow (k \in ℕ \lor k = 0)$
34	29 33	sylib	$⊢ ((φ \land k \in (0 \dots N) \land z \in ℂ) \land \neg k = 0) \to (k \in ℕ \lor k = 0)$
35		orel2	$⊢ \neg k = 0 \to ((k \in ℕ \lor k = 0) \to k \in ℕ)$
36	32 34 35	sylc	$⊢ ((φ \land k \in (0 \dots N) \land z \in ℂ) \land \neg k = 0) \to k \in ℕ$
37		nnm1nn0	$⊢ k \in ℕ \to k - 1 \in ℕ_{0}$
38	36 37	syl	$⊢ ((φ \land k \in (0 \dots N) \land z \in ℂ) \land \neg k = 0) \to k - 1 \in ℕ_{0}$
39	31 38	expcld	$⊢ ((φ \land k \in (0 \dots N) \land z \in ℂ) \land \neg k = 0) \to z^{k - 1} \in ℂ$
40	30 39	mulcld	$⊢ ((φ \land k \in (0 \dots N) \land z \in ℂ) \land \neg k = 0) \to k z^{k - 1} \in ℂ$
41	27 40	ifclda	$⊢ (φ \land k \in (0 \dots N) \land z \in ℂ) \to if (k = 0, 0, k z^{k - 1}) \in ℂ$
42	26 41	mulcld	$⊢ (φ \land k \in (0 \dots N) \land z \in ℂ) \to A (k) if (k = 0, 0, k z^{k - 1}) \in ℂ$
43	10	a1i	$⊢ (φ \land k \in (0 \dots N)) \to ℂ \in \{ℝ, ℂ\}$
44		c0ex	$⊢ 0 \in V$
45		ovex	$⊢ k z^{k - 1} \in V$
46	44 45	ifex	$⊢ if (k = 0, 0, k z^{k - 1}) \in V$
47	46	a1i	$⊢ ((φ \land k \in (0 \dots N)) \land z \in ℂ) \to if (k = 0, 0, k z^{k - 1}) \in V$
48	17	adantl	$⊢ (φ \land k \in (0 \dots N)) \to k \in ℕ_{0}$
49		dvexp2	$⊢ k \in ℕ_{0} \to \frac{d (z \in ℂ⟼ z^{k})}{d_{ℂ} z} = (z \in ℂ ⟼ if (k = 0, 0, k z^{k - 1}))$
50	48 49	syl	$⊢ (φ \land k \in (0 \dots N)) \to \frac{d (z \in ℂ⟼ z^{k})}{d_{ℂ} z} = (z \in ℂ ⟼ if (k = 0, 0, k z^{k - 1}))$
51	43 23 47 50 19	dvmptcmul	$⊢ (φ \land k \in (0 \dots N)) \to \frac{d (z \in ℂ⟼ A (k) z^{k})}{d_{ℂ} z} = (z \in ℂ ⟼ A (k) if (k = 0, 0, k z^{k - 1}))$
52	9 7 11 15 16 25 42 51	dvmptfsum	$⊢ φ \to \frac{d (z \in ℂ⟼ \sum_{k = 0}^{N} A (k) z^{k})}{d_{ℂ} z} = (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) if (k = 0, 0, k z^{k - 1}))$
53		elfznn	$⊢ k \in (1 \dots N) \to k \in ℕ$
54	53	nnne0d	$⊢ k \in (1 \dots N) \to k \neq 0$
55	54	neneqd	$⊢ k \in (1 \dots N) \to \neg k = 0$
56	55	adantl	$⊢ ((φ \land z \in ℂ) \land k \in (1 \dots N)) \to \neg k = 0$
57	56	iffalsed	$⊢ ((φ \land z \in ℂ) \land k \in (1 \dots N)) \to if (k = 0, 0, k z^{k - 1}) = k z^{k - 1}$
58	57	oveq2d	$⊢ ((φ \land z \in ℂ) \land k \in (1 \dots N)) \to A (k) if (k = 0, 0, k z^{k - 1}) = A (k) k z^{k - 1}$
59	58	sumeq2dv	$⊢ (φ \land z \in ℂ) \to \sum_{k = 1}^{N} A (k) if (k = 0, 0, k z^{k - 1}) = \sum_{k = 1}^{N} A (k) k z^{k - 1}$
60		1eluzge0	$⊢ 1 \in ℤ_{\geq 0}$
61		fzss1	$⊢ 1 \in ℤ_{\geq 0} \to (1 \dots N) \subseteq (0 \dots N)$
62	60 61	mp1i	$⊢ (φ \land z \in ℂ) \to (1 \dots N) \subseteq (0 \dots N)$
63	3	adantr	$⊢ (φ \land z \in ℂ) \to A : ℕ_{0} ⟶ ℂ$
64	53	nnnn0d	$⊢ k \in (1 \dots N) \to k \in ℕ_{0}$
65	63 64 18	syl2an	$⊢ ((φ \land z \in ℂ) \land k \in (1 \dots N)) \to A (k) \in ℂ$
66	54	adantl	$⊢ ((φ \land z \in ℂ) \land k \in (1 \dots N)) \to k \neq 0$
67	66	neneqd	$⊢ ((φ \land z \in ℂ) \land k \in (1 \dots N)) \to \neg k = 0$
68	67	iffalsed	$⊢ ((φ \land z \in ℂ) \land k \in (1 \dots N)) \to if (k = 0, 0, k z^{k - 1}) = k z^{k - 1}$
69	64	adantl	$⊢ ((φ \land z \in ℂ) \land k \in (1 \dots N)) \to k \in ℕ_{0}$
70	69	nn0cnd	$⊢ ((φ \land z \in ℂ) \land k \in (1 \dots N)) \to k \in ℂ$
71		simplr	$⊢ ((φ \land z \in ℂ) \land k \in (1 \dots N)) \to z \in ℂ$
72	53 37	syl	$⊢ k \in (1 \dots N) \to k - 1 \in ℕ_{0}$
73	72	adantl	$⊢ ((φ \land z \in ℂ) \land k \in (1 \dots N)) \to k - 1 \in ℕ_{0}$
74	71 73	expcld	$⊢ ((φ \land z \in ℂ) \land k \in (1 \dots N)) \to z^{k - 1} \in ℂ$
75	70 74	mulcld	$⊢ ((φ \land z \in ℂ) \land k \in (1 \dots N)) \to k z^{k - 1} \in ℂ$
76	68 75	eqeltrd	$⊢ ((φ \land z \in ℂ) \land k \in (1 \dots N)) \to if (k = 0, 0, k z^{k - 1}) \in ℂ$
77	65 76	mulcld	$⊢ ((φ \land z \in ℂ) \land k \in (1 \dots N)) \to A (k) if (k = 0, 0, k z^{k - 1}) \in ℂ$
78		eldifn	$⊢ k \in ((0 \dots N) ∖ (1 \dots N)) \to \neg k \in (1 \dots N)$
79		0p1e1	$⊢ 0 + 1 = 1$
80	79	oveq1i	$⊢ (0 + 1 \dots N) = (1 \dots N)$
81	80	eleq2i	$⊢ k \in (0 + 1 \dots N) \leftrightarrow k \in (1 \dots N)$
82	78 81	sylnibr	$⊢ k \in ((0 \dots N) ∖ (1 \dots N)) \to \neg k \in (0 + 1 \dots N)$
83	82	adantl	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots N) ∖ (1 \dots N))) \to \neg k \in (0 + 1 \dots N)$
84		eldifi	$⊢ k \in ((0 \dots N) ∖ (1 \dots N)) \to k \in (0 \dots N)$
85	84	adantl	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots N) ∖ (1 \dots N))) \to k \in (0 \dots N)$
86		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
87	5 86	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 0}$
88	87	ad2antrr	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots N) ∖ (1 \dots N))) \to N \in ℤ_{\geq 0}$
89		elfzp12	$⊢ N \in ℤ_{\geq 0} \to (k \in (0 \dots N) \leftrightarrow (k = 0 \lor k \in (0 + 1 \dots N)))$
90	88 89	syl	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots N) ∖ (1 \dots N))) \to (k \in (0 \dots N) \leftrightarrow (k = 0 \lor k \in (0 + 1 \dots N)))$
91	85 90	mpbid	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots N) ∖ (1 \dots N))) \to (k = 0 \lor k \in (0 + 1 \dots N))$
92		orel2	$⊢ \neg k \in (0 + 1 \dots N) \to ((k = 0 \lor k \in (0 + 1 \dots N)) \to k = 0)$
93	83 91 92	sylc	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots N) ∖ (1 \dots N))) \to k = 0$
94	93	iftrued	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots N) ∖ (1 \dots N))) \to if (k = 0, 0, k z^{k - 1}) = 0$
95	94	oveq2d	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots N) ∖ (1 \dots N))) \to A (k) if (k = 0, 0, k z^{k - 1}) = A (k) \cdot 0$
96	63 17 18	syl2an	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots N)) \to A (k) \in ℂ$
97	96	mul01d	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots N)) \to A (k) \cdot 0 = 0$
98	84 97	sylan2	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots N) ∖ (1 \dots N))) \to A (k) \cdot 0 = 0$
99	95 98	eqtrd	$⊢ ((φ \land z \in ℂ) \land k \in ((0 \dots N) ∖ (1 \dots N))) \to A (k) if (k = 0, 0, k z^{k - 1}) = 0$
100		fzfid	$⊢ (φ \land z \in ℂ) \to (0 \dots N) \in Fin$
101	62 77 99 100	fsumss	$⊢ (φ \land z \in ℂ) \to \sum_{k = 1}^{N} A (k) if (k = 0, 0, k z^{k - 1}) = \sum_{k = 0}^{N} A (k) if (k = 0, 0, k z^{k - 1})$
102		elfznn0	$⊢ j \in (0 \dots N - 1) \to j \in ℕ_{0}$
103	102	adantl	$⊢ ((φ \land z \in ℂ) \land j \in (0 \dots N - 1)) \to j \in ℕ_{0}$
104	103	nn0cnd	$⊢ ((φ \land z \in ℂ) \land j \in (0 \dots N - 1)) \to j \in ℂ$
105		ax-1cn	$⊢ 1 \in ℂ$
106		pncan	$⊢ (j \in ℂ \land 1 \in ℂ) \to j + 1 - 1 = j$
107	104 105 106	sylancl	$⊢ ((φ \land z \in ℂ) \land j \in (0 \dots N - 1)) \to j + 1 - 1 = j$
108	107	oveq2d	$⊢ ((φ \land z \in ℂ) \land j \in (0 \dots N - 1)) \to z^{j + 1 - 1} = z^{j}$
109	108	oveq2d	$⊢ ((φ \land z \in ℂ) \land j \in (0 \dots N - 1)) \to (j + 1) z^{j + 1 - 1} = (j + 1) z^{j}$
110	109	oveq2d	$⊢ ((φ \land z \in ℂ) \land j \in (0 \dots N - 1)) \to A (j + 1) (j + 1) z^{j + 1 - 1} = A (j + 1) (j + 1) z^{j}$
111	3	ad2antrr	$⊢ ((φ \land z \in ℂ) \land j \in (0 \dots N - 1)) \to A : ℕ_{0} ⟶ ℂ$
112		peano2nn0	$⊢ j \in ℕ_{0} \to j + 1 \in ℕ_{0}$
113	102 112	syl	$⊢ j \in (0 \dots N - 1) \to j + 1 \in ℕ_{0}$
114	113	adantl	$⊢ ((φ \land z \in ℂ) \land j \in (0 \dots N - 1)) \to j + 1 \in ℕ_{0}$
115	111 114	ffvelcdmd	$⊢ ((φ \land z \in ℂ) \land j \in (0 \dots N - 1)) \to A (j + 1) \in ℂ$
116	114	nn0cnd	$⊢ ((φ \land z \in ℂ) \land j \in (0 \dots N - 1)) \to j + 1 \in ℂ$
117		simplr	$⊢ ((φ \land z \in ℂ) \land j \in (0 \dots N - 1)) \to z \in ℂ$
118	117 103	expcld	$⊢ ((φ \land z \in ℂ) \land j \in (0 \dots N - 1)) \to z^{j} \in ℂ$
119	115 116 118	mulassd	$⊢ ((φ \land z \in ℂ) \land j \in (0 \dots N - 1)) \to A (j + 1) (j + 1) z^{j} = A (j + 1) (j + 1) z^{j}$
120	115 116	mulcomd	$⊢ ((φ \land z \in ℂ) \land j \in (0 \dots N - 1)) \to A (j + 1) (j + 1) = (j + 1) A (j + 1)$
121	120	oveq1d	$⊢ ((φ \land z \in ℂ) \land j \in (0 \dots N - 1)) \to A (j + 1) (j + 1) z^{j} = (j + 1) A (j + 1) z^{j}$
122	110 119 121	3eqtr2d	$⊢ ((φ \land z \in ℂ) \land j \in (0 \dots N - 1)) \to A (j + 1) (j + 1) z^{j + 1 - 1} = (j + 1) A (j + 1) z^{j}$
123	122	sumeq2dv	$⊢ (φ \land z \in ℂ) \to \sum_{j = 0}^{N - 1} A (j + 1) (j + 1) z^{j + 1 - 1} = \sum_{j = 0}^{N - 1} (j + 1) A (j + 1) z^{j}$
124		1m1e0	$⊢ 1 - 1 = 0$
125	124	oveq1i	$⊢ (1 - 1 \dots N - 1) = (0 \dots N - 1)$
126	125	sumeq1i	$⊢ \sum_{j = 1 - 1}^{N - 1} A (j + 1) (j + 1) z^{j + 1 - 1} = \sum_{j = 0}^{N - 1} A (j + 1) (j + 1) z^{j + 1 - 1}$
127		oveq1	$⊢ k = j \to k + 1 = j + 1$
128		fvoveq1	$⊢ k = j \to A (k + 1) = A (j + 1)$
129	127 128	oveq12d	$⊢ k = j \to (k + 1) A (k + 1) = (j + 1) A (j + 1)$
130		oveq2	$⊢ k = j \to z^{k} = z^{j}$
131	129 130	oveq12d	$⊢ k = j \to (k + 1) A (k + 1) z^{k} = (j + 1) A (j + 1) z^{j}$
132	131	cbvsumv	$⊢ \sum_{k = 0}^{N - 1} (k + 1) A (k + 1) z^{k} = \sum_{j = 0}^{N - 1} (j + 1) A (j + 1) z^{j}$
133	123 126 132	3eqtr4g	$⊢ (φ \land z \in ℂ) \to \sum_{j = 1 - 1}^{N - 1} A (j + 1) (j + 1) z^{j + 1 - 1} = \sum_{k = 0}^{N - 1} (k + 1) A (k + 1) z^{k}$
134		1zzd	$⊢ (φ \land z \in ℂ) \to 1 \in ℤ$
135	5	adantr	$⊢ (φ \land z \in ℂ) \to N \in ℕ_{0}$
136	135	nn0zd	$⊢ (φ \land z \in ℂ) \to N \in ℤ$
137	65 75	mulcld	$⊢ ((φ \land z \in ℂ) \land k \in (1 \dots N)) \to A (k) k z^{k - 1} \in ℂ$
138		fveq2	$⊢ k = j + 1 \to A (k) = A (j + 1)$
139		id	$⊢ k = j + 1 \to k = j + 1$
140		oveq1	$⊢ k = j + 1 \to k - 1 = j + 1 - 1$
141	140	oveq2d	$⊢ k = j + 1 \to z^{k - 1} = z^{j + 1 - 1}$
142	139 141	oveq12d	$⊢ k = j + 1 \to k z^{k - 1} = (j + 1) z^{j + 1 - 1}$
143	138 142	oveq12d	$⊢ k = j + 1 \to A (k) k z^{k - 1} = A (j + 1) (j + 1) z^{j + 1 - 1}$
144	134 134 136 137 143	fsumshftm	$⊢ (φ \land z \in ℂ) \to \sum_{k = 1}^{N} A (k) k z^{k - 1} = \sum_{j = 1 - 1}^{N - 1} A (j + 1) (j + 1) z^{j + 1 - 1}$
145		elfznn0	$⊢ k \in (0 \dots N - 1) \to k \in ℕ_{0}$
146	145	adantl	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots N - 1)) \to k \in ℕ_{0}$
147		ovex	$⊢ (k + 1) A (k + 1) \in V$
148	4	fvmpt2	$⊢ (k \in ℕ_{0} \land (k + 1) A (k + 1) \in V) \to B (k) = (k + 1) A (k + 1)$
149	146 147 148	sylancl	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots N - 1)) \to B (k) = (k + 1) A (k + 1)$
150	149	oveq1d	$⊢ ((φ \land z \in ℂ) \land k \in (0 \dots N - 1)) \to B (k) z^{k} = (k + 1) A (k + 1) z^{k}$
151	150	sumeq2dv	$⊢ (φ \land z \in ℂ) \to \sum_{k = 0}^{N - 1} B (k) z^{k} = \sum_{k = 0}^{N - 1} (k + 1) A (k + 1) z^{k}$
152	133 144 151	3eqtr4d	$⊢ (φ \land z \in ℂ) \to \sum_{k = 1}^{N} A (k) k z^{k - 1} = \sum_{k = 0}^{N - 1} B (k) z^{k}$
153	59 101 152	3eqtr3d	$⊢ (φ \land z \in ℂ) \to \sum_{k = 0}^{N} A (k) if (k = 0, 0, k z^{k - 1}) = \sum_{k = 0}^{N - 1} B (k) z^{k}$
154	153	mpteq2dva	$⊢ φ \to (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) if (k = 0, 0, k z^{k - 1})) = (z \in ℂ ⟼ \sum_{k = 0}^{N - 1} B (k) z^{k})$
155	154 2	eqtr4d	$⊢ φ \to (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) if (k = 0, 0, k z^{k - 1})) = G$
156	6 52 155	3eqtrd	$⊢ φ \to ℂ D F = G$

Metamath Proof Explorer

Theorem dvply1

Proof