dvnprodlem3 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dvnprodlem3		Structured version Unicode version

Theorem dvnprodlem3 31987

Description: The multinomial formula for the

-th derivative of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)

**Hypotheses**
Ref	Expression
dvnprodlem3.s
dvnprodlem3.x	ℂ_fld ↾_t
dvnprodlem3.t
dvnprodlem3.h	$/\$
dvnprodlem3.n
dvnprodlem3.dvnh	$/\$ $/\$
dvnprodlem3.f
dvnprodlem3.d
dvnprodlem3.c

**Assertion**
Ref	Expression
dvnprodlem3

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

Proof of Theorem dvnprodlem3 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		prodeq1 13801	. . . . . . . . 9
2	1	mpteq2dv 4526	. . . . . . . 8
3	2	oveq2d 6286	. . . . . . 7
4	3	fveq1d 5850	. . . . . 6
5		fveq2 5848	. . . . . . . . . 10
6	5	fveq1d 5850	. . . . . . . . 9
7	6	sumeq1d 13608	. . . . . . . 8
8		prodeq1 13801	. . . . . . . . . . 11
9	8	oveq2d 6286	. . . . . . . . . 10
10		prodeq1 13801	. . . . . . . . . 10
11	9, 10	oveq12d 6288	. . . . . . . . 9
12	11	sumeq2ad 31808	. . . . . . . 8
13	7, 12	eqtrd 2495	. . . . . . 7
14	13	mpteq2dv 4526	. . . . . 6
15	4, 14	eqeq12d 2476	. . . . 5
16	15	ralbidv 2893	. . . 4
17		prodeq1 13801	. . . . . . . . 9
18	17	mpteq2dv 4526	. . . . . . . 8
19	18	oveq2d 6286	. . . . . . 7
20	19	fveq1d 5850	. . . . . 6
21		fveq2 5848	. . . . . . . . . 10
22	21	fveq1d 5850	. . . . . . . . 9
23	22	sumeq1d 13608	. . . . . . . 8
24		prodeq1 13801	. . . . . . . . . . 11
25	24	oveq2d 6286	. . . . . . . . . 10
26		prodeq1 13801	. . . . . . . . . 10
27	25, 26	oveq12d 6288	. . . . . . . . 9
28	27	sumeq2ad 31808	. . . . . . . 8
29	23, 28	eqtrd 2495	. . . . . . 7
30	29	mpteq2dv 4526	. . . . . 6
31	20, 30	eqeq12d 2476	. . . . 5
32	31	ralbidv 2893	. . . 4
33		prodeq1 13801	. . . . . . . . 9
34	33	mpteq2dv 4526	. . . . . . . 8
35	34	oveq2d 6286	. . . . . . 7
36	35	fveq1d 5850	. . . . . 6
37		fveq2 5848	. . . . . . . . . 10
38	37	fveq1d 5850	. . . . . . . . 9
39	38	sumeq1d 13608	. . . . . . . 8
40		prodeq1 13801	. . . . . . . . . . 11
41	40	oveq2d 6286	. . . . . . . . . 10
42		prodeq1 13801	. . . . . . . . . 10
43	41, 42	oveq12d 6288	. . . . . . . . 9
44	43	sumeq2ad 31808	. . . . . . . 8
45	39, 44	eqtrd 2495	. . . . . . 7
46	45	mpteq2dv 4526	. . . . . 6
47	36, 46	eqeq12d 2476	. . . . 5
48	47	ralbidv 2893	. . . 4
49		prodeq1 13801	. . . . . . . . . 10
50	49	mpteq2dv 4526	. . . . . . . . 9
51		dvnprodlem3.f	. . . . . . . . . . 11
52	51	a1i 11	. . . . . . . . . 10
53	52	eqcomd 2462	. . . . . . . . 9
54	50, 53	eqtrd 2495	. . . . . . . 8
55	54	oveq2d 6286	. . . . . . 7
56	55	fveq1d 5850	. . . . . 6
57		fveq2 5848	. . . . . . . . . 10
58	57	fveq1d 5850	. . . . . . . . 9
59	58	sumeq1d 13608	. . . . . . . 8
60		prodeq1 13801	. . . . . . . . . . 11
61	60	oveq2d 6286	. . . . . . . . . 10
62		prodeq1 13801	. . . . . . . . . 10
63	61, 62	oveq12d 6288	. . . . . . . . 9
64	63	sumeq2ad 31808	. . . . . . . 8
65	59, 64	eqtrd 2495	. . . . . . 7
66	65	mpteq2dv 4526	. . . . . 6
67	56, 66	eqeq12d 2476	. . . . 5
68	67	ralbidv 2893	. . . 4
69		prod0 13835	. . . . . . . . . . . . 13
70	69	mpteq2i 4522	. . . . . . . . . . . 12
71	70	oveq2i 6281	. . . . . . . . . . 11
72	71	a1i 11	. . . . . . . . . 10
73		id 22	. . . . . . . . . 10
74	72, 73	fveq12d 5854	. . . . . . . . 9
75	74	adantl 464	. . . . . . . 8 $/\$
76		dvnprodlem3.s	. . . . . . . . . . 11
77		recnprss 22477	. . . . . . . . . . 11
78	76, 77	syl 16	. . . . . . . . . 10
79		1cnd 9601	. . . . . . . . . . . . . 14 $/\$
80		eqid 2454	. . . . . . . . . . . . . 14
81	79, 80	fmptd 6031	. . . . . . . . . . . . 13
82		1re 9584	. . . . . . . . . . . . . . . . 17
83	82	rgenw 2815	. . . . . . . . . . . . . . . 16
84		dmmptg 5487	. . . . . . . . . . . . . . . 16
85	83, 84	ax-mp 5	. . . . . . . . . . . . . . 15
86	85	a1i 11	. . . . . . . . . . . . . 14
87	86	feq2d 5700	. . . . . . . . . . . . 13
88	81, 87	mpbird 232	. . . . . . . . . . . 12
89		restsspw 14924	. . . . . . . . . . . . . . 15 ℂ_fld ↾_t
90		dvnprodlem3.x	. . . . . . . . . . . . . . 15 ℂ_fld ↾_t
91	89, 90	sseldi 3487	. . . . . . . . . . . . . 14
92		elpwi 4008	. . . . . . . . . . . . . 14
93	91, 92	syl 16	. . . . . . . . . . . . 13
94	86, 93	eqsstrd 3523	. . . . . . . . . . . 12
95	88, 94	jca 530	. . . . . . . . . . 11 $/\$
96		cnex 9562	. . . . . . . . . . . . 13
97	96	a1i 11	. . . . . . . . . . . 12
98		elpm2g 7428	. . . . . . . . . . . 12 $/\$ $/\$
99	97, 76, 98	syl2anc 659	. . . . . . . . . . 11 $/\$
100	95, 99	mpbird 232	. . . . . . . . . 10
101		dvn0 22496	. . . . . . . . . 10 $/\$
102	78, 100, 101	syl2anc 659	. . . . . . . . 9
103	102	adantr 463	. . . . . . . 8 $/\$
104		fveq2 5848	. . . . . . . . . . . . . . 15
105	104	adantl 464	. . . . . . . . . . . . . 14 $/\$
106		dvnprodlem3.d	. . . . . . . . . . . . . . . . . 18
107	106	a1i 11	. . . . . . . . . . . . . . . . 17
108		oveq2 6278	. . . . . . . . . . . . . . . . . . . . . 22
109		elmapfn 7434	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
110		fn0 5682	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
111	109, 110	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
112		elsn 4030	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
113	111, 112	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . 26
114	112	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
115		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
116		f0 5748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
117		ovex 6298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
118		0ex 4569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
119	117, 118	elmap 7440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
120	116, 119	mpbir 209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
121	120	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
122	115, 121	eqeltrd 2542	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
123	114, 122	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26
124	113, 123	impbii 188	. . . . . . . . . . . . . . . . . . . . . . . . 25
125	124	ax-gen 1623	. . . . . . . . . . . . . . . . . . . . . . . 24
126		dfcleq 2447	. . . . . . . . . . . . . . . . . . . . . . . 24
127	125, 126	mpbir 209	. . . . . . . . . . . . . . . . . . . . . . 23
128	127	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
129	108, 128	eqtrd 2495	. . . . . . . . . . . . . . . . . . . . 21
130		rabeq 3100	. . . . . . . . . . . . . . . . . . . . 21
131	129, 130	syl 16	. . . . . . . . . . . . . . . . . . . 20
132		sumeq1 13596	. . . . . . . . . . . . . . . . . . . . . 22
133	132	eqeq1d 2456	. . . . . . . . . . . . . . . . . . . . 21
134	133	rabbidv 3098	. . . . . . . . . . . . . . . . . . . 20
135	131, 134	eqtrd 2495	. . . . . . . . . . . . . . . . . . 19
136	135	mpteq2dv 4526	. . . . . . . . . . . . . . . . . 18
137	136	adantl 464	. . . . . . . . . . . . . . . . 17 $/\$
138		0elpw 4606	. . . . . . . . . . . . . . . . . 18
139	138	a1i 11	. . . . . . . . . . . . . . . . 17
140		nn0ex 10797	. . . . . . . . . . . . . . . . . . 19
141	140	mptex 6118	. . . . . . . . . . . . . . . . . 18
142	141	a1i 11	. . . . . . . . . . . . . . . . 17
143	107, 137, 139, 142	fvmptd 5936	. . . . . . . . . . . . . . . 16
144		eqeq2 2469	. . . . . . . . . . . . . . . . . 18
145	144	rabbidv 3098	. . . . . . . . . . . . . . . . 17
146	145	adantl 464	. . . . . . . . . . . . . . . 16 $/\$
147		0nn0 10806	. . . . . . . . . . . . . . . . 17
148	147	a1i 11	. . . . . . . . . . . . . . . 16
149		p0ex 4624	. . . . . . . . . . . . . . . . . 18
150	149	rabex 4588	. . . . . . . . . . . . . . . . 17
151	150	a1i 11	. . . . . . . . . . . . . . . 16
152	143, 146, 148, 151	fvmptd 5936	. . . . . . . . . . . . . . 15
153	152	adantr 463	. . . . . . . . . . . . . 14 $/\$
154		snidg 4042	. . . . . . . . . . . . . . . . . . . . . 22
155	118, 154	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
156		eqid 2454	. . . . . . . . . . . . . . . . . . . . 21
157	155, 156	pm3.2i 453	. . . . . . . . . . . . . . . . . . . 20 $/\$
158		sum0 13628	. . . . . . . . . . . . . . . . . . . . . . 23
159	158	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
160	159	eqeq1d 2456	. . . . . . . . . . . . . . . . . . . . 21
161	160	elrab 3254	. . . . . . . . . . . . . . . . . . . 20 $/\$
162	157, 161	mpbir 209	. . . . . . . . . . . . . . . . . . 19
163	162	ne0ii 3790	. . . . . . . . . . . . . . . . . 18
164	163	neii 2653	. . . . . . . . . . . . . . . . 17
165		eqid 2454	. . . . . . . . . . . . . . . . . 18
166		rabrsn 4086	. . . . . . . . . . . . . . . . . 18 $\/$
167	165, 166	ax-mp 5	. . . . . . . . . . . . . . . . 17 $\/$
168	164, 167	mtpor 1607	. . . . . . . . . . . . . . . 16
169	168	a1i 11	. . . . . . . . . . . . . . 15 $/\$
170		iftrue 3935	. . . . . . . . . . . . . . . 16
171	170	adantl 464	. . . . . . . . . . . . . . 15 $/\$
172	169, 171	eqtr4d 2498	. . . . . . . . . . . . . 14 $/\$
173	105, 153, 172	3eqtrd 2499	. . . . . . . . . . . . 13 $/\$
174	173, 171	eqtrd 2495	. . . . . . . . . . . 12 $/\$
175	174	sumeq1d 13608	. . . . . . . . . . 11 $/\$
176		fveq2 5848	. . . . . . . . . . . . . . . . . 18
177		fac0 12341	. . . . . . . . . . . . . . . . . . 19
178	177	a1i 11	. . . . . . . . . . . . . . . . . 18
179	176, 178	eqtrd 2495	. . . . . . . . . . . . . . . . 17
180	179	oveq1d 6285	. . . . . . . . . . . . . . . 16
181		prod0 13835	. . . . . . . . . . . . . . . . . 18
182	181	oveq2i 6281	. . . . . . . . . . . . . . . . 17
183		1div1e1 10233	. . . . . . . . . . . . . . . . 17
184	182, 183	eqtri 2483	. . . . . . . . . . . . . . . 16
185	180, 184	syl6eq 2511	. . . . . . . . . . . . . . 15
186		prod0 13835	. . . . . . . . . . . . . . . 16
187	186	a1i 11	. . . . . . . . . . . . . . 15
188	185, 187	oveq12d 6288	. . . . . . . . . . . . . 14
189	188	ad2antlr 724	. . . . . . . . . . . . 13 $/\$ $/\$
190		1t1e1 10679	. . . . . . . . . . . . . 14
191	190	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
192	189, 191	eqtrd 2495	. . . . . . . . . . . 12 $/\$ $/\$
193	192	sumeq2dv 13610	. . . . . . . . . . 11 $/\$
194		ax-1cn 9539	. . . . . . . . . . . . 13
195		eqidd 2455	. . . . . . . . . . . . . 14
196	195	sumsn 13648	. . . . . . . . . . . . 13 $/\$
197	118, 194, 196	mp2an 670	. . . . . . . . . . . 12
198	197	a1i 11	. . . . . . . . . . 11 $/\$
199	175, 193, 198	3eqtrd 2499	. . . . . . . . . 10 $/\$
200	199	mpteq2dv 4526	. . . . . . . . 9 $/\$
201	200	eqcomd 2462	. . . . . . . 8 $/\$
202	75, 103, 201	3eqtrd 2499	. . . . . . 7 $/\$
203	202	a1d 25	. . . . . 6 $/\$
204	71	fveq1i 5849	. . . . . . . . 9
205	204	a1i 11	. . . . . . . 8 $/\$ $/\$
206	76	adantr 463	. . . . . . . . . 10 $/\$
207	206	adantr 463	. . . . . . . . 9 $/\$ $/\$
208	90	adantr 463	. . . . . . . . . 10 $/\$ ℂ_fld ↾_t
209	208	adantr 463	. . . . . . . . 9 $/\$ $/\$ ℂ_fld ↾_t
210	194	a1i 11	. . . . . . . . 9 $/\$ $/\$
211		elfznn0 11775	. . . . . . . . . . . . 13
212	211	adantl 464	. . . . . . . . . . . 12 $/\$
213		neqne 31677	. . . . . . . . . . . . 13
214	213	adantr 463	. . . . . . . . . . . 12 $/\$
215	212, 214	jca 530	. . . . . . . . . . 11 $/\$ $/\$
216		elnnne0 10805	. . . . . . . . . . 11 $/\$
217	215, 216	sylibr 212	. . . . . . . . . 10 $/\$
218	217	adantll 711	. . . . . . . . 9 $/\$ $/\$
219	207, 209, 210, 218	dvnmptconst 31980	. . . . . . . 8 $/\$ $/\$
220	143	ad2antrr 723	. . . . . . . . . . . 12 $/\$ $/\$
221		eqeq2 2469	. . . . . . . . . . . . . . . . 17
222	221	rabbidv 3098	. . . . . . . . . . . . . . . 16
223	222	adantl 464	. . . . . . . . . . . . . . 15 $/\$
224		eqidd 2455	. . . . . . . . . . . . . . . . . . . . . 22
225		id 22	. . . . . . . . . . . . . . . . . . . . . . 23
226	225	eqcomd 2462	. . . . . . . . . . . . . . . . . . . . . 22
227	158	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
228	224, 226, 227	3eqtrd 2499	. . . . . . . . . . . . . . . . . . . . 21
229	228	adantl 464	. . . . . . . . . . . . . . . . . . . 20 $/\$
230	229	adantll 711	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
231		simpll 751	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
232	230, 231	pm2.65da 574	. . . . . . . . . . . . . . . . . 18 $/\$
233	232	ralrimiva 2868	. . . . . . . . . . . . . . . . 17
234		rabeq0 3806	. . . . . . . . . . . . . . . . 17
235	233, 234	sylibr 212	. . . . . . . . . . . . . . . 16
236	235	adantr 463	. . . . . . . . . . . . . . 15 $/\$
237	223, 236	eqtrd 2495	. . . . . . . . . . . . . 14 $/\$
238	237	adantll 711	. . . . . . . . . . . . 13 $/\$ $/\$
239	238	adantlr 712	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
240	211	adantl 464	. . . . . . . . . . . 12 $/\$ $/\$
241	118	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$
242	220, 239, 240, 241	fvmptd 5936	. . . . . . . . . . 11 $/\$ $/\$
243	242	sumeq1d 13608	. . . . . . . . . 10 $/\$ $/\$
244		sum0 13628	. . . . . . . . . . 11
245	244	a1i 11	. . . . . . . . . 10 $/\$ $/\$
246	243, 245	eqtr2d 2496	. . . . . . . . 9 $/\$ $/\$
247	246	mpteq2dv 4526	. . . . . . . 8 $/\$ $/\$
248	205, 219, 247	3eqtrd 2499	. . . . . . 7 $/\$ $/\$
249	248	ex 432	. . . . . 6 $/\$
250	203, 249	pm2.61dan 789	. . . . 5
251	250	ralrimiv 2866	. . . 4
252		simpll 751	. . . . . . . 8 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$
253		fveq2 5848	. . . . . . . . . . . . . . . . 17
254	253	prodeq2ad 31832	. . . . . . . . . . . . . . . 16
255		fveq2 5848	. . . . . . . . . . . . . . . . . . 19
256	255	fveq1d 5850	. . . . . . . . . . . . . . . . . 18
257	256	cbvprodv 13808	. . . . . . . . . . . . . . . . 17
258	257	a1i 11	. . . . . . . . . . . . . . . 16
259	254, 258	eqtrd 2495	. . . . . . . . . . . . . . 15
260	259	cbvmptv 4530	. . . . . . . . . . . . . 14
261	260	oveq2i 6281	. . . . . . . . . . . . 13
262	261	fveq1i 5849	. . . . . . . . . . . 12
263		fveq2 5848	. . . . . . . . . . . . . . . . . . . 20
264	263	fveq2d 5852	. . . . . . . . . . . . . . . . . . 19
265	264	cbvprodv 13808	. . . . . . . . . . . . . . . . . 18
266	265	oveq2i 6281	. . . . . . . . . . . . . . . . 17
267	266	a1i 11	. . . . . . . . . . . . . . . 16
268		fveq2 5848	. . . . . . . . . . . . . . . . . 18
269	268	prodeq2ad 31832	. . . . . . . . . . . . . . . . 17
270	255	oveq2d 6286	. . . . . . . . . . . . . . . . . . . . 21
271	270, 263	fveq12d 5854	. . . . . . . . . . . . . . . . . . . 20
272	271	fveq1d 5850	. . . . . . . . . . . . . . . . . . 19
273	272	cbvprodv 13808	. . . . . . . . . . . . . . . . . 18
274	273	a1i 11	. . . . . . . . . . . . . . . . 17
275	269, 274	eqtrd 2495	. . . . . . . . . . . . . . . 16
276	267, 275	oveq12d 6288	. . . . . . . . . . . . . . 15
277	276	sumeq2ad 31808	. . . . . . . . . . . . . 14
278		fveq1 5847	. . . . . . . . . . . . . . . . . . . 20
279	278	fveq2d 5852	. . . . . . . . . . . . . . . . . . 19
280	279	prodeq2ad 31832	. . . . . . . . . . . . . . . . . 18
281	280	oveq2d 6286	. . . . . . . . . . . . . . . . 17
282	278	fveq2d 5852	. . . . . . . . . . . . . . . . . . 19
283	282	fveq1d 5850	. . . . . . . . . . . . . . . . . 18
284	283	prodeq2ad 31832	. . . . . . . . . . . . . . . . 17
285	281, 284	oveq12d 6288	. . . . . . . . . . . . . . . 16
286	285	cbvsumv 13603	. . . . . . . . . . . . . . 15
287	286	a1i 11	. . . . . . . . . . . . . 14
288	277, 287	eqtrd 2495	. . . . . . . . . . . . 13
289	288	cbvmptv 4530	. . . . . . . . . . . 12
290	262, 289	eqeq12i 2474	. . . . . . . . . . 11
291	290	ralbii 2885	. . . . . . . . . 10
292	291	biimpi 194	. . . . . . . . 9
293	292	ad2antlr 724	. . . . . . . 8 $/\$ $/\$ $\$ $/\$ $/\$
294		simpr 459	. . . . . . . 8 $/\$ $/\$ $\$ $/\$ $/\$
295	76	ad3antrrr 727	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ $/\$
296	90	ad3antrrr 727	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ $/\$ ℂ_fld ↾_t
297		dvnprodlem3.t	. . . . . . . . . 10
298	297	ad3antrrr 727	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ $/\$
299		simp-4l 765	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$