dvnprodlem3 - Mathbox for Glauco Siliprandi

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

Theorem dvnprodlem3 37920

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 14040	. . . . . . . . 9
2	1	mpteq2dv 4483	. . . . . . . 8
3	2	oveq2d 6324	. . . . . . 7
4	3	fveq1d 5881	. . . . . 6
5		fveq2 5879	. . . . . . . . . 10
6	5	fveq1d 5881	. . . . . . . . 9
7	6	sumeq1d 13844	. . . . . . . 8
8		prodeq1 14040	. . . . . . . . . . 11
9	8	oveq2d 6324	. . . . . . . . . 10
10		prodeq1 14040	. . . . . . . . . 10
11	9, 10	oveq12d 6326	. . . . . . . . 9
12	11	sumeq2ad 37740	. . . . . . . 8
13	7, 12	eqtrd 2505	. . . . . . 7
14	13	mpteq2dv 4483	. . . . . 6
15	4, 14	eqeq12d 2486	. . . . 5
16	15	ralbidv 2829	. . . 4
17		prodeq1 14040	. . . . . . . . 9
18	17	mpteq2dv 4483	. . . . . . . 8
19	18	oveq2d 6324	. . . . . . 7
20	19	fveq1d 5881	. . . . . 6
21		fveq2 5879	. . . . . . . . . 10
22	21	fveq1d 5881	. . . . . . . . 9
23	22	sumeq1d 13844	. . . . . . . 8
24		prodeq1 14040	. . . . . . . . . . 11
25	24	oveq2d 6324	. . . . . . . . . 10
26		prodeq1 14040	. . . . . . . . . 10
27	25, 26	oveq12d 6326	. . . . . . . . 9
28	27	sumeq2ad 37740	. . . . . . . 8
29	23, 28	eqtrd 2505	. . . . . . 7
30	29	mpteq2dv 4483	. . . . . 6
31	20, 30	eqeq12d 2486	. . . . 5
32	31	ralbidv 2829	. . . 4
33		prodeq1 14040	. . . . . . . . 9
34	33	mpteq2dv 4483	. . . . . . . 8
35	34	oveq2d 6324	. . . . . . 7
36	35	fveq1d 5881	. . . . . 6
37		fveq2 5879	. . . . . . . . . 10
38	37	fveq1d 5881	. . . . . . . . 9
39	38	sumeq1d 13844	. . . . . . . 8
40		prodeq1 14040	. . . . . . . . . . 11
41	40	oveq2d 6324	. . . . . . . . . 10
42		prodeq1 14040	. . . . . . . . . 10
43	41, 42	oveq12d 6326	. . . . . . . . 9
44	43	sumeq2ad 37740	. . . . . . . 8
45	39, 44	eqtrd 2505	. . . . . . 7
46	45	mpteq2dv 4483	. . . . . 6
47	36, 46	eqeq12d 2486	. . . . 5
48	47	ralbidv 2829	. . . 4
49		prodeq1 14040	. . . . . . . . . 10
50	49	mpteq2dv 4483	. . . . . . . . 9
51		dvnprodlem3.f	. . . . . . . . . . 11
52	51	a1i 11	. . . . . . . . . 10
53	52	eqcomd 2477	. . . . . . . . 9
54	50, 53	eqtrd 2505	. . . . . . . 8
55	54	oveq2d 6324	. . . . . . 7
56	55	fveq1d 5881	. . . . . 6
57		fveq2 5879	. . . . . . . . . 10
58	57	fveq1d 5881	. . . . . . . . 9
59	58	sumeq1d 13844	. . . . . . . 8
60		prodeq1 14040	. . . . . . . . . . 11
61	60	oveq2d 6324	. . . . . . . . . 10
62		prodeq1 14040	. . . . . . . . . 10
63	61, 62	oveq12d 6326	. . . . . . . . 9
64	63	sumeq2ad 37740	. . . . . . . 8
65	59, 64	eqtrd 2505	. . . . . . 7
66	65	mpteq2dv 4483	. . . . . 6
67	56, 66	eqeq12d 2486	. . . . 5
68	67	ralbidv 2829	. . . 4
69		prod0 14074	. . . . . . . . . . . . 13
70	69	mpteq2i 4479	. . . . . . . . . . . 12
71	70	oveq2i 6319	. . . . . . . . . . 11
72	71	a1i 11	. . . . . . . . . 10
73		id 22	. . . . . . . . . 10
74	72, 73	fveq12d 5885	. . . . . . . . 9
75	74	adantl 473	. . . . . . . 8 $/\$
76		dvnprodlem3.s	. . . . . . . . . . 11
77		recnprss 22938	. . . . . . . . . . 11
78	76, 77	syl 17	. . . . . . . . . 10
79		1cnd 9677	. . . . . . . . . . . . . 14 $/\$
80		eqid 2471	. . . . . . . . . . . . . 14
81	79, 80	fmptd 6061	. . . . . . . . . . . . 13
82		1re 9660	. . . . . . . . . . . . . . . . 17
83	82	rgenw 2768	. . . . . . . . . . . . . . . 16
84		dmmptg 5339	. . . . . . . . . . . . . . . 16
85	83, 84	ax-mp 5	. . . . . . . . . . . . . . 15
86	85	a1i 11	. . . . . . . . . . . . . 14
87	86	feq2d 5725	. . . . . . . . . . . . 13
88	81, 87	mpbird 240	. . . . . . . . . . . 12
89		restsspw 15408	. . . . . . . . . . . . . . 15 ℂ_fld ↾_t
90		dvnprodlem3.x	. . . . . . . . . . . . . . 15 ℂ_fld ↾_t
91	89, 90	sseldi 3416	. . . . . . . . . . . . . 14
92		elpwi 3951	. . . . . . . . . . . . . 14
93	91, 92	syl 17	. . . . . . . . . . . . 13
94	86, 93	eqsstrd 3452	. . . . . . . . . . . 12
95	88, 94	jca 541	. . . . . . . . . . 11 $/\$
96		cnex 9638	. . . . . . . . . . . . 13
97	96	a1i 11	. . . . . . . . . . . 12
98		elpm2g 7506	. . . . . . . . . . . 12 $/\$ $/\$
99	97, 76, 98	syl2anc 673	. . . . . . . . . . 11 $/\$
100	95, 99	mpbird 240	. . . . . . . . . 10
101		dvn0 22957	. . . . . . . . . 10 $/\$
102	78, 100, 101	syl2anc 673	. . . . . . . . 9
103	102	adantr 472	. . . . . . . 8 $/\$
104		fveq2 5879	. . . . . . . . . . . . . . 15
105	104	adantl 473	. . . . . . . . . . . . . 14 $/\$
106		dvnprodlem3.d	. . . . . . . . . . . . . . . . . 18
107	106	a1i 11	. . . . . . . . . . . . . . . . 17
108		oveq2 6316	. . . . . . . . . . . . . . . . . . . . . 22
109		elmapfn 7512	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
110		fn0 5705	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
111	109, 110	sylib 201	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
112		elsn 3973	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
113	111, 112	sylibr 217	. . . . . . . . . . . . . . . . . . . . . . . . . 26
114	112	biimpi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
115		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
116		f0 5777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
117		ovex 6336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
118		0ex 4528	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
119	117, 118	elmap 7518	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
120	116, 119	mpbir 214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
121	120	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
122	115, 121	eqeltrd 2549	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
123	114, 122	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
124	113, 123	impbii 192	. . . . . . . . . . . . . . . . . . . . . . . . 25
125	124	ax-gen 1677	. . . . . . . . . . . . . . . . . . . . . . . 24
126		dfcleq 2465	. . . . . . . . . . . . . . . . . . . . . . . 24
127	125, 126	mpbir 214	. . . . . . . . . . . . . . . . . . . . . . 23
128	127	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
129	108, 128	eqtrd 2505	. . . . . . . . . . . . . . . . . . . . 21
130		rabeq 3024	. . . . . . . . . . . . . . . . . . . . 21
131	129, 130	syl 17	. . . . . . . . . . . . . . . . . . . 20
132		sumeq1 13832	. . . . . . . . . . . . . . . . . . . . . 22
133	132	eqeq1d 2473	. . . . . . . . . . . . . . . . . . . . 21
134	133	rabbidv 3022	. . . . . . . . . . . . . . . . . . . 20
135	131, 134	eqtrd 2505	. . . . . . . . . . . . . . . . . . 19
136	135	mpteq2dv 4483	. . . . . . . . . . . . . . . . . 18
137	136	adantl 473	. . . . . . . . . . . . . . . . 17 $/\$
138		0elpw 4570	. . . . . . . . . . . . . . . . . 18
139	138	a1i 11	. . . . . . . . . . . . . . . . 17
140		nn0ex 10899	. . . . . . . . . . . . . . . . . . 19
141	140	mptex 6152	. . . . . . . . . . . . . . . . . 18
142	141	a1i 11	. . . . . . . . . . . . . . . . 17
143	107, 137, 139, 142	fvmptd 5969	. . . . . . . . . . . . . . . 16
144		eqeq2 2482	. . . . . . . . . . . . . . . . . 18
145	144	rabbidv 3022	. . . . . . . . . . . . . . . . 17
146	145	adantl 473	. . . . . . . . . . . . . . . 16 $/\$
147		0nn0 10908	. . . . . . . . . . . . . . . . 17
148	147	a1i 11	. . . . . . . . . . . . . . . 16
149		p0ex 4588	. . . . . . . . . . . . . . . . . 18
150	149	rabex 4550	. . . . . . . . . . . . . . . . 17
151	150	a1i 11	. . . . . . . . . . . . . . . 16
152	143, 146, 148, 151	fvmptd 5969	. . . . . . . . . . . . . . 15
153	152	adantr 472	. . . . . . . . . . . . . 14 $/\$
154		snidg 3986	. . . . . . . . . . . . . . . . . . . . . 22
155	118, 154	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
156		eqid 2471	. . . . . . . . . . . . . . . . . . . . 21
157	155, 156	pm3.2i 462	. . . . . . . . . . . . . . . . . . . 20 $/\$
158		sum0 13864	. . . . . . . . . . . . . . . . . . . . . . 23
159	158	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
160	159	eqeq1d 2473	. . . . . . . . . . . . . . . . . . . . 21
161	160	elrab 3184	. . . . . . . . . . . . . . . . . . . 20 $/\$
162	157, 161	mpbir 214	. . . . . . . . . . . . . . . . . . 19
163	162	ne0ii 3729	. . . . . . . . . . . . . . . . . 18
164	163	neii 2645	. . . . . . . . . . . . . . . . 17
165		eqid 2471	. . . . . . . . . . . . . . . . . 18
166		rabrsn 4033	. . . . . . . . . . . . . . . . . 18 $\/$
167	165, 166	ax-mp 5	. . . . . . . . . . . . . . . . 17 $\/$
168	164, 167	mtpor 1661	. . . . . . . . . . . . . . . 16
169	168	a1i 11	. . . . . . . . . . . . . . 15 $/\$
170		iftrue 3878	. . . . . . . . . . . . . . . 16
171	170	adantl 473	. . . . . . . . . . . . . . 15 $/\$
172	169, 171	eqtr4d 2508	. . . . . . . . . . . . . 14 $/\$
173	105, 153, 172	3eqtrd 2509	. . . . . . . . . . . . 13 $/\$
174	173, 171	eqtrd 2505	. . . . . . . . . . . 12 $/\$
175	174	sumeq1d 13844	. . . . . . . . . . 11 $/\$
176		fveq2 5879	. . . . . . . . . . . . . . . . . 18
177		fac0 12500	. . . . . . . . . . . . . . . . . . 19
178	177	a1i 11	. . . . . . . . . . . . . . . . . 18
179	176, 178	eqtrd 2505	. . . . . . . . . . . . . . . . 17
180	179	oveq1d 6323	. . . . . . . . . . . . . . . 16
181		prod0 14074	. . . . . . . . . . . . . . . . . 18
182	181	oveq2i 6319	. . . . . . . . . . . . . . . . 17
183		1div1e1 10322	. . . . . . . . . . . . . . . . 17
184	182, 183	eqtri 2493	. . . . . . . . . . . . . . . 16
185	180, 184	syl6eq 2521	. . . . . . . . . . . . . . 15
186		prod0 14074	. . . . . . . . . . . . . . . 16
187	186	a1i 11	. . . . . . . . . . . . . . 15
188	185, 187	oveq12d 6326	. . . . . . . . . . . . . 14
189	188	ad2antlr 741	. . . . . . . . . . . . 13 $/\$ $/\$
190		1t1e1 10780	. . . . . . . . . . . . . 14
191	190	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
192	189, 191	eqtrd 2505	. . . . . . . . . . . 12 $/\$ $/\$
193	192	sumeq2dv 13846	. . . . . . . . . . 11 $/\$
194		ax-1cn 9615	. . . . . . . . . . . . 13
195		eqidd 2472	. . . . . . . . . . . . . 14
196	195	sumsn 13884	. . . . . . . . . . . . 13 $/\$
197	118, 194, 196	mp2an 686	. . . . . . . . . . . 12
198	197	a1i 11	. . . . . . . . . . 11 $/\$
199	175, 193, 198	3eqtrd 2509	. . . . . . . . . 10 $/\$
200	199	mpteq2dv 4483	. . . . . . . . 9 $/\$
201	200	eqcomd 2477	. . . . . . . 8 $/\$
202	75, 103, 201	3eqtrd 2509	. . . . . . 7 $/\$
203	202	a1d 25	. . . . . 6 $/\$
204	71	fveq1i 5880	. . . . . . . . 9
205	204	a1i 11	. . . . . . . 8 $/\$ $/\$
206	76	adantr 472	. . . . . . . . . 10 $/\$
207	206	adantr 472	. . . . . . . . 9 $/\$ $/\$
208	90	adantr 472	. . . . . . . . . 10 $/\$ ℂ_fld ↾_t
209	208	adantr 472	. . . . . . . . 9 $/\$ $/\$ ℂ_fld ↾_t
210	194	a1i 11	. . . . . . . . 9 $/\$ $/\$
211		elfznn0 11913	. . . . . . . . . . . . 13
212	211	adantl 473	. . . . . . . . . . . 12 $/\$
213		neqne 2651	. . . . . . . . . . . . 13
214	213	adantr 472	. . . . . . . . . . . 12 $/\$
215	212, 214	jca 541	. . . . . . . . . . 11 $/\$ $/\$
216		elnnne0 10907	. . . . . . . . . . 11 $/\$
217	215, 216	sylibr 217	. . . . . . . . . 10 $/\$
218	217	adantll 728	. . . . . . . . 9 $/\$ $/\$
219	207, 209, 210, 218	dvnmptconst 37913	. . . . . . . 8 $/\$ $/\$
220	143	ad2antrr 740	. . . . . . . . . . . 12 $/\$ $/\$
221		eqeq2 2482	. . . . . . . . . . . . . . . . 17
222	221	rabbidv 3022	. . . . . . . . . . . . . . . 16
223	222	adantl 473	. . . . . . . . . . . . . . 15 $/\$
224		eqidd 2472	. . . . . . . . . . . . . . . . . . . . . 22
225		id 22	. . . . . . . . . . . . . . . . . . . . . . 23
226	225	eqcomd 2477	. . . . . . . . . . . . . . . . . . . . . 22
227	158	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
228	224, 226, 227	3eqtrd 2509	. . . . . . . . . . . . . . . . . . . . 21
229	228	adantl 473	. . . . . . . . . . . . . . . . . . . 20 $/\$
230	229	adantll 728	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
231		simpll 768	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
232	230, 231	pm2.65da 586	. . . . . . . . . . . . . . . . . 18 $/\$
233	232	ralrimiva 2809	. . . . . . . . . . . . . . . . 17
234		rabeq0 3757	. . . . . . . . . . . . . . . . 17
235	233, 234	sylibr 217	. . . . . . . . . . . . . . . 16
236	235	adantr 472	. . . . . . . . . . . . . . 15 $/\$
237	223, 236	eqtrd 2505	. . . . . . . . . . . . . 14 $/\$
238	237	adantll 728	. . . . . . . . . . . . 13 $/\$ $/\$
239	238	adantlr 729	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
240	211	adantl 473	. . . . . . . . . . . 12 $/\$ $/\$
241	118	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$
242	220, 239, 240, 241	fvmptd 5969	. . . . . . . . . . 11 $/\$ $/\$
243	242	sumeq1d 13844	. . . . . . . . . 10 $/\$ $/\$
244		sum0 13864	. . . . . . . . . . 11
245	244	a1i 11	. . . . . . . . . 10 $/\$ $/\$
246	243, 245	eqtr2d 2506	. . . . . . . . 9 $/\$ $/\$
247	246	mpteq2dv 4483	. . . . . . . 8 $/\$ $/\$
248	205, 219, 247	3eqtrd 2509	. . . . . . 7 $/\$ $/\$
249	248	ex 441	. . . . . 6 $/\$
250	203, 249	pm2.61dan 808	. . . . 5
251	250	ralrimiv 2808	. . . 4
252		simpll 768	. . . . . . . 8 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$
253		fveq2 5879	. . . . . . . . . . . . . . . . 17
254	253	prodeq2ad 37769	. . . . . . . . . . . . . . . 16
255		fveq2 5879	. . . . . . . . . . . . . . . . . . 19
256	255	fveq1d 5881	. . . . . . . . . . . . . . . . . 18
257	256	cbvprodv 14047	. . . . . . . . . . . . . . . . 17
258	257	a1i 11	. . . . . . . . . . . . . . . 16
259	254, 258	eqtrd 2505	. . . . . . . . . . . . . . 15
260	259	cbvmptv 4488	. . . . . . . . . . . . . 14
261	260	oveq2i 6319	. . . . . . . . . . . . 13
262	261	fveq1i 5880	. . . . . . . . . . . 12
263		fveq2 5879	. . . . . . . . . . . . . . . . . . . 20
264	263	fveq2d 5883	. . . . . . . . . . . . . . . . . . 19
265	264	cbvprodv 14047	. . . . . . . . . . . . . . . . . 18
266	265	oveq2i 6319	. . . . . . . . . . . . . . . . 17
267	266	a1i 11	. . . . . . . . . . . . . . . 16
268		fveq2 5879	. . . . . . . . . . . . . . . . . 18
269	268	prodeq2ad 37769	. . . . . . . . . . . . . . . . 17
270	255	oveq2d 6324	. . . . . . . . . . . . . . . . . . . . 21
271	270, 263	fveq12d 5885	. . . . . . . . . . . . . . . . . . . 20
272	271	fveq1d 5881	. . . . . . . . . . . . . . . . . . 19
273	272	cbvprodv 14047	. . . . . . . . . . . . . . . . . 18
274	273	a1i 11	. . . . . . . . . . . . . . . . 17
275	269, 274	eqtrd 2505	. . . . . . . . . . . . . . . 16
276	267, 275	oveq12d 6326	. . . . . . . . . . . . . . 15
277	276	sumeq2ad 37740	. . . . . . . . . . . . . 14
278		fveq1 5878	. . . . . . . . . . . . . . . . . . . 20
279	278	fveq2d 5883	. . . . . . . . . . . . . . . . . . 19
280	279	prodeq2ad 37769	. . . . . . . . . . . . . . . . . 18
281	280	oveq2d 6324	. . . . . . . . . . . . . . . . 17
282	278	fveq2d 5883	. . . . . . . . . . . . . . . . . . 19
283	282	fveq1d 5881	. . . . . . . . . . . . . . . . . 18
284	283	prodeq2ad 37769	. . . . . . . . . . . . . . . . 17
285	281, 284	oveq12d 6326	. . . . . . . . . . . . . . . 16
286	285	cbvsumv 13839	. . . . . . . . . . . . . . 15
287	286	a1i 11	. . . . . . . . . . . . . 14
288	277, 287	eqtrd 2505	. . . . . . . . . . . . 13
289	288	cbvmptv 4488	. . . . . . . . . . . 12
290	262, 289	eqeq12i 2485	. . . . . . . . . . 11
291	290	ralbii 2823	. . . . . . . . . 10
292	291	biimpi 199	. . . . . . . . 9
293	292	ad2antlr 741	. . . . . . . 8 $/\$ $/\$ $\$ $/\$ $/\$
294		simpr 468	. . . . . . . 8 $/\$ $/\$ $\$ $/\$ $/\$
295	76	ad3antrrr 744	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ $/\$
296	90	ad3antrrr 744	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ $/\$ ℂ_fld ↾_t
297		dvnprodlem3.t	. . . . . . . . . 10
298	297	ad3antrrr 744	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ $/\$
299		simp-4l 784	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$