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 37823

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 13963	. . . . . . . . 9
2	1	mpteq2dv 4490	. . . . . . . 8
3	2	oveq2d 6306	. . . . . . 7
4	3	fveq1d 5867	. . . . . 6
5		fveq2 5865	. . . . . . . . . 10
6	5	fveq1d 5867	. . . . . . . . 9
7	6	sumeq1d 13767	. . . . . . . 8
8		prodeq1 13963	. . . . . . . . . . 11
9	8	oveq2d 6306	. . . . . . . . . 10
10		prodeq1 13963	. . . . . . . . . 10
11	9, 10	oveq12d 6308	. . . . . . . . 9
12	11	sumeq2ad 37644	. . . . . . . 8
13	7, 12	eqtrd 2485	. . . . . . 7
14	13	mpteq2dv 4490	. . . . . 6
15	4, 14	eqeq12d 2466	. . . . 5
16	15	ralbidv 2827	. . . 4
17		prodeq1 13963	. . . . . . . . 9
18	17	mpteq2dv 4490	. . . . . . . 8
19	18	oveq2d 6306	. . . . . . 7
20	19	fveq1d 5867	. . . . . 6
21		fveq2 5865	. . . . . . . . . 10
22	21	fveq1d 5867	. . . . . . . . 9
23	22	sumeq1d 13767	. . . . . . . 8
24		prodeq1 13963	. . . . . . . . . . 11
25	24	oveq2d 6306	. . . . . . . . . 10
26		prodeq1 13963	. . . . . . . . . 10
27	25, 26	oveq12d 6308	. . . . . . . . 9
28	27	sumeq2ad 37644	. . . . . . . 8
29	23, 28	eqtrd 2485	. . . . . . 7
30	29	mpteq2dv 4490	. . . . . 6
31	20, 30	eqeq12d 2466	. . . . 5
32	31	ralbidv 2827	. . . 4
33		prodeq1 13963	. . . . . . . . 9
34	33	mpteq2dv 4490	. . . . . . . 8
35	34	oveq2d 6306	. . . . . . 7
36	35	fveq1d 5867	. . . . . 6
37		fveq2 5865	. . . . . . . . . 10
38	37	fveq1d 5867	. . . . . . . . 9
39	38	sumeq1d 13767	. . . . . . . 8
40		prodeq1 13963	. . . . . . . . . . 11
41	40	oveq2d 6306	. . . . . . . . . 10
42		prodeq1 13963	. . . . . . . . . 10
43	41, 42	oveq12d 6308	. . . . . . . . 9
44	43	sumeq2ad 37644	. . . . . . . 8
45	39, 44	eqtrd 2485	. . . . . . 7
46	45	mpteq2dv 4490	. . . . . 6
47	36, 46	eqeq12d 2466	. . . . 5
48	47	ralbidv 2827	. . . 4
49		prodeq1 13963	. . . . . . . . . 10
50	49	mpteq2dv 4490	. . . . . . . . 9
51		dvnprodlem3.f	. . . . . . . . . . 11
52	51	a1i 11	. . . . . . . . . 10
53	52	eqcomd 2457	. . . . . . . . 9
54	50, 53	eqtrd 2485	. . . . . . . 8
55	54	oveq2d 6306	. . . . . . 7
56	55	fveq1d 5867	. . . . . 6
57		fveq2 5865	. . . . . . . . . 10
58	57	fveq1d 5867	. . . . . . . . 9
59	58	sumeq1d 13767	. . . . . . . 8
60		prodeq1 13963	. . . . . . . . . . 11
61	60	oveq2d 6306	. . . . . . . . . 10
62		prodeq1 13963	. . . . . . . . . 10
63	61, 62	oveq12d 6308	. . . . . . . . 9
64	63	sumeq2ad 37644	. . . . . . . 8
65	59, 64	eqtrd 2485	. . . . . . 7
66	65	mpteq2dv 4490	. . . . . 6
67	56, 66	eqeq12d 2466	. . . . 5
68	67	ralbidv 2827	. . . 4
69		prod0 13997	. . . . . . . . . . . . 13
70	69	mpteq2i 4486	. . . . . . . . . . . 12
71	70	oveq2i 6301	. . . . . . . . . . 11
72	71	a1i 11	. . . . . . . . . 10
73		id 22	. . . . . . . . . 10
74	72, 73	fveq12d 5871	. . . . . . . . 9
75	74	adantl 468	. . . . . . . 8 $/\$
76		dvnprodlem3.s	. . . . . . . . . . 11
77		recnprss 22859	. . . . . . . . . . 11
78	76, 77	syl 17	. . . . . . . . . 10
79		1cnd 9659	. . . . . . . . . . . . . 14 $/\$
80		eqid 2451	. . . . . . . . . . . . . 14
81	79, 80	fmptd 6046	. . . . . . . . . . . . 13
82		1re 9642	. . . . . . . . . . . . . . . . 17
83	82	rgenw 2749	. . . . . . . . . . . . . . . 16
84		dmmptg 5332	. . . . . . . . . . . . . . . 16
85	83, 84	ax-mp 5	. . . . . . . . . . . . . . 15
86	85	a1i 11	. . . . . . . . . . . . . 14
87	86	feq2d 5715	. . . . . . . . . . . . 13
88	81, 87	mpbird 236	. . . . . . . . . . . 12
89		restsspw 15330	. . . . . . . . . . . . . . 15 ℂ_fld ↾_t
90		dvnprodlem3.x	. . . . . . . . . . . . . . 15 ℂ_fld ↾_t
91	89, 90	sseldi 3430	. . . . . . . . . . . . . 14
92		elpwi 3960	. . . . . . . . . . . . . 14
93	91, 92	syl 17	. . . . . . . . . . . . 13
94	86, 93	eqsstrd 3466	. . . . . . . . . . . 12
95	88, 94	jca 535	. . . . . . . . . . 11 $/\$
96		cnex 9620	. . . . . . . . . . . . 13
97	96	a1i 11	. . . . . . . . . . . 12
98		elpm2g 7488	. . . . . . . . . . . 12 $/\$ $/\$
99	97, 76, 98	syl2anc 667	. . . . . . . . . . 11 $/\$
100	95, 99	mpbird 236	. . . . . . . . . 10
101		dvn0 22878	. . . . . . . . . 10 $/\$
102	78, 100, 101	syl2anc 667	. . . . . . . . 9
103	102	adantr 467	. . . . . . . 8 $/\$
104		fveq2 5865	. . . . . . . . . . . . . . 15
105	104	adantl 468	. . . . . . . . . . . . . 14 $/\$
106		dvnprodlem3.d	. . . . . . . . . . . . . . . . . 18
107	106	a1i 11	. . . . . . . . . . . . . . . . 17
108		oveq2 6298	. . . . . . . . . . . . . . . . . . . . . 22
109		elmapfn 7494	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
110		fn0 5695	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
111	109, 110	sylib 200	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
112		elsn 3982	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
113	111, 112	sylibr 216	. . . . . . . . . . . . . . . . . . . . . . . . . 26
114	112	biimpi 198	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
115		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
116		f0 5764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
117		ovex 6318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
118		0ex 4535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
119	117, 118	elmap 7500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
120	116, 119	mpbir 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
121	120	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
122	115, 121	eqeltrd 2529	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
123	114, 122	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
124	113, 123	impbii 191	. . . . . . . . . . . . . . . . . . . . . . . . 25
125	124	ax-gen 1669	. . . . . . . . . . . . . . . . . . . . . . . 24
126		dfcleq 2445	. . . . . . . . . . . . . . . . . . . . . . . 24
127	125, 126	mpbir 213	. . . . . . . . . . . . . . . . . . . . . . 23
128	127	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
129	108, 128	eqtrd 2485	. . . . . . . . . . . . . . . . . . . . 21
130		rabeq 3038	. . . . . . . . . . . . . . . . . . . . 21
131	129, 130	syl 17	. . . . . . . . . . . . . . . . . . . 20
132		sumeq1 13755	. . . . . . . . . . . . . . . . . . . . . 22
133	132	eqeq1d 2453	. . . . . . . . . . . . . . . . . . . . 21
134	133	rabbidv 3036	. . . . . . . . . . . . . . . . . . . 20
135	131, 134	eqtrd 2485	. . . . . . . . . . . . . . . . . . 19
136	135	mpteq2dv 4490	. . . . . . . . . . . . . . . . . 18
137	136	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$
138		0elpw 4572	. . . . . . . . . . . . . . . . . 18
139	138	a1i 11	. . . . . . . . . . . . . . . . 17
140		nn0ex 10875	. . . . . . . . . . . . . . . . . . 19
141	140	mptex 6136	. . . . . . . . . . . . . . . . . 18
142	141	a1i 11	. . . . . . . . . . . . . . . . 17
143	107, 137, 139, 142	fvmptd 5954	. . . . . . . . . . . . . . . 16
144		eqeq2 2462	. . . . . . . . . . . . . . . . . 18
145	144	rabbidv 3036	. . . . . . . . . . . . . . . . 17
146	145	adantl 468	. . . . . . . . . . . . . . . 16 $/\$
147		0nn0 10884	. . . . . . . . . . . . . . . . 17
148	147	a1i 11	. . . . . . . . . . . . . . . 16
149		p0ex 4590	. . . . . . . . . . . . . . . . . 18
150	149	rabex 4554	. . . . . . . . . . . . . . . . 17
151	150	a1i 11	. . . . . . . . . . . . . . . 16
152	143, 146, 148, 151	fvmptd 5954	. . . . . . . . . . . . . . 15
153	152	adantr 467	. . . . . . . . . . . . . 14 $/\$
154		snidg 3994	. . . . . . . . . . . . . . . . . . . . . 22
155	118, 154	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
156		eqid 2451	. . . . . . . . . . . . . . . . . . . . 21
157	155, 156	pm3.2i 457	. . . . . . . . . . . . . . . . . . . 20 $/\$
158		sum0 13787	. . . . . . . . . . . . . . . . . . . . . . 23
159	158	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
160	159	eqeq1d 2453	. . . . . . . . . . . . . . . . . . . . 21
161	160	elrab 3196	. . . . . . . . . . . . . . . . . . . 20 $/\$
162	157, 161	mpbir 213	. . . . . . . . . . . . . . . . . . 19
163	162	ne0ii 3738	. . . . . . . . . . . . . . . . . 18
164	163	neii 2626	. . . . . . . . . . . . . . . . 17
165		eqid 2451	. . . . . . . . . . . . . . . . . 18
166		rabrsn 4042	. . . . . . . . . . . . . . . . . 18 $\/$
167	165, 166	ax-mp 5	. . . . . . . . . . . . . . . . 17 $\/$
168	164, 167	mtpor 1653	. . . . . . . . . . . . . . . 16
169	168	a1i 11	. . . . . . . . . . . . . . 15 $/\$
170		iftrue 3887	. . . . . . . . . . . . . . . 16
171	170	adantl 468	. . . . . . . . . . . . . . 15 $/\$
172	169, 171	eqtr4d 2488	. . . . . . . . . . . . . 14 $/\$
173	105, 153, 172	3eqtrd 2489	. . . . . . . . . . . . 13 $/\$
174	173, 171	eqtrd 2485	. . . . . . . . . . . 12 $/\$
175	174	sumeq1d 13767	. . . . . . . . . . 11 $/\$
176		fveq2 5865	. . . . . . . . . . . . . . . . . 18
177		fac0 12462	. . . . . . . . . . . . . . . . . . 19
178	177	a1i 11	. . . . . . . . . . . . . . . . . 18
179	176, 178	eqtrd 2485	. . . . . . . . . . . . . . . . 17
180	179	oveq1d 6305	. . . . . . . . . . . . . . . 16
181		prod0 13997	. . . . . . . . . . . . . . . . . 18
182	181	oveq2i 6301	. . . . . . . . . . . . . . . . 17
183		1div1e1 10300	. . . . . . . . . . . . . . . . 17
184	182, 183	eqtri 2473	. . . . . . . . . . . . . . . 16
185	180, 184	syl6eq 2501	. . . . . . . . . . . . . . 15
186		prod0 13997	. . . . . . . . . . . . . . . 16
187	186	a1i 11	. . . . . . . . . . . . . . 15
188	185, 187	oveq12d 6308	. . . . . . . . . . . . . 14
189	188	ad2antlr 733	. . . . . . . . . . . . 13 $/\$ $/\$
190		1t1e1 10757	. . . . . . . . . . . . . 14
191	190	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
192	189, 191	eqtrd 2485	. . . . . . . . . . . 12 $/\$ $/\$
193	192	sumeq2dv 13769	. . . . . . . . . . 11 $/\$
194		ax-1cn 9597	. . . . . . . . . . . . 13
195		eqidd 2452	. . . . . . . . . . . . . 14
196	195	sumsn 13807	. . . . . . . . . . . . 13 $/\$
197	118, 194, 196	mp2an 678	. . . . . . . . . . . 12
198	197	a1i 11	. . . . . . . . . . 11 $/\$
199	175, 193, 198	3eqtrd 2489	. . . . . . . . . 10 $/\$
200	199	mpteq2dv 4490	. . . . . . . . 9 $/\$
201	200	eqcomd 2457	. . . . . . . 8 $/\$
202	75, 103, 201	3eqtrd 2489	. . . . . . 7 $/\$
203	202	a1d 26	. . . . . 6 $/\$
204	71	fveq1i 5866	. . . . . . . . 9
205	204	a1i 11	. . . . . . . 8 $/\$ $/\$
206	76	adantr 467	. . . . . . . . . 10 $/\$
207	206	adantr 467	. . . . . . . . 9 $/\$ $/\$
208	90	adantr 467	. . . . . . . . . 10 $/\$ ℂ_fld ↾_t
209	208	adantr 467	. . . . . . . . 9 $/\$ $/\$ ℂ_fld ↾_t
210	194	a1i 11	. . . . . . . . 9 $/\$ $/\$
211		elfznn0 11887	. . . . . . . . . . . . 13
212	211	adantl 468	. . . . . . . . . . . 12 $/\$
213		neqne 37374	. . . . . . . . . . . . 13
214	213	adantr 467	. . . . . . . . . . . 12 $/\$
215	212, 214	jca 535	. . . . . . . . . . 11 $/\$ $/\$
216		elnnne0 10883	. . . . . . . . . . 11 $/\$
217	215, 216	sylibr 216	. . . . . . . . . 10 $/\$
218	217	adantll 720	. . . . . . . . 9 $/\$ $/\$
219	207, 209, 210, 218	dvnmptconst 37816	. . . . . . . 8 $/\$ $/\$
220	143	ad2antrr 732	. . . . . . . . . . . 12 $/\$ $/\$
221		eqeq2 2462	. . . . . . . . . . . . . . . . 17
222	221	rabbidv 3036	. . . . . . . . . . . . . . . 16
223	222	adantl 468	. . . . . . . . . . . . . . 15 $/\$
224		eqidd 2452	. . . . . . . . . . . . . . . . . . . . . 22
225		id 22	. . . . . . . . . . . . . . . . . . . . . . 23
226	225	eqcomd 2457	. . . . . . . . . . . . . . . . . . . . . 22
227	158	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
228	224, 226, 227	3eqtrd 2489	. . . . . . . . . . . . . . . . . . . . 21
229	228	adantl 468	. . . . . . . . . . . . . . . . . . . 20 $/\$
230	229	adantll 720	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
231		simpll 760	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
232	230, 231	pm2.65da 580	. . . . . . . . . . . . . . . . . 18 $/\$
233	232	ralrimiva 2802	. . . . . . . . . . . . . . . . 17
234		rabeq0 3754	. . . . . . . . . . . . . . . . 17
235	233, 234	sylibr 216	. . . . . . . . . . . . . . . 16
236	235	adantr 467	. . . . . . . . . . . . . . 15 $/\$
237	223, 236	eqtrd 2485	. . . . . . . . . . . . . 14 $/\$
238	237	adantll 720	. . . . . . . . . . . . 13 $/\$ $/\$
239	238	adantlr 721	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
240	211	adantl 468	. . . . . . . . . . . 12 $/\$ $/\$
241	118	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$
242	220, 239, 240, 241	fvmptd 5954	. . . . . . . . . . 11 $/\$ $/\$
243	242	sumeq1d 13767	. . . . . . . . . 10 $/\$ $/\$
244		sum0 13787	. . . . . . . . . . 11
245	244	a1i 11	. . . . . . . . . 10 $/\$ $/\$
246	243, 245	eqtr2d 2486	. . . . . . . . 9 $/\$ $/\$
247	246	mpteq2dv 4490	. . . . . . . 8 $/\$ $/\$
248	205, 219, 247	3eqtrd 2489	. . . . . . 7 $/\$ $/\$
249	248	ex 436	. . . . . 6 $/\$
250	203, 249	pm2.61dan 800	. . . . 5
251	250	ralrimiv 2800	. . . 4
252		simpll 760	. . . . . . . 8 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$
253		fveq2 5865	. . . . . . . . . . . . . . . . 17
254	253	prodeq2ad 37672	. . . . . . . . . . . . . . . 16
255		fveq2 5865	. . . . . . . . . . . . . . . . . . 19
256	255	fveq1d 5867	. . . . . . . . . . . . . . . . . 18
257	256	cbvprodv 13970	. . . . . . . . . . . . . . . . 17
258	257	a1i 11	. . . . . . . . . . . . . . . 16
259	254, 258	eqtrd 2485	. . . . . . . . . . . . . . 15
260	259	cbvmptv 4495	. . . . . . . . . . . . . 14
261	260	oveq2i 6301	. . . . . . . . . . . . 13
262	261	fveq1i 5866	. . . . . . . . . . . 12
263		fveq2 5865	. . . . . . . . . . . . . . . . . . . 20
264	263	fveq2d 5869	. . . . . . . . . . . . . . . . . . 19
265	264	cbvprodv 13970	. . . . . . . . . . . . . . . . . 18
266	265	oveq2i 6301	. . . . . . . . . . . . . . . . 17
267	266	a1i 11	. . . . . . . . . . . . . . . 16
268		fveq2 5865	. . . . . . . . . . . . . . . . . 18
269	268	prodeq2ad 37672	. . . . . . . . . . . . . . . . 17
270	255	oveq2d 6306	. . . . . . . . . . . . . . . . . . . . 21
271	270, 263	fveq12d 5871	. . . . . . . . . . . . . . . . . . . 20
272	271	fveq1d 5867	. . . . . . . . . . . . . . . . . . 19
273	272	cbvprodv 13970	. . . . . . . . . . . . . . . . . 18
274	273	a1i 11	. . . . . . . . . . . . . . . . 17
275	269, 274	eqtrd 2485	. . . . . . . . . . . . . . . 16
276	267, 275	oveq12d 6308	. . . . . . . . . . . . . . 15
277	276	sumeq2ad 37644	. . . . . . . . . . . . . 14
278		fveq1 5864	. . . . . . . . . . . . . . . . . . . 20
279	278	fveq2d 5869	. . . . . . . . . . . . . . . . . . 19
280	279	prodeq2ad 37672	. . . . . . . . . . . . . . . . . 18
281	280	oveq2d 6306	. . . . . . . . . . . . . . . . 17
282	278	fveq2d 5869	. . . . . . . . . . . . . . . . . . 19
283	282	fveq1d 5867	. . . . . . . . . . . . . . . . . 18
284	283	prodeq2ad 37672	. . . . . . . . . . . . . . . . 17
285	281, 284	oveq12d 6308	. . . . . . . . . . . . . . . 16
286	285	cbvsumv 13762	. . . . . . . . . . . . . . 15
287	286	a1i 11	. . . . . . . . . . . . . 14
288	277, 287	eqtrd 2485	. . . . . . . . . . . . 13
289	288	cbvmptv 4495	. . . . . . . . . . . 12
290	262, 289	eqeq12i 2465	. . . . . . . . . . 11
291	290	ralbii 2819	. . . . . . . . . 10
292	291	biimpi 198	. . . . . . . . 9
293	292	ad2antlr 733	. . . . . . . 8 $/\$ $/\$ $\$ $/\$ $/\$
294		simpr 463	. . . . . . . 8 $/\$ $/\$ $\$ $/\$ $/\$
295	76	ad3antrrr 736	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ $/\$
296	90	ad3antrrr 736	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ $/\$ ℂ_fld ↾_t
297		dvnprodlem3.t	. . . . . . . . . 10
298	297	ad3antrrr 736	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ $/\$
299		simp-4l 776	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$