incexclem - Metamath Proof Explorer

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

Theorem incexclem 13660

Description: Lemma for incexc 13661. (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 2514	. . . . . . . . . 10
4	3	ineq2d 3696	. . . . . . . . 9
5		in0 3820	. . . . . . . . 9
6	4, 5	syl6eq 2514	. . . . . . . 8
7	6	fveq2d 5876	. . . . . . 7
8		hash0 12440	. . . . . . 7
9	7, 8	syl6eq 2514	. . . . . 6
10	9	oveq2d 6312	. . . . 5
11		pweq 4018	. . . . . . 7
12		pw0 4179	. . . . . . 7
13	11, 12	syl6eq 2514	. . . . . 6
14	13	sumeq1d 13535	. . . . 5
15	10, 14	eqeq12d 2479	. . . 4
16	15	ralbidv 2896	. . 3
17		unieq 4259	. . . . . . . 8
18	17	ineq2d 3696	. . . . . . 7
19	18	fveq2d 5876	. . . . . 6
20	19	oveq2d 6312	. . . . 5
21		pweq 4018	. . . . . 6
22	21	sumeq1d 13535	. . . . 5
23	20, 22	eqeq12d 2479	. . . 4
24	23	ralbidv 2896	. . 3
25		unieq 4259	. . . . . . . . 9
26		uniun 4270	. . . . . . . . . 10
27		vex 3112	. . . . . . . . . . . 12
28	27	unisn 4266	. . . . . . . . . . 11
29	28	uneq2i 3651	. . . . . . . . . 10
30	26, 29	eqtri 2486	. . . . . . . . 9
31	25, 30	syl6eq 2514	. . . . . . . 8
32	31	ineq2d 3696	. . . . . . 7
33	32	fveq2d 5876	. . . . . 6
34	33	oveq2d 6312	. . . . 5
35		pweq 4018	. . . . . 6
36	35	sumeq1d 13535	. . . . 5
37	34, 36	eqeq12d 2479	. . . 4
38	37	ralbidv 2896	. . 3
39		unieq 4259	. . . . . . . 8
40	39	ineq2d 3696	. . . . . . 7
41	40	fveq2d 5876	. . . . . 6
42	41	oveq2d 6312	. . . . 5
43		pweq 4018	. . . . . 6
44	43	sumeq1d 13535	. . . . 5
45	42, 44	eqeq12d 2479	. . . 4
46	45	ralbidv 2896	. . 3
47		hashcl 12431	. . . . . . 7
48	47	nn0cnd 10875	. . . . . 6
49	48	mulid2d 9631	. . . . 5
50		0ex 4587	. . . . . 6
51	49, 48	eqeltrd 2545	. . . . . 6
52		fveq2 5872	. . . . . . . . . . 11
53	52, 8	syl6eq 2514	. . . . . . . . . 10
54	53	oveq2d 6312	. . . . . . . . 9
55		neg1cn 10660	. . . . . . . . . 10
56		exp0 12173	. . . . . . . . . 10
57	55, 56	ax-mp 5	. . . . . . . . 9
58	54, 57	syl6eq 2514	. . . . . . . 8
59		rint0 4329	. . . . . . . . 9
60	59	fveq2d 5876	. . . . . . . 8
61	58, 60	oveq12d 6314	. . . . . . 7
62	61	sumsn 13575	. . . . . 6 $/\$
63	50, 51, 62	sylancr 663	. . . . 5
64	48	subid1d 9939	. . . . 5
65	49, 63, 64	3eqtr4rd 2509	. . . 4
66	65	rgen 2817	. . 3
67		fveq2 5872	. . . . . . . . . . . 12
68		ineq1 3689	. . . . . . . . . . . . 13
69	68	fveq2d 5876	. . . . . . . . . . . 12
70	67, 69	oveq12d 6314	. . . . . . . . . . 11
71		simpl 457	. . . . . . . . . . . . . . 15 $/\$
72	71	ineq1d 3695	. . . . . . . . . . . . . 14 $/\$
73	72	fveq2d 5876	. . . . . . . . . . . . 13 $/\$
74	73	oveq2d 6312	. . . . . . . . . . . 12 $/\$
75	74	sumeq2dv 13537	. . . . . . . . . . 11
76	70, 75	eqeq12d 2479	. . . . . . . . . 10
77	76	rspcva 3208	. . . . . . . . 9 $/\$
78	77	adantll 713	. . . . . . . 8 $/\$ $/\$ $/\$
79		simpr 461	. . . . . . . . . 10 $/\$ $/\$
80		inss1 3714	. . . . . . . . . 10
81		ssfi 7759	. . . . . . . . . 10 $/\$
82	79, 80, 81	sylancl 662	. . . . . . . . 9 $/\$ $/\$
83		fveq2 5872	. . . . . . . . . . . 12
84		ineq1 3689	. . . . . . . . . . . . . 14
85		in32 3706	. . . . . . . . . . . . . . 15
86		inass 3704	. . . . . . . . . . . . . . 15
87	85, 86	eqtri 2486	. . . . . . . . . . . . . 14
88	84, 87	syl6eq 2514	. . . . . . . . . . . . 13
89	88	fveq2d 5876	. . . . . . . . . . . 12
90	83, 89	oveq12d 6314	. . . . . . . . . . 11
91		ineq1 3689	. . . . . . . . . . . . . . 15
92		in32 3706	. . . . . . . . . . . . . . . 16
93		inass 3704	. . . . . . . . . . . . . . . 16
94	92, 93	eqtri 2486	. . . . . . . . . . . . . . 15
95	91, 94	syl6eq 2514	. . . . . . . . . . . . . 14
96	95	fveq2d 5876	. . . . . . . . . . . . 13
97	96	oveq2d 6312	. . . . . . . . . . . 12
98	97	sumeq2sdv 13538	. . . . . . . . . . 11
99	90, 98	eqeq12d 2479	. . . . . . . . . 10
100	99	rspcva 3208	. . . . . . . . 9 $/\$
101	82, 100	sylan 471	. . . . . . . 8 $/\$ $/\$ $/\$
102	78, 101	oveq12d 6314	. . . . . . 7 $/\$ $/\$ $/\$
103		inss1 3714	. . . . . . . . . . . . . 14
104		ssfi 7759	. . . . . . . . . . . . . 14 $/\$
105	79, 103, 104	sylancl 662	. . . . . . . . . . . . 13 $/\$ $/\$
106		hashun3 12455	. . . . . . . . . . . . 13 $/\$
107	105, 82, 106	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$
108		indi 3751	. . . . . . . . . . . . 13
109	108	fveq2i 5875	. . . . . . . . . . . 12
110		inindi 3711	. . . . . . . . . . . . . 14
111	110	fveq2i 5875	. . . . . . . . . . . . 13
112	111	oveq2i 6307	. . . . . . . . . . . 12
113	107, 109, 112	3eqtr4g 2523	. . . . . . . . . . 11 $/\$ $/\$
114		hashcl 12431	. . . . . . . . . . . . . 14
115	105, 114	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$
116	115	nn0cnd 10875	. . . . . . . . . . . 12 $/\$ $/\$
117		hashcl 12431	. . . . . . . . . . . . . 14
118	82, 117	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$
119	118	nn0cnd 10875	. . . . . . . . . . . 12 $/\$ $/\$
120		inss1 3714	. . . . . . . . . . . . . . 15
121		ssfi 7759	. . . . . . . . . . . . . . 15 $/\$
122	79, 120, 121	sylancl 662	. . . . . . . . . . . . . 14 $/\$ $/\$
123		hashcl 12431	. . . . . . . . . . . . . 14
124	122, 123	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$
125	124	nn0cnd 10875	. . . . . . . . . . . 12 $/\$ $/\$
126	116, 119, 125	addsubassd 9970	. . . . . . . . . . 11 $/\$ $/\$
127	113, 126	eqtrd 2498	. . . . . . . . . 10 $/\$ $/\$
128	127	oveq2d 6312	. . . . . . . . 9 $/\$ $/\$
129		hashcl 12431	. . . . . . . . . . . 12
130	129	adantl 466	. . . . . . . . . . 11 $/\$ $/\$
131	130	nn0cnd 10875	. . . . . . . . . 10 $/\$ $/\$
132	119, 125	subcld 9950	. . . . . . . . . 10 $/\$ $/\$
133	131, 116, 132	subsub4d 9981	. . . . . . . . 9 $/\$ $/\$
134	128, 133	eqtr4d 2501	. . . . . . . 8 $/\$ $/\$
135	134	adantr 465	. . . . . . 7 $/\$ $/\$ $/\$
136		disjdif 3903	. . . . . . . . . . 11 $\$
137	136	a1i 11	. . . . . . . . . 10 $/\$ $/\$ $\$
138		ssun1 3663	. . . . . . . . . . . . . 14
139		sspwb 4705	. . . . . . . . . . . . . 14
140	138, 139	mpbi 208	. . . . . . . . . . . . 13
141		undif 3911	. . . . . . . . . . . . 13 $\$
142	140, 141	mpbi 208	. . . . . . . . . . . 12 $\$
143	142	eqcomi 2470	. . . . . . . . . . 11 $\$
144	143	a1i 11	. . . . . . . . . 10 $/\$ $/\$ $\$
145		simpll 753	. . . . . . . . . . . 12 $/\$ $/\$
146		snfi 7615	. . . . . . . . . . . 12
147		unfi 7805	. . . . . . . . . . . 12 $/\$
148	145, 146, 147	sylancl 662	. . . . . . . . . . 11 $/\$ $/\$
149		pwfi 7833	. . . . . . . . . . 11
150	148, 149	sylib 196	. . . . . . . . . 10 $/\$ $/\$
151	55	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152		elpwi 4024	. . . . . . . . . . . . . 14
153		ssfi 7759	. . . . . . . . . . . . . 14 $/\$
154	148, 152, 153	syl2an 477	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
155		hashcl 12431	. . . . . . . . . . . . 13
156	154, 155	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
157	151, 156	expcld 12313	. . . . . . . . . . 11 $/\$ $/\$ $/\$
158		simplr 755	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
159		inss1 3714	. . . . . . . . . . . . . 14
160		ssfi 7759	. . . . . . . . . . . . . 14 $/\$
161	158, 159, 160	sylancl 662	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
162		hashcl 12431	. . . . . . . . . . . . 13
163	161, 162	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
164	163	nn0cnd 10875	. . . . . . . . . . 11 $/\$ $/\$ $/\$
165	157, 164	mulcld 9633	. . . . . . . . . 10 $/\$ $/\$ $/\$
166	137, 144, 150, 165	fsumsplit 13574	. . . . . . . . 9 $/\$ $/\$ $\$
167		fveq2 5872	. . . . . . . . . . . . . 14
168	167	oveq2d 6312	. . . . . . . . . . . . 13
169		inteq 4291	. . . . . . . . . . . . . . . 16
170	27	intunsn 4328	. . . . . . . . . . . . . . . 16
171	169, 170	syl6eq 2514	. . . . . . . . . . . . . . 15
172	171	ineq2d 3696	. . . . . . . . . . . . . 14
173	172	fveq2d 5876	. . . . . . . . . . . . 13
174	168, 173	oveq12d 6314	. . . . . . . . . . . 12
175		pwfi 7833	. . . . . . . . . . . . 13
176	145, 175	sylib 196	. . . . . . . . . . . 12 $/\$ $/\$
177		eqid 2457	. . . . . . . . . . . . 13
178		elpwi 4024	. . . . . . . . . . . . . . . . 17
179	178	adantl 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
180		unss1 3669	. . . . . . . . . . . . . . . 16
181	179, 180	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
182		vex 3112	. . . . . . . . . . . . . . . . 17
183		snex 4697	. . . . . . . . . . . . . . . . 17
184	182, 183	unex 6597	. . . . . . . . . . . . . . . 16
185	184	elpw 4021	. . . . . . . . . . . . . . 15
186	181, 185	sylibr 212	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
187		simpllr 760	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
188		elpwi 4024	. . . . . . . . . . . . . . . 16
189		ssun2 3664	. . . . . . . . . . . . . . . . . . 19
190	27	snss 4156	. . . . . . . . . . . . . . . . . . 19
191	189, 190	mpbir 209	. . . . . . . . . . . . . . . . . 18
192	191	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
193		ssel 3493	. . . . . . . . . . . . . . . . 17
194	192, 193	syl5com 30	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
195	188, 194	syl5 32	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
196	187, 195	mtod 177	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
197	186, 196	eldifd 3482	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
198		eldifi 3622	. . . . . . . . . . . . . . . . . 18 $\$
199	198	adantl 466	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
200	199	elpwid 4025	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
201		uncom 3644	. . . . . . . . . . . . . . . 16
202	200, 201	syl6sseq 3545	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
203		ssundif 3914	. . . . . . . . . . . . . . 15 $\$
204	202, 203	sylib 196	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
205		vex 3112	. . . . . . . . . . . . . . 15
206	205	elpw2 4620	. . . . . . . . . . . . . 14 $\$ $\$
207	204, 206	sylibr 212	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
208		elpwunsn 4073	. . . . . . . . . . . . . . . . . . 19 $\$
209	208	ad2antll 728	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$
210	209	snssd 4177	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\$
211		ssequn2 3673	. . . . . . . . . . . . . . . . 17
212	210, 211	sylib 196	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $\$
213	212	eqcomd 2465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$
214		uneq1 3647	. . . . . . . . . . . . . . . . 17 $\$ $\$
215		undif1 3906	. . . . . . . . . . . . . . . . 17 $\$
216	214, 215	syl6eq 2514	. . . . . . . . . . . . . . . 16 $\$
217	216	eqeq2d 2471	. . . . . . . . . . . . . . 15 $\$
218	213, 217	syl5ibrcom 222	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $\$ $\$
219	178	ad2antrl 727	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$
220		simpllr 760	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$
221	219, 220	ssneldd 3502	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\$
222		difsnb 4174	. . . . . . . . . . . . . . . . 17 $\$
223	221, 222	sylib 196	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $\$ $\$
224	223	eqcomd 2465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$ $\$
225		difeq1 3611	. . . . . . . . . . . . . . . . 17 $\$ $\$
226		difun2 3910	. . . . . . . . . . . . . . . . 17 $\$ $\$
227	225, 226	syl6eq 2514	. . . . . . . . . . . . . . . 16 $\$ $\$
228	227	eqeq2d 2471	. . . . . . . . . . . . . . 15 $\$ $\$
229	224, 228	syl5ibrcom 222	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $\$ $\$
230	218, 229	impbid 191	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\$ $\$
231	177, 197, 207, 230	f1o2d 6526	. . . . . . . . . . . 12 $/\$ $/\$ $\$
232		uneq1 3647	. . . . . . . . . . . . . 14
233		vex 3112	. . . . . . . . . . . . . . 15
234	233, 183	unex 6597	. . . . . . . . . . . . . 14
235	232, 177, 234	fvmpt 5956	. . . . . . . . . . . . 13
236	235	adantl 466	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
237	198, 165	sylan2 474	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
238	174, 176, 231, 236, 237	fsumf1o 13557	. . . . . . . . . . 11 $/\$ $/\$ $\$
239		uneq1 3647	. . . . . . . . . . . . . . . 16
240	239	fveq2d 5876	. . . . . . . . . . . . . . 15
241	240	oveq2d 6312	. . . . . . . . . . . . . 14
242		inteq 4291	. . . . . . . . . . . . . . . . 17
243	242	ineq1d 3695	. . . . . . . . . . . . . . . 16
244	243	ineq2d 3696	. . . . . . . . . . . . . . 15
245	244	fveq2d 5876	. . . . . . . . . . . . . 14
246	241, 245	oveq12d 6314	. . . . . . . . . . . . 13
247	246	cbvsumv 13530	. . . . . . . . . . . 12
248		elpwi 4024	. . . . . . . . . . . . . . . . . . . 20
249		ssfi 7759	. . . . . . . . . . . . . . . . . . . 20 $/\$
250	145, 248, 249	syl2an 477	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
251	248	adantl 466	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
252		simpllr 760	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
253	251, 252	ssneldd 3502	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
254		hashunsng 12463	. . . . . . . . . . . . . . . . . . . 20 $/\$
255	27, 254	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 $/\$
256	250, 253, 255	syl2anc 661	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
257	256	oveq2d 6312	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
258	55	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
259	250, 155	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
260	258, 259	expp1d 12314	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
261	257, 260	eqtrd 2498	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
262	140	sseli 3495	. . . . . . . . . . . . . . . . . 18
263	262, 157	sylan2 474	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
264	258, 263	mulcomd 9634	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
265	263	mulm1d 10029	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
266	261, 264, 265	3eqtr2d 2504	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
267	266	oveq1d 6311	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
268		inss1 3714	. . . . . . . . . . . . . . . . . . 19
269		ssfi 7759	. . . . . . . . . . . . . . . . . . 19 $/\$
270	158, 268, 269	sylancl 662	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
271		hashcl 12431	. . . . . . . . . . . . . . . . . 18
272	270, 271	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
273	272	nn0cnd 10875	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
274	262, 273	sylan2 474	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
275	263, 274	mulneg1d 10030	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
276	267, 275	eqtrd 2498	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
277	276	sumeq2dv 13537	. . . . . . . . . . . 12 $/\$ $/\$
278	247, 277	syl5eq 2510	. . . . . . . . . . 11 $/\$ $/\$
279	157, 273	mulcld 9633	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
280	262, 279	sylan2 474	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
281	176, 280	fsumneg 13614	. . . . . . . . . . 11 $/\$ $/\$
282	238, 278, 281	3eqtrd 2502	. . . . . . . . . 10 $/\$ $/\$ $\$
283	282	oveq2d 6312	. . . . . . . . 9 $/\$ $/\$ $\$
284	140	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
285	284	sselda 3499	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
286	285, 165	syldan 470	. . . . . . . . . . 11 $/\$ $/\$ $/\$
287	176, 286	fsumcl 13567	. . . . . . . . . 10 $/\$ $/\$
288	285, 279	syldan 470	. . . . . . . . . . 11 $/\$ $/\$ $/\$
289	176, 288	fsumcl 13567	. . . . . . . . . 10 $/\$ $/\$
290	287, 289	negsubd 9956	. . . . . . . . 9 $/\$ $/\$
291	166, 283, 290	3eqtrd 2502	. . . . . . . 8 $/\$ $/\$
292	291	adantr 465	. . . . . . 7 $/\$ $/\$ $/\$
293	102, 135, 292	3eqtr4d 2508	. . . . . 6 $/\$ $/\$ $/\$
294	293	ex 434	. . . . 5 $/\$ $/\$
295	294	ralrimdva 2875	. . . 4 $/\$
296		ineq1 3689	. . . . . . . 8
297	296	fveq2d 5876	. . . . . . 7
298	67, 297	oveq12d 6314	. . . . . 6
299		ineq1 3689	. . . . . . . . 9
300	299	fveq2d 5876	. . . . . . . 8
301	300	oveq2d 6312	. . . . . . 7
302	301	sumeq2sdv 13538	. . . . . 6
303	298, 302	eqeq12d 2479	. . . . 5
304	303	cbvralv 3084	. . . 4
305	295, 304	syl6ibr 227	. . 3 $/\$
306	16, 24, 38, 46, 66, 305	findcard2s 7779	. 2
307		fveq2 5872	. . . . 5
308		ineq1 3689	. . . . . 6
309	308	fveq2d 5876	. . . . 5
310	307, 309	oveq12d 6314	. . . 4
311		simpl 457	. . . . . . . 8 $/\$
312	311	ineq1d 3695	. . . . . . 7 $/\$
313	312	fveq2d 5876	. . . . . 6 $/\$
314	313	oveq2d 6312	. . . . 5 $/\$
315	314	sumeq2dv 13537	. . . 4
316	310, 315	eqeq12d 2479	. . 3
317	316	rspccva 3209	. 2 $/\$
318	306, 317	sylan 471	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 369

wceq 1395

wcel 1819

wral 2807

cvv 3109 $\$ cdif 3468

cun 3469

cin 3470

wss 3471

c0 3793

cpw 4015

csn 4032

cuni 4251

cint 4288

cmpt 4515

cfv 5594 (class class class)co 6296

cfn 7535

cc 9507

cc0 9509

c1 9510

caddc 9512

cmul 9514

cmin 9824

cneg 9825

cn0 10816

cexp 12169

chash 12408

csu 13520

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-inf2 8075 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-fal 1401 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-se 4848 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 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 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6700 df-1st 6799 df-2nd 6800 df-recs 7060 df-rdg 7094 df-1o 7148 df-2o 7149 df-oadd 7152 df-er 7329 df-map 7440 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-sup 7919 df-oi 7953 df-card 8337 df-cda 8565 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-2 10615 df-3 10616 df-n0 10817 df-z 10886 df-uz 11107 df-rp 11246 df-fz 11698 df-fzo 11822 df-seq 12111 df-exp 12170 df-hash 12409 df-cj 12944 df-re 12945 df-im 12946 df-sqrt 13080 df-abs 13081 df-clim 13323 df-sum 13521

This theorem is referenced by: incexc 13661

W3C validator