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 40163

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 14639	. . . . . . . . 9
2	1	mpteq2dv 4745	. . . . . . . 8
3	2	oveq2d 6666	. . . . . . 7
4	3	fveq1d 6193	. . . . . 6
5		fveq2 6191	. . . . . . . . . 10
6	5	fveq1d 6193	. . . . . . . . 9
7	6	sumeq1d 14431	. . . . . . . 8
8		prodeq1 14639	. . . . . . . . . . 11
9	8	oveq2d 6666	. . . . . . . . . 10
10		prodeq1 14639	. . . . . . . . . 10
11	9, 10	oveq12d 6668	. . . . . . . . 9
12	11	sumeq2ad 14434	. . . . . . . 8
13	7, 12	eqtrd 2656	. . . . . . 7
14	13	mpteq2dv 4745	. . . . . 6
15	4, 14	eqeq12d 2637	. . . . 5
16	15	ralbidv 2986	. . . 4
17		prodeq1 14639	. . . . . . . . 9
18	17	mpteq2dv 4745	. . . . . . . 8
19	18	oveq2d 6666	. . . . . . 7
20	19	fveq1d 6193	. . . . . 6
21		fveq2 6191	. . . . . . . . . 10
22	21	fveq1d 6193	. . . . . . . . 9
23	22	sumeq1d 14431	. . . . . . . 8
24		prodeq1 14639	. . . . . . . . . . 11
25	24	oveq2d 6666	. . . . . . . . . 10
26		prodeq1 14639	. . . . . . . . . 10
27	25, 26	oveq12d 6668	. . . . . . . . 9
28	27	sumeq2ad 14434	. . . . . . . 8
29	23, 28	eqtrd 2656	. . . . . . 7
30	29	mpteq2dv 4745	. . . . . 6
31	20, 30	eqeq12d 2637	. . . . 5
32	31	ralbidv 2986	. . . 4
33		prodeq1 14639	. . . . . . . . 9
34	33	mpteq2dv 4745	. . . . . . . 8
35	34	oveq2d 6666	. . . . . . 7
36	35	fveq1d 6193	. . . . . 6
37		fveq2 6191	. . . . . . . . . 10
38	37	fveq1d 6193	. . . . . . . . 9
39	38	sumeq1d 14431	. . . . . . . 8
40		prodeq1 14639	. . . . . . . . . . 11
41	40	oveq2d 6666	. . . . . . . . . 10
42		prodeq1 14639	. . . . . . . . . 10
43	41, 42	oveq12d 6668	. . . . . . . . 9
44	43	sumeq2ad 14434	. . . . . . . 8
45	39, 44	eqtrd 2656	. . . . . . 7
46	45	mpteq2dv 4745	. . . . . 6
47	36, 46	eqeq12d 2637	. . . . 5
48	47	ralbidv 2986	. . . 4
49		prodeq1 14639	. . . . . . . . . 10
50	49	mpteq2dv 4745	. . . . . . . . 9
51		dvnprodlem3.f	. . . . . . . . . . 11
52	51	a1i 11	. . . . . . . . . 10
53	52	eqcomd 2628	. . . . . . . . 9
54	50, 53	eqtrd 2656	. . . . . . . 8
55	54	oveq2d 6666	. . . . . . 7
56	55	fveq1d 6193	. . . . . 6
57		fveq2 6191	. . . . . . . . . 10
58	57	fveq1d 6193	. . . . . . . . 9
59	58	sumeq1d 14431	. . . . . . . 8
60		prodeq1 14639	. . . . . . . . . . 11
61	60	oveq2d 6666	. . . . . . . . . 10
62		prodeq1 14639	. . . . . . . . . 10
63	61, 62	oveq12d 6668	. . . . . . . . 9
64	63	sumeq2ad 14434	. . . . . . . 8
65	59, 64	eqtrd 2656	. . . . . . 7
66	65	mpteq2dv 4745	. . . . . 6
67	56, 66	eqeq12d 2637	. . . . 5
68	67	ralbidv 2986	. . . 4
69		prod0 14673	. . . . . . . . . . . . 13
70	69	mpteq2i 4741	. . . . . . . . . . . 12
71	70	oveq2i 6661	. . . . . . . . . . 11
72	71	a1i 11	. . . . . . . . . 10
73		id 22	. . . . . . . . . 10
74	72, 73	fveq12d 6197	. . . . . . . . 9
75	74	adantl 482	. . . . . . . 8 $/\$
76		dvnprodlem3.s	. . . . . . . . . . 11
77		recnprss 23668	. . . . . . . . . . 11
78	76, 77	syl 17	. . . . . . . . . 10
79		1cnd 10056	. . . . . . . . . . . . . 14 $/\$
80		eqid 2622	. . . . . . . . . . . . . 14
81	79, 80	fmptd 6385	. . . . . . . . . . . . 13
82		1re 10039	. . . . . . . . . . . . . . . . 17
83	82	rgenw 2924	. . . . . . . . . . . . . . . 16
84		dmmptg 5632	. . . . . . . . . . . . . . . 16
85	83, 84	ax-mp 5	. . . . . . . . . . . . . . 15
86	85	a1i 11	. . . . . . . . . . . . . 14
87	86	feq2d 6031	. . . . . . . . . . . . 13
88	81, 87	mpbird 247	. . . . . . . . . . . 12
89		restsspw 16092	. . . . . . . . . . . . . . 15 ℂ_fld ↾_t
90		dvnprodlem3.x	. . . . . . . . . . . . . . 15 ℂ_fld ↾_t
91	89, 90	sseldi 3601	. . . . . . . . . . . . . 14
92		elpwi 4168	. . . . . . . . . . . . . 14
93	91, 92	syl 17	. . . . . . . . . . . . 13
94	86, 93	eqsstrd 3639	. . . . . . . . . . . 12
95	88, 94	jca 554	. . . . . . . . . . 11 $/\$
96		cnex 10017	. . . . . . . . . . . . 13
97	96	a1i 11	. . . . . . . . . . . 12
98		elpm2g 7874	. . . . . . . . . . . 12 $/\$ $/\$
99	97, 76, 98	syl2anc 693	. . . . . . . . . . 11 $/\$
100	95, 99	mpbird 247	. . . . . . . . . 10
101		dvn0 23687	. . . . . . . . . 10 $/\$
102	78, 100, 101	syl2anc 693	. . . . . . . . 9
103	102	adantr 481	. . . . . . . 8 $/\$
104		fveq2 6191	. . . . . . . . . . . . . . 15
105	104	adantl 482	. . . . . . . . . . . . . 14 $/\$
106		dvnprodlem3.d	. . . . . . . . . . . . . . . . . 18
107	106	a1i 11	. . . . . . . . . . . . . . . . 17
108		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . 22
109		elmapfn 7880	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
110		fn0 6011	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
111	109, 110	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
112		velsn 4193	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
113	111, 112	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . 26
114	112	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
115		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
116		f0 6086	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
117		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
118		0ex 4790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
119	117, 118	elmap 7886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
120	116, 119	mpbir 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
121	120	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
122	115, 121	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
123	114, 122	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
124	113, 123	impbii 199	. . . . . . . . . . . . . . . . . . . . . . . . 25
125	124	ax-gen 1722	. . . . . . . . . . . . . . . . . . . . . . . 24
126		dfcleq 2616	. . . . . . . . . . . . . . . . . . . . . . . 24
127	125, 126	mpbir 221	. . . . . . . . . . . . . . . . . . . . . . 23
128	127	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
129	108, 128	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21
130		rabeq 3192	. . . . . . . . . . . . . . . . . . . . 21
131	129, 130	syl 17	. . . . . . . . . . . . . . . . . . . 20
132		sumeq1 14419	. . . . . . . . . . . . . . . . . . . . . 22
133	132	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . 21
134	133	rabbidv 3189	. . . . . . . . . . . . . . . . . . . 20
135	131, 134	eqtrd 2656	. . . . . . . . . . . . . . . . . . 19
136	135	mpteq2dv 4745	. . . . . . . . . . . . . . . . . 18
137	136	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$
138		0elpw 4834	. . . . . . . . . . . . . . . . . 18
139	138	a1i 11	. . . . . . . . . . . . . . . . 17
140		nn0ex 11298	. . . . . . . . . . . . . . . . . . 19
141	140	mptex 6486	. . . . . . . . . . . . . . . . . 18
142	141	a1i 11	. . . . . . . . . . . . . . . . 17
143	107, 137, 139, 142	fvmptd 6288	. . . . . . . . . . . . . . . 16
144		eqeq2 2633	. . . . . . . . . . . . . . . . . 18
145	144	rabbidv 3189	. . . . . . . . . . . . . . . . 17
146	145	adantl 482	. . . . . . . . . . . . . . . 16 $/\$
147		0nn0 11307	. . . . . . . . . . . . . . . . 17
148	147	a1i 11	. . . . . . . . . . . . . . . 16
149		p0ex 4853	. . . . . . . . . . . . . . . . . 18
150	149	rabex 4813	. . . . . . . . . . . . . . . . 17
151	150	a1i 11	. . . . . . . . . . . . . . . 16
152	143, 146, 148, 151	fvmptd 6288	. . . . . . . . . . . . . . 15
153	152	adantr 481	. . . . . . . . . . . . . 14 $/\$
154		snidg 4206	. . . . . . . . . . . . . . . . . . . . 21
155	118, 154	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
156		eqid 2622	. . . . . . . . . . . . . . . . . . . 20
157	155, 156	pm3.2i 471	. . . . . . . . . . . . . . . . . . 19 $/\$
158		sum0 14452	. . . . . . . . . . . . . . . . . . . . . 22
159	158	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
160	159	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . 20
161	160	elrab 3363	. . . . . . . . . . . . . . . . . . 19 $/\$
162	157, 161	mpbir 221	. . . . . . . . . . . . . . . . . 18
163	162	n0ii 3922	. . . . . . . . . . . . . . . . 17
164		eqid 2622	. . . . . . . . . . . . . . . . . 18
165		rabrsn 4259	. . . . . . . . . . . . . . . . . 18 $\/$
166	164, 165	ax-mp 5	. . . . . . . . . . . . . . . . 17 $\/$
167	163, 166	mtpor 1695	. . . . . . . . . . . . . . . 16
168	167	a1i 11	. . . . . . . . . . . . . . 15 $/\$
169		iftrue 4092	. . . . . . . . . . . . . . . 16
170	169	adantl 482	. . . . . . . . . . . . . . 15 $/\$
171	168, 170	eqtr4d 2659	. . . . . . . . . . . . . 14 $/\$
172	105, 153, 171	3eqtrd 2660	. . . . . . . . . . . . 13 $/\$
173	172, 170	eqtrd 2656	. . . . . . . . . . . 12 $/\$
174	173	sumeq1d 14431	. . . . . . . . . . 11 $/\$
175		fveq2 6191	. . . . . . . . . . . . . . . . . 18
176		fac0 13063	. . . . . . . . . . . . . . . . . . 19
177	176	a1i 11	. . . . . . . . . . . . . . . . . 18
178	175, 177	eqtrd 2656	. . . . . . . . . . . . . . . . 17
179	178	oveq1d 6665	. . . . . . . . . . . . . . . 16
180		prod0 14673	. . . . . . . . . . . . . . . . . 18
181	180	oveq2i 6661	. . . . . . . . . . . . . . . . 17
182		1div1e1 10717	. . . . . . . . . . . . . . . . 17
183	181, 182	eqtri 2644	. . . . . . . . . . . . . . . 16
184	179, 183	syl6eq 2672	. . . . . . . . . . . . . . 15
185		prod0 14673	. . . . . . . . . . . . . . . 16
186	185	a1i 11	. . . . . . . . . . . . . . 15
187	184, 186	oveq12d 6668	. . . . . . . . . . . . . 14
188	187	ad2antlr 763	. . . . . . . . . . . . 13 $/\$ $/\$
189		1t1e1 11175	. . . . . . . . . . . . . 14
190	189	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
191	188, 190	eqtrd 2656	. . . . . . . . . . . 12 $/\$ $/\$
192	191	sumeq2dv 14433	. . . . . . . . . . 11 $/\$
193		ax-1cn 9994	. . . . . . . . . . . . 13
194		eqidd 2623	. . . . . . . . . . . . . 14
195	194	sumsn 14475	. . . . . . . . . . . . 13 $/\$
196	118, 193, 195	mp2an 708	. . . . . . . . . . . 12
197	196	a1i 11	. . . . . . . . . . 11 $/\$
198	174, 192, 197	3eqtrd 2660	. . . . . . . . . 10 $/\$
199	198	mpteq2dv 4745	. . . . . . . . 9 $/\$
200	199	eqcomd 2628	. . . . . . . 8 $/\$
201	75, 103, 200	3eqtrd 2660	. . . . . . 7 $/\$
202	201	a1d 25	. . . . . 6 $/\$
203	71	fveq1i 6192	. . . . . . . . 9
204	203	a1i 11	. . . . . . . 8 $/\$ $/\$
205	76	adantr 481	. . . . . . . . . 10 $/\$
206	205	adantr 481	. . . . . . . . 9 $/\$ $/\$
207	90	adantr 481	. . . . . . . . . 10 $/\$ ℂ_fld ↾_t
208	207	adantr 481	. . . . . . . . 9 $/\$ $/\$ ℂ_fld ↾_t
209	193	a1i 11	. . . . . . . . 9 $/\$ $/\$
210		elfznn0 12433	. . . . . . . . . . . . 13
211	210	adantl 482	. . . . . . . . . . . 12 $/\$
212		neqne 2802	. . . . . . . . . . . . 13
213	212	adantr 481	. . . . . . . . . . . 12 $/\$
214	211, 213	jca 554	. . . . . . . . . . 11 $/\$ $/\$
215		elnnne0 11306	. . . . . . . . . . 11 $/\$
216	214, 215	sylibr 224	. . . . . . . . . 10 $/\$
217	216	adantll 750	. . . . . . . . 9 $/\$ $/\$
218	206, 208, 209, 217	dvnmptconst 40156	. . . . . . . 8 $/\$ $/\$
219	143	ad2antrr 762	. . . . . . . . . . . 12 $/\$ $/\$
220		eqeq2 2633	. . . . . . . . . . . . . . . . 17
221	220	rabbidv 3189	. . . . . . . . . . . . . . . 16
222	221	adantl 482	. . . . . . . . . . . . . . 15 $/\$
223		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . 22
224		id 22	. . . . . . . . . . . . . . . . . . . . . . 23
225	224	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . 22
226	158	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
227	223, 225, 226	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . 21
228	227	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$
229	228	adantll 750	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
230		simpll 790	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
231	229, 230	pm2.65da 600	. . . . . . . . . . . . . . . . . 18 $/\$
232	231	ralrimiva 2966	. . . . . . . . . . . . . . . . 17
233		rabeq0 3957	. . . . . . . . . . . . . . . . 17
234	232, 233	sylibr 224	. . . . . . . . . . . . . . . 16
235	234	adantr 481	. . . . . . . . . . . . . . 15 $/\$
236	222, 235	eqtrd 2656	. . . . . . . . . . . . . 14 $/\$
237	236	adantll 750	. . . . . . . . . . . . 13 $/\$ $/\$
238	237	adantlr 751	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
239	210	adantl 482	. . . . . . . . . . . 12 $/\$ $/\$
240	118	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$
241	219, 238, 239, 240	fvmptd 6288	. . . . . . . . . . 11 $/\$ $/\$
242	241	sumeq1d 14431	. . . . . . . . . 10 $/\$ $/\$
243		sum0 14452	. . . . . . . . . . 11
244	243	a1i 11	. . . . . . . . . 10 $/\$ $/\$
245	242, 244	eqtr2d 2657	. . . . . . . . 9 $/\$ $/\$
246	245	mpteq2dv 4745	. . . . . . . 8 $/\$ $/\$
247	204, 218, 246	3eqtrd 2660	. . . . . . 7 $/\$ $/\$
248	247	ex 450	. . . . . 6 $/\$
249	202, 248	pm2.61dan 832	. . . . 5
250	249	ralrimiv 2965	. . . 4
251		simpll 790	. . . . . . . 8 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$
252		fveq2 6191	. . . . . . . . . . . . . . . . 17
253	252	prodeq2ad 39824	. . . . . . . . . . . . . . . 16
254		fveq2 6191	. . . . . . . . . . . . . . . . . . 19
255	254	fveq1d 6193	. . . . . . . . . . . . . . . . . 18
256	255	cbvprodv 14646	. . . . . . . . . . . . . . . . 17
257	256	a1i 11	. . . . . . . . . . . . . . . 16
258	253, 257	eqtrd 2656	. . . . . . . . . . . . . . 15
259	258	cbvmptv 4750	. . . . . . . . . . . . . 14
260	259	oveq2i 6661	. . . . . . . . . . . . 13
261	260	fveq1i 6192	. . . . . . . . . . . 12
262		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20
263	262	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19
264	263	cbvprodv 14646	. . . . . . . . . . . . . . . . . 18
265	264	oveq2i 6661	. . . . . . . . . . . . . . . . 17
266	265	a1i 11	. . . . . . . . . . . . . . . 16
267		fveq2 6191	. . . . . . . . . . . . . . . . . 18
268	267	prodeq2ad 39824	. . . . . . . . . . . . . . . . 17
269	254	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . 21
270	269, 262	fveq12d 6197	. . . . . . . . . . . . . . . . . . . 20
271	270	fveq1d 6193	. . . . . . . . . . . . . . . . . . 19
272	271	cbvprodv 14646	. . . . . . . . . . . . . . . . . 18
273	272	a1i 11	. . . . . . . . . . . . . . . . 17
274	268, 273	eqtrd 2656	. . . . . . . . . . . . . . . 16
275	266, 274	oveq12d 6668	. . . . . . . . . . . . . . 15
276	275	sumeq2ad 14434	. . . . . . . . . . . . . 14
277		fveq1 6190	. . . . . . . . . . . . . . . . . . . 20
278	277	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19
279	278	prodeq2ad 39824	. . . . . . . . . . . . . . . . . 18
280	279	oveq2d 6666	. . . . . . . . . . . . . . . . 17
281	277	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19
282	281	fveq1d 6193	. . . . . . . . . . . . . . . . . 18
283	282	prodeq2ad 39824	. . . . . . . . . . . . . . . . 17
284	280, 283	oveq12d 6668	. . . . . . . . . . . . . . . 16
285	284	cbvsumv 14426	. . . . . . . . . . . . . . 15
286	285	a1i 11	. . . . . . . . . . . . . 14
287	276, 286	eqtrd 2656	. . . . . . . . . . . . 13
288	287	cbvmptv 4750	. . . . . . . . . . . 12
289	261, 288	eqeq12i 2636	. . . . . . . . . . 11
290	289	ralbii 2980	. . . . . . . . . 10
291	290	biimpi 206	. . . . . . . . 9
292	291	ad2antlr 763	. . . . . . . 8 $/\$ $/\$ $\$ $/\$ $/\$
293		simpr 477	. . . . . . . 8 $/\$ $/\$ $\$ $/\$ $/\$
294	76	ad3antrrr 766	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ $/\$
295	90	ad3antrrr 766	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ $/\$ ℂ_fld ↾_t
296		dvnprodlem3.t	. . . . . . . . . 10
297	296	ad3antrrr 766	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ $/\$
298		simp-4l 806	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $/\$ $/\$
299		simpr 477	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $/\$ $/\$
300		dvnprodlem3.h	. . . . . . . . . 10 $/\$
301	298, 299, 300	syl2anc 693	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ $/\$ $/\$
302		dvnprodlem3.n	. . . . . . . . . 10
303	302	ad3antrrr 766	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ $/\$
304		simplll 798	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $/\$
305	304	3ad2ant1 1082	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$
306		simp2 1062	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$
307		simp3 1063	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$
308		eleq1 2689	. . . . . . . . . . . . 13
309	308	3anbi3d 1405	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
310		fveq2 6191	. . . . . . . . . . . . 13
311	310	feq1d 6030	. . . . . . . . . . . 12
312	309, 311	imbi12d 334	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
313		dvnprodlem3.dvnh	. . . . . . . . . . 11 $/\$ $/\$
314	312, 313	chvarv 2263	. . . . . . . . . 10 $/\$ $/\$
315	305, 306, 307, 314	syl3anc 1326	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$
316		simprl 794	. . . . . . . . . 10 $/\$ $/\$ $\$
317	316	ad2antrr 762	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ $/\$
318		simprr 796	. . . . . . . . . 10 $/\$ $/\$ $\$ $\$
319	318	ad2antrr 762	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ $/\$ $\$
320	260	eqcomi 2631	. . . . . . . . . . . . . . 15
321	320	a1i 11	. . . . . . . . . . . . . 14
322		id 22	. . . . . . . . . . . . . 14
323	321, 322	fveq12d 6197	. . . . . . . . . . . . 13
324	288	eqcomi 2631	. . . . . . . . . . . . . . 15
325	324	a1i 11	. . . . . . . . . . . . . 14
326		fveq2 6191	. . . . . . . . . . . . . . . . . . 19
327	326	oveq1d 6665	. . . . . . . . . . . . . . . . . 18
328	327	oveq1d 6665	. . . . . . . . . . . . . . . . 17
329	328	sumeq2ad 14434	. . . . . . . . . . . . . . . 16
330		fveq2 6191	. . . . . . . . . . . . . . . . 17
331	330	sumeq1d 14431	. . . . . . . . . . . . . . . 16
332	329, 331	eqtrd 2656	. . . . . . . . . . . . . . 15
333	332	mpteq2dv 4745	. . . . . . . . . . . . . 14
334	325, 333	eqtrd 2656	. . . . . . . . . . . . 13
335	323, 334	eqeq12d 2637	. . . . . . . . . . . 12
336	335	cbvralv 3171	. . . . . . . . . . 11
337	336	biimpi 206	. . . . . . . . . 10
338	337	ad2antlr 763	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ $/\$
339		simpr 477	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ $/\$
340		fveq1 6190	. . . . . . . . . . . 12
341	340	oveq2d 6666	. . . . . . . . . . 11
342		reseq1 5390	. . . . . . . . . . 11
343	341, 342	opeq12d 4410	. . . . . . . . . 10
344	343	cbvmptv 4750	. . . . . . . . 9
345	294, 295, 297, 301, 303, 315, 106, 317, 319, 338, 339, 344	dvnprodlem2 40162	. . . . . . . 8 $/\$ $/\$ $\$ $/\$ $/\$
346	251, 292, 293, 345	syl21anc 1325	. . . . . . 7 $/\$ $/\$ $\$ $/\$ $/\$
347	346	ralrimiva 2966	. . . . . 6 $/\$ $/\$ $\$ $/\$
348		fveq2 6191	. . . . . . . 8
349		fveq2 6191	. . . . . . . . . . . . 13
350	349	oveq1d 6665	. . . . . . . . . . . 12
351	350	oveq1d 6665	. . . . . . . . . . 11
352	351	sumeq2ad 14434	. . . . . . . . . 10
353		fveq2 6191	. . . . . . . . . . 11
354	353	sumeq1d 14431	. . . . . . . . . 10
355	352, 354	eqtrd 2656	. . . . . . . . 9
356	355	mpteq2dv 4745	. . . . . . . 8
357	348, 356	eqeq12d 2637	. . . . . . 7
358	357	cbvralv 3171	. . . . . 6
359	347, 358	sylib 208	. . . . 5 $/\$ $/\$ $\$ $/\$
360	359	ex 450	. . . 4 $/\$ $/\$ $\$
361	16, 32, 48, 68, 250, 360, 296	findcard2d 8202	. . 3
362		nn0uz 11722	. . . . 5
363	302, 362	syl6eleq 2711	. . . 4
364		eluzfz2 12349	. . . 4
365	363, 364	syl 17	. . 3
366		fveq2 6191	. . . . 5
367		fveq2 6191	. . . . . . . 8
368	367	sumeq1d 14431	. . . . . . 7
369		fveq2 6191	. . . . . . . . . 10
370	369	oveq1d 6665	. . . . . . . . 9
371	370	oveq1d 6665	. . . . . . . 8
372	371	sumeq2ad 14434	. . . . . . 7
373	368, 372	eqtrd 2656	. . . . . 6
374	373	mpteq2dv 4745	. . . . 5
375	366, 374	eqeq12d 2637	. . . 4
376	375	rspccva 3308	. . 3 $/\$
377	361, 365, 376	syl2anc 693	. 2
378		oveq2 6658	. . . . . . . . . . 11
379		rabeq 3192	. . . . . . . . . . 11
380	378, 379	syl 17	. . . . . . . . . 10
381		sumeq1 14419	. . . . . . . . . . . 12
382	381	eqeq1d 2624	. . . . . . . . . . 11
383	382	rabbidv 3189	. . . . . . . . . 10
384	380, 383	eqtrd 2656	. . . . . . . . 9
385	384	mpteq2dv 4745	. . . . . . . 8
386	385	adantl 482	. . . . . . 7 $/\$
387		pwidg 4173	. . . . . . . 8
388	296, 387	syl 17	. . . . . . 7
389	140	mptex 6486	. . . . . . . 8
390	389	a1i 11	. . . . . . 7
391	107, 386, 388, 390	fvmptd 6288	. . . . . 6
392		dvnprodlem3.c	. . . . . . 7
393	392	a1i 11	. . . . . 6
394	391, 393	eqtr4d 2659	. . . . 5
395	394	fveq1d 6193	. . . 4
396	395	sumeq1d 14431	. . 3
397	396	mpteq2dv 4745	. 2
398	377, 397	eqtrd 2656	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384 $/\$ w3a 1037

