incexclem - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > incexclem		Unicode version

Theorem incexclem 12571

Description: Lemma for incexc 12572. (Contributed by Mario Carneiro, 7-Aug-2017.)

**Assertion**
Ref	Expression
incexclem	$/\$

Distinct variable groups:

Proof of Theorem incexclem Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		unieq 3984	. . . . . . . . . . 11
2		uni0 4002	. . . . . . . . . . 11
3	1, 2	syl6eq 2452	. . . . . . . . . 10
4	3	ineq2d 3502	. . . . . . . . 9
5		in0 3613	. . . . . . . . 9
6	4, 5	syl6eq 2452	. . . . . . . 8
7	6	fveq2d 5691	. . . . . . 7
8		hash0 11601	. . . . . . 7
9	7, 8	syl6eq 2452	. . . . . 6
10	9	oveq2d 6056	. . . . 5
11		pweq 3762	. . . . . . 7
12		pw0 3905	. . . . . . 7
13	11, 12	syl6eq 2452	. . . . . 6
14	13	sumeq1d 12450	. . . . 5
15	10, 14	eqeq12d 2418	. . . 4
16	15	ralbidv 2686	. . 3
17		unieq 3984	. . . . . . . 8
18	17	ineq2d 3502	. . . . . . 7
19	18	fveq2d 5691	. . . . . 6
20	19	oveq2d 6056	. . . . 5
21		pweq 3762	. . . . . 6
22	21	sumeq1d 12450	. . . . 5
23	20, 22	eqeq12d 2418	. . . 4
24	23	ralbidv 2686	. . 3
25		unieq 3984	. . . . . . . . 9
26		uniun 3994	. . . . . . . . . 10
27		vex 2919	. . . . . . . . . . . 12
28	27	unisn 3991	. . . . . . . . . . 11
29	28	uneq2i 3458	. . . . . . . . . 10
30	26, 29	eqtri 2424	. . . . . . . . 9
31	25, 30	syl6eq 2452	. . . . . . . 8
32	31	ineq2d 3502	. . . . . . 7
33	32	fveq2d 5691	. . . . . 6
34	33	oveq2d 6056	. . . . 5
35		pweq 3762	. . . . . 6
36	35	sumeq1d 12450	. . . . 5
37	34, 36	eqeq12d 2418	. . . 4
38	37	ralbidv 2686	. . 3
39		unieq 3984	. . . . . . . 8
40	39	ineq2d 3502	. . . . . . 7
41	40	fveq2d 5691	. . . . . 6
42	41	oveq2d 6056	. . . . 5
43		pweq 3762	. . . . . 6
44	43	sumeq1d 12450	. . . . 5
45	42, 44	eqeq12d 2418	. . . 4
46	45	ralbidv 2686	. . 3
47		hashcl 11594	. . . . . . 7
48	47	nn0cnd 10232	. . . . . 6
49	48	mulid2d 9062	. . . . 5
50		0ex 4299	. . . . . 6
51	49, 48	eqeltrd 2478	. . . . . 6
52		fveq2 5687	. . . . . . . . . . 11
53	52, 8	syl6eq 2452	. . . . . . . . . 10
54	53	oveq2d 6056	. . . . . . . . 9
55		neg1cn 10023	. . . . . . . . . 10
56		exp0 11341	. . . . . . . . . 10
57	55, 56	ax-mp 8	. . . . . . . . 9
58	54, 57	syl6eq 2452	. . . . . . . 8
59		rint0 4050	. . . . . . . . 9
60	59	fveq2d 5691	. . . . . . . 8
61	58, 60	oveq12d 6058	. . . . . . 7
62	61	sumsn 12489	. . . . . 6 $/\$
63	50, 51, 62	sylancr 645	. . . . 5
64	48	subid1d 9356	. . . . 5
65	49, 63, 64	3eqtr4rd 2447	. . . 4
66	65	rgen 2731	. . 3
67		fveq2 5687	. . . . . . . . . . . 12
68		ineq1 3495	. . . . . . . . . . . . 13
69	68	fveq2d 5691	. . . . . . . . . . . 12
70	67, 69	oveq12d 6058	. . . . . . . . . . 11
71		simpl 444	. . . . . . . . . . . . . . 15 $/\$
72	71	ineq1d 3501	. . . . . . . . . . . . . 14 $/\$
73	72	fveq2d 5691	. . . . . . . . . . . . 13 $/\$
74	73	oveq2d 6056	. . . . . . . . . . . 12 $/\$
75	74	sumeq2dv 12452	. . . . . . . . . . 11
76	70, 75	eqeq12d 2418	. . . . . . . . . 10
77	76	rspcva 3010	. . . . . . . . 9 $/\$
78	77	adantll 695	. . . . . . . 8 $/\$ $/\$ $/\$
79		simpr 448	. . . . . . . . . 10 $/\$ $/\$
80		inss1 3521	. . . . . . . . . 10
81		ssfi 7288	. . . . . . . . . 10 $/\$
82	79, 80, 81	sylancl 644	. . . . . . . . 9 $/\$ $/\$
83		fveq2 5687	. . . . . . . . . . . 12
84		ineq1 3495	. . . . . . . . . . . . . 14
85		in32 3513	. . . . . . . . . . . . . . 15
86		inass 3511	. . . . . . . . . . . . . . 15
87	85, 86	eqtri 2424	. . . . . . . . . . . . . 14
88	84, 87	syl6eq 2452	. . . . . . . . . . . . 13
89	88	fveq2d 5691	. . . . . . . . . . . 12
90	83, 89	oveq12d 6058	. . . . . . . . . . 11
91		ineq1 3495	. . . . . . . . . . . . . . 15
92		in32 3513	. . . . . . . . . . . . . . . 16
93		inass 3511	. . . . . . . . . . . . . . . 16
94	92, 93	eqtri 2424	. . . . . . . . . . . . . . 15
95	91, 94	syl6eq 2452	. . . . . . . . . . . . . 14
96	95	fveq2d 5691	. . . . . . . . . . . . 13
97	96	oveq2d 6056	. . . . . . . . . . . 12
98	97	sumeq2sdv 12453	. . . . . . . . . . 11
99	90, 98	eqeq12d 2418	. . . . . . . . . 10
100	99	rspcva 3010	. . . . . . . . 9 $/\$
101	82, 100	sylan 458	. . . . . . . 8 $/\$ $/\$ $/\$
102	78, 101	oveq12d 6058	. . . . . . 7 $/\$ $/\$ $/\$
103		inss1 3521	. . . . . . . . . . . . . 14
104		ssfi 7288	. . . . . . . . . . . . . 14 $/\$
105	79, 103, 104	sylancl 644	. . . . . . . . . . . . 13 $/\$ $/\$
106		hashun3 11613	. . . . . . . . . . . . 13 $/\$
107	105, 82, 106	syl2anc 643	. . . . . . . . . . . 12 $/\$ $/\$
108		indi 3547	. . . . . . . . . . . . 13
109	108	fveq2i 5690	. . . . . . . . . . . 12
110		inindi 3518	. . . . . . . . . . . . . 14
111	110	fveq2i 5690	. . . . . . . . . . . . 13
112	111	oveq2i 6051	. . . . . . . . . . . 12
113	107, 109, 112	3eqtr4g 2461	. . . . . . . . . . 11 $/\$ $/\$
114		hashcl 11594	. . . . . . . . . . . . . 14
115	105, 114	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$
116	115	nn0cnd 10232	. . . . . . . . . . . 12 $/\$ $/\$
117		hashcl 11594	. . . . . . . . . . . . . 14
118	82, 117	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$
119	118	nn0cnd 10232	. . . . . . . . . . . 12 $/\$ $/\$
120		inss1 3521	. . . . . . . . . . . . . . 15
121		ssfi 7288	. . . . . . . . . . . . . . 15 $/\$
122	79, 120, 121	sylancl 644	. . . . . . . . . . . . . 14 $/\$ $/\$
123		hashcl 11594	. . . . . . . . . . . . . 14
124	122, 123	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$
125	124	nn0cnd 10232	. . . . . . . . . . . 12 $/\$ $/\$
126	116, 119, 125	addsubassd 9387	. . . . . . . . . . 11 $/\$ $/\$
127	113, 126	eqtrd 2436	. . . . . . . . . 10 $/\$ $/\$
128	127	oveq2d 6056	. . . . . . . . 9 $/\$ $/\$
129		hashcl 11594	. . . . . . . . . . . 12
130	129	adantl 453	. . . . . . . . . . 11 $/\$ $/\$
131	130	nn0cnd 10232	. . . . . . . . . 10 $/\$ $/\$
132	119, 125	subcld 9367	. . . . . . . . . 10 $/\$ $/\$
133	131, 116, 132	subsub4d 9398	. . . . . . . . 9 $/\$ $/\$
134	128, 133	eqtr4d 2439	. . . . . . . 8 $/\$ $/\$
135	134	adantr 452	. . . . . . 7 $/\$ $/\$ $/\$
136		disjdif 3660	. . . . . . . . . . 11 $\$
137	136	a1i 11	. . . . . . . . . 10 $/\$ $/\$ $\$
138		ssun1 3470	. . . . . . . . . . . . . 14
139		sspwb 4373	. . . . . . . . . . . . . 14
140	138, 139	mpbi 200	. . . . . . . . . . . . 13
141		undif 3668	. . . . . . . . . . . . 13 $\$
142	140, 141	mpbi 200	. . . . . . . . . . . 12 $\$
143	142	eqcomi 2408	. . . . . . . . . . 11 $\$
144	143	a1i 11	. . . . . . . . . 10 $/\$ $/\$ $\$
145		simpll 731	. . . . . . . . . . . 12 $/\$ $/\$
146		snfi 7146	. . . . . . . . . . . 12
147		unfi 7333	. . . . . . . . . . . 12 $/\$
148	145, 146, 147	sylancl 644	. . . . . . . . . . 11 $/\$ $/\$
149		pwfi 7360	. . . . . . . . . . 11
150	148, 149	sylib 189	. . . . . . . . . 10 $/\$ $/\$
151	55	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152		elpwi 3767	. . . . . . . . . . . . . 14
153		ssfi 7288	. . . . . . . . . . . . . 14 $/\$
154	148, 152, 153	syl2an 464	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
155		hashcl 11594	. . . . . . . . . . . . 13
156	154, 155	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
157	151, 156	expcld 11478	. . . . . . . . . . 11 $/\$ $/\$ $/\$
158		simplr 732	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
159		inss1 3521	. . . . . . . . . . . . . 14
160		ssfi 7288	. . . . . . . . . . . . . 14 $/\$
161	158, 159, 160	sylancl 644	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
162		hashcl 11594	. . . . . . . . . . . . 13
163	161, 162	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
164	163	nn0cnd 10232	. . . . . . . . . . 11 $/\$ $/\$ $/\$
165	157, 164	mulcld 9064	. . . . . . . . . 10 $/\$ $/\$ $/\$
166	137, 144, 150, 165	fsumsplit 12488	. . . . . . . . 9 $/\$ $/\$ $\$
167		fveq2 5687	. . . . . . . . . . . . . 14
168	167	oveq2d 6056	. . . . . . . . . . . . 13
169		inteq 4013	. . . . . . . . . . . . . . . 16
170	27	intunsn 4049	. . . . . . . . . . . . . . . 16
171	169, 170	syl6eq 2452	. . . . . . . . . . . . . . 15
172	171	ineq2d 3502	. . . . . . . . . . . . . 14
173	172	fveq2d 5691	. . . . . . . . . . . . 13
174	168, 173	oveq12d 6058	. . . . . . . . . . . 12
175		pwfi 7360	. . . . . . . . . . . . 13
176	145, 175	sylib 189	. . . . . . . . . . . 12 $/\$ $/\$
177		eqid 2404	. . . . . . . . . . . . 13
178		elpwi 3767	. . . . . . . . . . . . . . . . 17
179	178	adantl 453	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
180		unss1 3476	. . . . . . . . . . . . . . . 16
181	179, 180	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
182		vex 2919	. . . . . . . . . . . . . . . . 17
183		snex 4365	. . . . . . . . . . . . . . . . 17
184	182, 183	unex 4666	. . . . . . . . . . . . . . . 16
185	184	elpw 3765	. . . . . . . . . . . . . . 15
186	181, 185	sylibr 204	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
187		simpllr 736	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
188		elpwi 3767	. . . . . . . . . . . . . . . 16
189		ssun2 3471	. . . . . . . . . . . . . . . . . . 19
190	27	snss 3886	. . . . . . . . . . . . . . . . . . 19
191	189, 190	mpbir 201	. . . . . . . . . . . . . . . . . 18
192	191	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
193		ssel 3302	. . . . . . . . . . . . . . . . 17
194	192, 193	syl5com 28	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
195	188, 194	syl5 30	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
196	187, 195	mtod 170	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
197	186, 196	eldifd 3291	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
198		eldifi 3429	. . . . . . . . . . . . . . . . . 18 $\$
199	198	adantl 453	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
200	199	elpwid 3768	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
201		uncom 3451	. . . . . . . . . . . . . . . 16
202	200, 201	syl6sseq 3354	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
203		ssundif 3671	. . . . . . . . . . . . . . 15 $\$
204	202, 203	sylib 189	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
205		vex 2919	. . . . . . . . . . . . . . 15
206	205	elpw2 4324	. . . . . . . . . . . . . 14 $\$ $\$
207	204, 206	sylibr 204	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
208		elpwunsn 4716	. . . . . . . . . . . . . . . . . . 19 $\$
209	208	ad2antll 710	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$
210	209	snssd 3903	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\$
211		ssequn2 3480	. . . . . . . . . . . . . . . . 17
212	210, 211	sylib 189	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $\$
213	212	eqcomd 2409	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$
214		uneq1 3454	. . . . . . . . . . . . . . . . 17 $\$ $\$
215		undif1 3663	. . . . . . . . . . . . . . . . 17 $\$
216	214, 215	syl6eq 2452	. . . . . . . . . . . . . . . 16 $\$
217	216	eqeq2d 2415	. . . . . . . . . . . . . . 15 $\$
218	213, 217	syl5ibrcom 214	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $\$ $\$
219	178	ad2antrl 709	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$
220		simpllr 736	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$
221	219, 220	ssneldd 3311	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\$
222		difsnb 3900	. . . . . . . . . . . . . . . . 17 $\$
223	221, 222	sylib 189	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $\$ $\$
224	223	eqcomd 2409	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$ $\$
225		difeq1 3418	. . . . . . . . . . . . . . . . 17 $\$ $\$
226		difun2 3667	. . . . . . . . . . . . . . . . 17 $\$ $\$
227	225, 226	syl6eq 2452	. . . . . . . . . . . . . . . 16 $\$ $\$
228	227	eqeq2d 2415	. . . . . . . . . . . . . . 15 $\$ $\$
229	224, 228	syl5ibrcom 214	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $\$ $\$
230	218, 229	impbid 184	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\$ $\$
231	177, 197, 207, 230	f1o2d 6255	. . . . . . . . . . . 12 $/\$ $/\$ $\$
232		uneq1 3454	. . . . . . . . . . . . . 14
233		vex 2919	. . . . . . . . . . . . . . 15
234	233, 183	unex 4666	. . . . . . . . . . . . . 14
235	232, 177, 234	fvmpt 5765	. . . . . . . . . . . . 13
236	235	adantl 453	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
237	198, 165	sylan2 461	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
238	174, 176, 231, 236, 237	fsumf1o 12472	. . . . . . . . . . 11 $/\$ $/\$ $\$
239		uneq1 3454	. . . . . . . . . . . . . . . 16
240	239	fveq2d 5691	. . . . . . . . . . . . . . 15
241	240	oveq2d 6056	. . . . . . . . . . . . . 14
242		inteq 4013	. . . . . . . . . . . . . . . . 17
243	242	ineq1d 3501	. . . . . . . . . . . . . . . 16
244	243	ineq2d 3502	. . . . . . . . . . . . . . 15
245	244	fveq2d 5691	. . . . . . . . . . . . . 14
246	241, 245	oveq12d 6058	. . . . . . . . . . . . 13
247	246	cbvsumv 12445	. . . . . . . . . . . 12
248		elpwi 3767	. . . . . . . . . . . . . . . . . . . 20
249		ssfi 7288	. . . . . . . . . . . . . . . . . . . 20 $/\$
250	145, 248, 249	syl2an 464	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
251	248	adantl 453	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
252		simpllr 736	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
253	251, 252	ssneldd 3311	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
254		hashunsng 11620	. . . . . . . . . . . . . . . . . . . 20 $/\$
255	27, 254	ax-mp 8	. . . . . . . . . . . . . . . . . . 19 $/\$
256	250, 253, 255	syl2anc 643	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
257	256	oveq2d 6056	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
258	55	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
259	250, 155	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
260	258, 259	expp1d 11479	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
261	257, 260	eqtrd 2436	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
262	140	sseli 3304	. . . . . . . . . . . . . . . . . 18
263	262, 157	sylan2 461	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
264	258, 263	mulcomd 9065	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
265	263	mulm1d 9441	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
266	261, 264, 265	3eqtr2d 2442	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
267	266	oveq1d 6055	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
268		inss1 3521	. . . . . . . . . . . . . . . . . . 19
269		ssfi 7288	. . . . . . . . . . . . . . . . . . 19 $/\$
270	158, 268, 269	sylancl 644	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
271		hashcl 11594	. . . . . . . . . . . . . . . . . 18
272	270, 271	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
273	272	nn0cnd 10232	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
274	262, 273	sylan2 461	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
275	263, 274	mulneg1d 9442	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
276	267, 275	eqtrd 2436	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
277	276	sumeq2dv 12452	. . . . . . . . . . . 12 $/\$ $/\$
278	247, 277	syl5eq 2448	. . . . . . . . . . 11 $/\$ $/\$
279	157, 273	mulcld 9064	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
280	262, 279	sylan2 461	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
281	176, 280	fsumneg 12525	. . . . . . . . . . 11 $/\$ $/\$
282	238, 278, 281	3eqtrd 2440	. . . . . . . . . 10 $/\$ $/\$ $\$
283	282	oveq2d 6056	. . . . . . . . 9 $/\$ $/\$ $\$
284	140	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
285	284	sselda 3308	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
286	285, 165	syldan 457	. . . . . . . . . . 11 $/\$ $/\$ $/\$
287	176, 286	fsumcl 12482	. . . . . . . . . 10 $/\$ $/\$
288	285, 279	syldan 457	. . . . . . . . . . 11 $/\$ $/\$ $/\$
289	176, 288	fsumcl 12482	. . . . . . . . . 10 $/\$ $/\$
290	287, 289	negsubd 9373	. . . . . . . . 9 $/\$ $/\$
291	166, 283, 290	3eqtrd 2440	. . . . . . . 8 $/\$ $/\$
292	291	adantr 452	. . . . . . 7 $/\$ $/\$ $/\$
293	102, 135, 292	3eqtr4d 2446	. . . . . 6 $/\$ $/\$ $/\$
294	293	ex 424	. . . . 5 $/\$ $/\$
295	294	ralrimdva 2756	. . . 4 $/\$
296		ineq1 3495	. . . . . . . 8
297	296	fveq2d 5691	. . . . . . 7
298	67, 297	oveq12d 6058	. . . . . 6
299		ineq1 3495	. . . . . . . . 9
300	299	fveq2d 5691	. . . . . . . 8
301	300	oveq2d 6056	. . . . . . 7
302	301	sumeq2sdv 12453	. . . . . 6
303	298, 302	eqeq12d 2418	. . . . 5
304	303	cbvralv 2892	. . . 4
305	295, 304	syl6ibr 219	. . 3 $/\$
306	16, 24, 38, 46, 66, 305	findcard2s 7308	. 2
307		fveq2 5687	. . . . 5
308		ineq1 3495	. . . . . 6
309	308	fveq2d 5691	. . . . 5
310	307, 309	oveq12d 6058	. . . 4
311		simpl 444	. . . . . . . 8 $/\$
312	311	ineq1d 3501	. . . . . . 7 $/\$
313	312	fveq2d 5691	. . . . . 6 $/\$
314	313	oveq2d 6056	. . . . 5 $/\$
315	314	sumeq2dv 12452	. . . 4
316	310, 315	eqeq12d 2418	. . 3
317	316	rspccva 3011	. 2 $/\$
318	306, 317	sylan 458	1 $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 359

wceq 1649

wcel 1721

wral 2666

cvv 2916 $\$ cdif 3277

cun 3278

cin 3279

wss 3280

c0 3588

cpw 3759

csn 3774

cuni 3975

cint 4010

cmpt 4226

cfv 5413 (class class class)co 6040

cfn 7068

cc 8944

cc0 8946

c1 8947

caddc 8949

cmul 8951

cmin 9247

cneg 9248

cn0 10177

cexp 11337

chash 11573

csu 12434

This theorem is referenced by: incexc 12572

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-inf2 7552 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-se 4502 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-2o 6684 df-oadd 6687 df-er 6864 df-map 6979 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-sup 7404 df-oi 7435 df-card 7782 df-cda 8004 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-3 10015 df-n0 10178 df-z 10239 df-uz 10445 df-rp 10569 df-fz 11000 df-fzo 11091 df-seq 11279 df-exp 11338 df-hash 11574 df-cj 11859 df-re 11860 df-im 11861 df-sqr 11995 df-abs 11996 df-clim 12237 df-sum 12435

W3C validator