incexclem - Metamath Proof Explorer

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

Theorem incexclem 13627

Description: Lemma for incexc 13628. (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 4259	. . . . . . . . . . 11
2		uni0 4278	. . . . . . . . . . 11
3	1, 2	syl6eq 2524	. . . . . . . . . 10
4	3	ineq2d 3705	. . . . . . . . 9
5		in0 3816	. . . . . . . . 9
6	4, 5	syl6eq 2524	. . . . . . . 8
7	6	fveq2d 5876	. . . . . . 7
8		hash0 12417	. . . . . . 7
9	7, 8	syl6eq 2524	. . . . . 6
10	9	oveq2d 6311	. . . . 5
11		pweq 4019	. . . . . . 7
12		pw0 4180	. . . . . . 7
13	11, 12	syl6eq 2524	. . . . . 6
14	13	sumeq1d 13502	. . . . 5
15	10, 14	eqeq12d 2489	. . . 4
16	15	ralbidv 2906	. . 3
17		unieq 4259	. . . . . . . 8
18	17	ineq2d 3705	. . . . . . 7
19	18	fveq2d 5876	. . . . . 6
20	19	oveq2d 6311	. . . . 5
21		pweq 4019	. . . . . 6
22	21	sumeq1d 13502	. . . . 5
23	20, 22	eqeq12d 2489	. . . 4
24	23	ralbidv 2906	. . 3
25		unieq 4259	. . . . . . . . 9
26		uniun 4270	. . . . . . . . . 10
27		vex 3121	. . . . . . . . . . . 12
28	27	unisn 4266	. . . . . . . . . . 11
29	28	uneq2i 3660	. . . . . . . . . 10
30	26, 29	eqtri 2496	. . . . . . . . 9
31	25, 30	syl6eq 2524	. . . . . . . 8
32	31	ineq2d 3705	. . . . . . 7
33	32	fveq2d 5876	. . . . . 6
34	33	oveq2d 6311	. . . . 5
35		pweq 4019	. . . . . 6
36	35	sumeq1d 13502	. . . . 5
37	34, 36	eqeq12d 2489	. . . 4
38	37	ralbidv 2906	. . 3
39		unieq 4259	. . . . . . . 8
40	39	ineq2d 3705	. . . . . . 7
41	40	fveq2d 5876	. . . . . 6
42	41	oveq2d 6311	. . . . 5
43		pweq 4019	. . . . . 6
44	43	sumeq1d 13502	. . . . 5
45	42, 44	eqeq12d 2489	. . . 4
46	45	ralbidv 2906	. . 3
47		hashcl 12408	. . . . . . 7
48	47	nn0cnd 10866	. . . . . 6
49	48	mulid2d 9626	. . . . 5
50		0ex 4583	. . . . . 6
51	49, 48	eqeltrd 2555	. . . . . 6
52		fveq2 5872	. . . . . . . . . . 11
53	52, 8	syl6eq 2524	. . . . . . . . . 10
54	53	oveq2d 6311	. . . . . . . . 9
55		neg1cn 10651	. . . . . . . . . 10
56		exp0 12150	. . . . . . . . . 10
57	55, 56	ax-mp 5	. . . . . . . . 9
58	54, 57	syl6eq 2524	. . . . . . . 8
59		rint0 4328	. . . . . . . . 9
60	59	fveq2d 5876	. . . . . . . 8
61	58, 60	oveq12d 6313	. . . . . . 7
62	61	sumsn 13542	. . . . . 6 $/\$
63	50, 51, 62	sylancr 663	. . . . 5
64	48	subid1d 9931	. . . . 5
65	49, 63, 64	3eqtr4rd 2519	. . . 4
66	65	rgen 2827	. . 3
67		fveq2 5872	. . . . . . . . . . . 12
68		ineq1 3698	. . . . . . . . . . . . 13
69	68	fveq2d 5876	. . . . . . . . . . . 12
70	67, 69	oveq12d 6313	. . . . . . . . . . 11
71		simpl 457	. . . . . . . . . . . . . . 15 $/\$
72	71	ineq1d 3704	. . . . . . . . . . . . . 14 $/\$
73	72	fveq2d 5876	. . . . . . . . . . . . 13 $/\$
74	73	oveq2d 6311	. . . . . . . . . . . 12 $/\$
75	74	sumeq2dv 13504	. . . . . . . . . . 11
76	70, 75	eqeq12d 2489	. . . . . . . . . 10
77	76	rspcva 3217	. . . . . . . . 9 $/\$
78	77	adantll 713	. . . . . . . 8 $/\$ $/\$ $/\$
79		simpr 461	. . . . . . . . . 10 $/\$ $/\$
80		inss1 3723	. . . . . . . . . 10
81		ssfi 7752	. . . . . . . . . 10 $/\$
82	79, 80, 81	sylancl 662	. . . . . . . . 9 $/\$ $/\$
83		fveq2 5872	. . . . . . . . . . . 12
84		ineq1 3698	. . . . . . . . . . . . . 14
85		in32 3715	. . . . . . . . . . . . . . 15
86		inass 3713	. . . . . . . . . . . . . . 15
87	85, 86	eqtri 2496	. . . . . . . . . . . . . 14
88	84, 87	syl6eq 2524	. . . . . . . . . . . . 13
89	88	fveq2d 5876	. . . . . . . . . . . 12
90	83, 89	oveq12d 6313	. . . . . . . . . . 11
91		ineq1 3698	. . . . . . . . . . . . . . 15
92		in32 3715	. . . . . . . . . . . . . . . 16
93		inass 3713	. . . . . . . . . . . . . . . 16
94	92, 93	eqtri 2496	. . . . . . . . . . . . . . 15
95	91, 94	syl6eq 2524	. . . . . . . . . . . . . 14
96	95	fveq2d 5876	. . . . . . . . . . . . 13
97	96	oveq2d 6311	. . . . . . . . . . . 12
98	97	sumeq2sdv 13505	. . . . . . . . . . 11
99	90, 98	eqeq12d 2489	. . . . . . . . . 10
100	99	rspcva 3217	. . . . . . . . 9 $/\$
101	82, 100	sylan 471	. . . . . . . 8 $/\$ $/\$ $/\$
102	78, 101	oveq12d 6313	. . . . . . 7 $/\$ $/\$ $/\$
103		inss1 3723	. . . . . . . . . . . . . 14
104		ssfi 7752	. . . . . . . . . . . . . 14 $/\$
105	79, 103, 104	sylancl 662	. . . . . . . . . . . . 13 $/\$ $/\$
106		hashun3 12432	. . . . . . . . . . . . 13 $/\$
107	105, 82, 106	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$
108		indi 3749	. . . . . . . . . . . . 13
109	108	fveq2i 5875	. . . . . . . . . . . 12
110		inindi 3720	. . . . . . . . . . . . . 14
111	110	fveq2i 5875	. . . . . . . . . . . . 13
112	111	oveq2i 6306	. . . . . . . . . . . 12
113	107, 109, 112	3eqtr4g 2533	. . . . . . . . . . 11 $/\$ $/\$
114		hashcl 12408	. . . . . . . . . . . . . 14
115	105, 114	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$
116	115	nn0cnd 10866	. . . . . . . . . . . 12 $/\$ $/\$
117		hashcl 12408	. . . . . . . . . . . . . 14
118	82, 117	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$
119	118	nn0cnd 10866	. . . . . . . . . . . 12 $/\$ $/\$
120		inss1 3723	. . . . . . . . . . . . . . 15
121		ssfi 7752	. . . . . . . . . . . . . . 15 $/\$
122	79, 120, 121	sylancl 662	. . . . . . . . . . . . . 14 $/\$ $/\$
123		hashcl 12408	. . . . . . . . . . . . . 14
124	122, 123	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$
125	124	nn0cnd 10866	. . . . . . . . . . . 12 $/\$ $/\$
126	116, 119, 125	addsubassd 9962	. . . . . . . . . . 11 $/\$ $/\$
127	113, 126	eqtrd 2508	. . . . . . . . . 10 $/\$ $/\$
128	127	oveq2d 6311	. . . . . . . . 9 $/\$ $/\$
129		hashcl 12408	. . . . . . . . . . . 12
130	129	adantl 466	. . . . . . . . . . 11 $/\$ $/\$
131	130	nn0cnd 10866	. . . . . . . . . 10 $/\$ $/\$
132	119, 125	subcld 9942	. . . . . . . . . 10 $/\$ $/\$
133	131, 116, 132	subsub4d 9973	. . . . . . . . 9 $/\$ $/\$
134	128, 133	eqtr4d 2511	. . . . . . . 8 $/\$ $/\$
135	134	adantr 465	. . . . . . 7 $/\$ $/\$ $/\$
136		disjdif 3905	. . . . . . . . . . 11 $\$
137	136	a1i 11	. . . . . . . . . 10 $/\$ $/\$ $\$
138		ssun1 3672	. . . . . . . . . . . . . 14
139		sspwb 4702	. . . . . . . . . . . . . 14
140	138, 139	mpbi 208	. . . . . . . . . . . . 13
141		undif 3913	. . . . . . . . . . . . 13 $\$
142	140, 141	mpbi 208	. . . . . . . . . . . 12 $\$
143	142	eqcomi 2480	. . . . . . . . . . 11 $\$
144	143	a1i 11	. . . . . . . . . 10 $/\$ $/\$ $\$
145		simpll 753	. . . . . . . . . . . 12 $/\$ $/\$
146		snfi 7608	. . . . . . . . . . . 12
147		unfi 7799	. . . . . . . . . . . 12 $/\$
148	145, 146, 147	sylancl 662	. . . . . . . . . . 11 $/\$ $/\$
149		pwfi 7827	. . . . . . . . . . 11
150	148, 149	sylib 196	. . . . . . . . . 10 $/\$ $/\$
151	55	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152		elpwi 4025	. . . . . . . . . . . . . 14
153		ssfi 7752	. . . . . . . . . . . . . 14 $/\$
154	148, 152, 153	syl2an 477	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
155		hashcl 12408	. . . . . . . . . . . . 13
156	154, 155	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
157	151, 156	expcld 12290	. . . . . . . . . . 11 $/\$ $/\$ $/\$
158		simplr 754	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
159		inss1 3723	. . . . . . . . . . . . . 14
160		ssfi 7752	. . . . . . . . . . . . . 14 $/\$
161	158, 159, 160	sylancl 662	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
162		hashcl 12408	. . . . . . . . . . . . 13
163	161, 162	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
164	163	nn0cnd 10866	. . . . . . . . . . 11 $/\$ $/\$ $/\$
165	157, 164	mulcld 9628	. . . . . . . . . 10 $/\$ $/\$ $/\$
166	137, 144, 150, 165	fsumsplit 13541	. . . . . . . . 9 $/\$ $/\$ $\$
167		fveq2 5872	. . . . . . . . . . . . . 14
168	167	oveq2d 6311	. . . . . . . . . . . . 13
169		inteq 4291	. . . . . . . . . . . . . . . 16
170	27	intunsn 4327	. . . . . . . . . . . . . . . 16
171	169, 170	syl6eq 2524	. . . . . . . . . . . . . . 15
172	171	ineq2d 3705	. . . . . . . . . . . . . 14
173	172	fveq2d 5876	. . . . . . . . . . . . 13
174	168, 173	oveq12d 6313	. . . . . . . . . . . 12
175		pwfi 7827	. . . . . . . . . . . . 13
176	145, 175	sylib 196	. . . . . . . . . . . 12 $/\$ $/\$
177		eqid 2467	. . . . . . . . . . . . 13
178		elpwi 4025	. . . . . . . . . . . . . . . . 17
179	178	adantl 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
180		unss1 3678	. . . . . . . . . . . . . . . 16
181	179, 180	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
182		vex 3121	. . . . . . . . . . . . . . . . 17
183		snex 4694	. . . . . . . . . . . . . . . . 17
184	182, 183	unex 6593	. . . . . . . . . . . . . . . 16
185	184	elpw 4022	. . . . . . . . . . . . . . 15
186	181, 185	sylibr 212	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
187		simpllr 758	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
188		elpwi 4025	. . . . . . . . . . . . . . . 16
189		ssun2 3673	. . . . . . . . . . . . . . . . . . 19
190	27	snss 4157	. . . . . . . . . . . . . . . . . . 19
191	189, 190	mpbir 209	. . . . . . . . . . . . . . . . . 18
192	191	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
193		ssel 3503	. . . . . . . . . . . . . . . . 17
194	192, 193	syl5com 30	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
195	188, 194	syl5 32	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
196	187, 195	mtod 177	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
197	186, 196	eldifd 3492	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
198		eldifi 3631	. . . . . . . . . . . . . . . . . 18 $\$
199	198	adantl 466	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
200	199	elpwid 4026	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
201		uncom 3653	. . . . . . . . . . . . . . . 16
202	200, 201	syl6sseq 3555	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
203		ssundif 3916	. . . . . . . . . . . . . . 15 $\$
204	202, 203	sylib 196	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
205		vex 3121	. . . . . . . . . . . . . . 15
206	205	elpw2 4617	. . . . . . . . . . . . . 14 $\$ $\$
207	204, 206	sylibr 212	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
208		elpwunsn 4074	. . . . . . . . . . . . . . . . . . 19 $\$
209	208	ad2antll 728	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$
210	209	snssd 4178	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\$
211		ssequn2 3682	. . . . . . . . . . . . . . . . 17
212	210, 211	sylib 196	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $\$
213	212	eqcomd 2475	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$
214		uneq1 3656	. . . . . . . . . . . . . . . . 17 $\$ $\$
215		undif1 3908	. . . . . . . . . . . . . . . . 17 $\$
216	214, 215	syl6eq 2524	. . . . . . . . . . . . . . . 16 $\$
217	216	eqeq2d 2481	. . . . . . . . . . . . . . 15 $\$
218	213, 217	syl5ibrcom 222	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $\$ $\$
219	178	ad2antrl 727	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$
220		simpllr 758	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$
221	219, 220	ssneldd 3512	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\$
222		difsnb 4175	. . . . . . . . . . . . . . . . 17 $\$
223	221, 222	sylib 196	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $\$ $\$
224	223	eqcomd 2475	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$ $\$
225		difeq1 3620	. . . . . . . . . . . . . . . . 17 $\$ $\$
226		difun2 3912	. . . . . . . . . . . . . . . . 17 $\$ $\$
227	225, 226	syl6eq 2524	. . . . . . . . . . . . . . . 16 $\$ $\$
228	227	eqeq2d 2481	. . . . . . . . . . . . . . 15 $\$ $\$
229	224, 228	syl5ibrcom 222	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $\$ $\$
230	218, 229	impbid 191	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\$ $\$
231	177, 197, 207, 230	f1o2d 6522	. . . . . . . . . . . 12 $/\$ $/\$ $\$
232		uneq1 3656	. . . . . . . . . . . . . 14
233		vex 3121	. . . . . . . . . . . . . . 15
234	233, 183	unex 6593	. . . . . . . . . . . . . 14
235	232, 177, 234	fvmpt 5957	. . . . . . . . . . . . 13
236	235	adantl 466	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
237	198, 165	sylan2 474	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
238	174, 176, 231, 236, 237	fsumf1o 13524	. . . . . . . . . . 11 $/\$ $/\$ $\$
239		uneq1 3656	. . . . . . . . . . . . . . . 16
240	239	fveq2d 5876	. . . . . . . . . . . . . . 15
241	240	oveq2d 6311	. . . . . . . . . . . . . 14
242		inteq 4291	. . . . . . . . . . . . . . . . 17
243	242	ineq1d 3704	. . . . . . . . . . . . . . . 16
244	243	ineq2d 3705	. . . . . . . . . . . . . . 15
245	244	fveq2d 5876	. . . . . . . . . . . . . 14
246	241, 245	oveq12d 6313	. . . . . . . . . . . . 13
247	246	cbvsumv 13497	. . . . . . . . . . . 12
248		elpwi 4025	. . . . . . . . . . . . . . . . . . . 20
249		ssfi 7752	. . . . . . . . . . . . . . . . . . . 20 $/\$
250	145, 248, 249	syl2an 477	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
251	248	adantl 466	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
252		simpllr 758	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
253	251, 252	ssneldd 3512	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
254		hashunsng 12439	. . . . . . . . . . . . . . . . . . . 20 $/\$
255	27, 254	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 $/\$
256	250, 253, 255	syl2anc 661	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
257	256	oveq2d 6311	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
258	55	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
259	250, 155	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
260	258, 259	expp1d 12291	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
261	257, 260	eqtrd 2508	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
262	140	sseli 3505	. . . . . . . . . . . . . . . . . 18
263	262, 157	sylan2 474	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
264	258, 263	mulcomd 9629	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
265	263	mulm1d 10020	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
266	261, 264, 265	3eqtr2d 2514	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
267	266	oveq1d 6310	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
268		inss1 3723	. . . . . . . . . . . . . . . . . . 19
269		ssfi 7752	. . . . . . . . . . . . . . . . . . 19 $/\$
270	158, 268, 269	sylancl 662	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
271		hashcl 12408	. . . . . . . . . . . . . . . . . 18
272	270, 271	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
273	272	nn0cnd 10866	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
274	262, 273	sylan2 474	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
275	263, 274	mulneg1d 10021	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
276	267, 275	eqtrd 2508	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
277	276	sumeq2dv 13504	. . . . . . . . . . . 12 $/\$ $/\$
278	247, 277	syl5eq 2520	. . . . . . . . . . 11 $/\$ $/\$
279	157, 273	mulcld 9628	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
280	262, 279	sylan2 474	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
281	176, 280	fsumneg 13581	. . . . . . . . . . 11 $/\$ $/\$
282	238, 278, 281	3eqtrd 2512	. . . . . . . . . 10 $/\$ $/\$ $\$
283	282	oveq2d 6311	. . . . . . . . 9 $/\$ $/\$ $\$
284	140	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
285	284	sselda 3509	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
286	285, 165	syldan 470	. . . . . . . . . . 11 $/\$ $/\$ $/\$
287	176, 286	fsumcl 13534	. . . . . . . . . 10 $/\$ $/\$
288	285, 279	syldan 470	. . . . . . . . . . 11 $/\$ $/\$ $/\$
289	176, 288	fsumcl 13534	. . . . . . . . . 10 $/\$ $/\$
290	287, 289	negsubd 9948	. . . . . . . . 9 $/\$ $/\$
291	166, 283, 290	3eqtrd 2512	. . . . . . . 8 $/\$ $/\$
292	291	adantr 465	. . . . . . 7 $/\$ $/\$ $/\$
293	102, 135, 292	3eqtr4d 2518	. . . . . 6 $/\$ $/\$ $/\$
294	293	ex 434	. . . . 5 $/\$ $/\$
295	294	ralrimdva 2885	. . . 4 $/\$
296		ineq1 3698	. . . . . . . 8
297	296	fveq2d 5876	. . . . . . 7
298	67, 297	oveq12d 6313	. . . . . 6
299		ineq1 3698	. . . . . . . . 9
300	299	fveq2d 5876	. . . . . . . 8
301	300	oveq2d 6311	. . . . . . 7
302	301	sumeq2sdv 13505	. . . . . 6
303	298, 302	eqeq12d 2489	. . . . 5
304	303	cbvralv 3093	. . . 4
305	295, 304	syl6ibr 227	. . 3 $/\$
306	16, 24, 38, 46, 66, 305	findcard2s 7773	. 2
307		fveq2 5872	. . . . 5
308		ineq1 3698	. . . . . 6
309	308	fveq2d 5876	. . . . 5
310	307, 309	oveq12d 6313	. . . 4
311		simpl 457	. . . . . . . 8 $/\$
312	311	ineq1d 3704	. . . . . . 7 $/\$
313	312	fveq2d 5876	. . . . . 6 $/\$
314	313	oveq2d 6311	. . . . 5 $/\$
315	314	sumeq2dv 13504	. . . 4
316	310, 315	eqeq12d 2489	. . 3
317	316	rspccva 3218	. 2 $/\$
318	306, 317	sylan 471	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 369

wceq 1379

wcel 1767

wral 2817

cvv 3118 $\$ cdif 3478

cun 3479

cin 3480

wss 3481

c0 3790

cpw 4016

csn 4033

cuni 4251

cint 4288

cmpt 4511

cfv 5594 (class class class)co 6295

cfn 7528

cc 9502

cc0 9504

c1 9505

caddc 9507

cmul 9509

cmin 9817

cneg 9818

cn0 10807

cexp 12146

chash 12385

csu 13487

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4564 ax-sep 4574 ax-nul 4582 ax-pow 4631 ax-pr 4692 ax-un 6587 ax-inf2 8070 ax-cnex 9560 ax-resscn 9561 ax-1cn 9562 ax-icn 9563 ax-addcl 9564 ax-addrcl 9565 ax-mulcl 9566 ax-mulrcl 9567 ax-mulcom 9568 ax-addass 9569 ax-mulass 9570 ax-distr 9571 ax-i2m1 9572 ax-1ne0 9573 ax-1rid 9574 ax-rnegex 9575 ax-rrecex 9576 ax-cnre 9577 ax-pre-lttri 9578 ax-pre-lttrn 9579 ax-pre-ltadd 9580 ax-pre-mulgt0 9581 ax-pre-sup 9582

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2822 df-rex 2823 df-reu 2824 df-rmo 2825 df-rab 2826 df-v 3120 df-sbc 3337 df-csb 3441 df-dif 3484 df-un 3486 df-in 3488 df-ss 3495 df-pss 3497 df-nul 3791 df-if 3946 df-pw 4018 df-sn 4034 df-pr 4036 df-tp 4038 df-op 4040 df-uni 4252 df-int 4289 df-iun 4333 df-br 4454 df-opab 4512 df-mpt 4513 df-tr 4547 df-eprel 4797 df-id 4801 df-po 4806 df-so 4807 df-fr 4844 df-se 4845 df-we 4846 df-ord 4887 df-on 4888 df-lim 4889 df-suc 4890 df-xp 5011 df-rel 5012 df-cnv 5013 df-co 5014 df-dm 5015 df-rn 5016 df-res 5017 df-ima 5018 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-isom 5603 df-riota 6256 df-ov 6298 df-oprab 6299 df-mpt2 6300 df-om 6696 df-1st 6795 df-2nd 6796 df-recs 7054 df-rdg 7088 df-1o 7142 df-2o 7143 df-oadd 7146 df-er 7323 df-map 7434 df-en 7529 df-dom 7530 df-sdom 7531 df-fin 7532 df-sup 7913 df-oi 7947 df-card 8332 df-cda 8560 df-pnf 9642 df-mnf 9643 df-xr 9644 df-ltxr 9645 df-le 9646 df-sub 9819 df-neg 9820 df-div 10219 df-nn 10549 df-2 10606 df-3 10607 df-n0 10808 df-z 10877 df-uz 11095 df-rp 11233 df-fz 11685 df-fzo 11805 df-seq 12088 df-exp 12147 df-hash 12386 df-cj 12911 df-re 12912 df-im 12913 df-sqrt 13047 df-abs 13048 df-clim 13290 df-sum 13488

This theorem is referenced by: incexc 13628

W3C validator