wal 1481

wceq 1483

wcel 1990

wne 2794

wral 2912

crab 2916

cvv 3200 $\$ cdif 3571

cun 3572

wss 3574

c0 3915

cif 4086

cpw 4158

csn 4177

cpr 4179

cop 4183

cmpt 4729

cdm 5114

cres 5116

wfn 5883

wf 5884

cfv 5888 (class class class)co 6650

cmap 7857

cpm 7858

cfn 7955

cc 9934

cr 9935

cc0 9936

c1 9937

cmul 9941

cmin 10266

cdiv 10684

cn 11020

cn0 11292

cuz 11687

cfz 12326

cfa 13060

csu 14416

cprod 14635 ↾_t crest 16081

ctopn 16082 ℂ_fldccnfld 19746

cdvn 23628

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-seq 12802 df-exp 12861 df-fac 13061 df-bc 13090 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-sum 14417 df-prod 14636 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-hom 15966 df-cco 15967 df-rest 16083 df-topn 16084 df-0g 16102 df-gsum 16103 df-topgen 16104 df-pt 16105 df-prds 16108 df-xrs 16162 df-qtop 16167 df-imas 16168 df-xps 16170 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-submnd 17336 df-mulg 17541 df-cntz 17750 df-cmn 18195 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-fbas 19743 df-fg 19744 df-cnfld 19747 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cld 20823 df-ntr 20824 df-cls 20825 df-nei 20902 df-lp 20940 df-perf 20941 df-cn 21031 df-cnp 21032 df-haus 21119 df-tx 21365 df-hmeo 21558 df-fil 21650 df-fm 21742 df-flim 21743 df-flf 21744 df-xms 22125 df-ms 22126 df-tms 22127 df-cncf 22681 df-limc 23630 df-dv 23631 df-dvn 23632

This theorem is referenced by: dvnprod 40164

W3C validator