incexclem - Metamath Proof Explorer

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

Theorem incexclem 13801

Description: Lemma for incexc 13802. (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 4201	. . . . . . . . . . 11
2		uni0 4220	. . . . . . . . . . 11
3	1, 2	syl6eq 2461	. . . . . . . . . 10
4	3	ineq2d 3643	. . . . . . . . 9
5		in0 3767	. . . . . . . . 9
6	4, 5	syl6eq 2461	. . . . . . . 8
7	6	fveq2d 5855	. . . . . . 7
8		hash0 12487	. . . . . . 7
9	7, 8	syl6eq 2461	. . . . . 6
10	9	oveq2d 6296	. . . . 5
11		pweq 3960	. . . . . . 7
12		pw0 4121	. . . . . . 7
13	11, 12	syl6eq 2461	. . . . . 6
14	13	sumeq1d 13674	. . . . 5
15	10, 14	eqeq12d 2426	. . . 4
16	15	ralbidv 2845	. . 3
17		unieq 4201	. . . . . . . 8
18	17	ineq2d 3643	. . . . . . 7
19	18	fveq2d 5855	. . . . . 6
20	19	oveq2d 6296	. . . . 5
21		pweq 3960	. . . . . 6
22	21	sumeq1d 13674	. . . . 5
23	20, 22	eqeq12d 2426	. . . 4
24	23	ralbidv 2845	. . 3
25		unieq 4201	. . . . . . . . 9
26		uniun 4212	. . . . . . . . . 10
27		vex 3064	. . . . . . . . . . . 12
28	27	unisn 4208	. . . . . . . . . . 11
29	28	uneq2i 3596	. . . . . . . . . 10
30	26, 29	eqtri 2433	. . . . . . . . 9
31	25, 30	syl6eq 2461	. . . . . . . 8
32	31	ineq2d 3643	. . . . . . 7
33	32	fveq2d 5855	. . . . . 6
34	33	oveq2d 6296	. . . . 5
35		pweq 3960	. . . . . 6
36	35	sumeq1d 13674	. . . . 5
37	34, 36	eqeq12d 2426	. . . 4
38	37	ralbidv 2845	. . 3
39		unieq 4201	. . . . . . . 8
40	39	ineq2d 3643	. . . . . . 7
41	40	fveq2d 5855	. . . . . 6
42	41	oveq2d 6296	. . . . 5
43		pweq 3960	. . . . . 6
44	43	sumeq1d 13674	. . . . 5
45	42, 44	eqeq12d 2426	. . . 4
46	45	ralbidv 2845	. . 3
47		hashcl 12477	. . . . . . 7
48	47	nn0cnd 10897	. . . . . 6
49	48	mulid2d 9646	. . . . 5
50		0ex 4528	. . . . . 6
51	49, 48	eqeltrd 2492	. . . . . 6
52		fveq2 5851	. . . . . . . . . . 11
53	52, 8	syl6eq 2461	. . . . . . . . . 10
54	53	oveq2d 6296	. . . . . . . . 9
55		neg1cn 10682	. . . . . . . . . 10
56		exp0 12216	. . . . . . . . . 10
57	55, 56	ax-mp 5	. . . . . . . . 9
58	54, 57	syl6eq 2461	. . . . . . . 8
59		rint0 4270	. . . . . . . . 9
60	59	fveq2d 5855	. . . . . . . 8
61	58, 60	oveq12d 6298	. . . . . . 7
62	61	sumsn 13714	. . . . . 6 $/\$
63	50, 51, 62	sylancr 663	. . . . 5
64	48	subid1d 9958	. . . . 5
65	49, 63, 64	3eqtr4rd 2456	. . . 4
66	65	rgen 2766	. . 3
67		fveq2 5851	. . . . . . . . . . . 12
68		ineq1 3636	. . . . . . . . . . . . 13
69	68	fveq2d 5855	. . . . . . . . . . . 12
70	67, 69	oveq12d 6298	. . . . . . . . . . 11
71		simpl 457	. . . . . . . . . . . . . . 15 $/\$
72	71	ineq1d 3642	. . . . . . . . . . . . . 14 $/\$
73	72	fveq2d 5855	. . . . . . . . . . . . 13 $/\$
74	73	oveq2d 6296	. . . . . . . . . . . 12 $/\$
75	74	sumeq2dv 13676	. . . . . . . . . . 11
76	70, 75	eqeq12d 2426	. . . . . . . . . 10
77	76	rspcva 3160	. . . . . . . . 9 $/\$
78	77	adantll 714	. . . . . . . 8 $/\$ $/\$ $/\$
79		simpr 461	. . . . . . . . . 10 $/\$ $/\$
80		inss1 3661	. . . . . . . . . 10
81		ssfi 7777	. . . . . . . . . 10 $/\$
82	79, 80, 81	sylancl 662	. . . . . . . . 9 $/\$ $/\$
83		fveq2 5851	. . . . . . . . . . . 12
84		ineq1 3636	. . . . . . . . . . . . . 14
85		in32 3653	. . . . . . . . . . . . . . 15
86		inass 3651	. . . . . . . . . . . . . . 15
87	85, 86	eqtri 2433	. . . . . . . . . . . . . 14
88	84, 87	syl6eq 2461	. . . . . . . . . . . . 13
89	88	fveq2d 5855	. . . . . . . . . . . 12
90	83, 89	oveq12d 6298	. . . . . . . . . . 11
91		ineq1 3636	. . . . . . . . . . . . . . 15
92		in32 3653	. . . . . . . . . . . . . . . 16
93		inass 3651	. . . . . . . . . . . . . . . 16
94	92, 93	eqtri 2433	. . . . . . . . . . . . . . 15
95	91, 94	syl6eq 2461	. . . . . . . . . . . . . 14
96	95	fveq2d 5855	. . . . . . . . . . . . 13
97	96	oveq2d 6296	. . . . . . . . . . . 12
98	97	sumeq2sdv 13677	. . . . . . . . . . 11
99	90, 98	eqeq12d 2426	. . . . . . . . . 10
100	99	rspcva 3160	. . . . . . . . 9 $/\$
101	82, 100	sylan 471	. . . . . . . 8 $/\$ $/\$ $/\$
102	78, 101	oveq12d 6298	. . . . . . 7 $/\$ $/\$ $/\$
103		inss1 3661	. . . . . . . . . . . . . 14
104		ssfi 7777	. . . . . . . . . . . . . 14 $/\$
105	79, 103, 104	sylancl 662	. . . . . . . . . . . . 13 $/\$ $/\$
106		hashun3 12502	. . . . . . . . . . . . 13 $/\$
107	105, 82, 106	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$
108		indi 3698	. . . . . . . . . . . . 13
109	108	fveq2i 5854	. . . . . . . . . . . 12
110		inindi 3658	. . . . . . . . . . . . . 14
111	110	fveq2i 5854	. . . . . . . . . . . . 13
112	111	oveq2i 6291	. . . . . . . . . . . 12
113	107, 109, 112	3eqtr4g 2470	. . . . . . . . . . 11 $/\$ $/\$
114		hashcl 12477	. . . . . . . . . . . . . 14
115	105, 114	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
116	115	nn0cnd 10897	. . . . . . . . . . . 12 $/\$ $/\$
117		hashcl 12477	. . . . . . . . . . . . . 14
118	82, 117	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
119	118	nn0cnd 10897	. . . . . . . . . . . 12 $/\$ $/\$
120		inss1 3661	. . . . . . . . . . . . . . 15
121		ssfi 7777	. . . . . . . . . . . . . . 15 $/\$
122	79, 120, 121	sylancl 662	. . . . . . . . . . . . . 14 $/\$ $/\$
123		hashcl 12477	. . . . . . . . . . . . . 14
124	122, 123	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
125	124	nn0cnd 10897	. . . . . . . . . . . 12 $/\$ $/\$
126	116, 119, 125	addsubassd 9989	. . . . . . . . . . 11 $/\$ $/\$
127	113, 126	eqtrd 2445	. . . . . . . . . 10 $/\$ $/\$
128	127	oveq2d 6296	. . . . . . . . 9 $/\$ $/\$
129		hashcl 12477	. . . . . . . . . . . 12
130	129	adantl 466	. . . . . . . . . . 11 $/\$ $/\$
131	130	nn0cnd 10897	. . . . . . . . . 10 $/\$ $/\$
132	119, 125	subcld 9969	. . . . . . . . . 10 $/\$ $/\$
133	131, 116, 132	subsub4d 10000	. . . . . . . . 9 $/\$ $/\$
134	128, 133	eqtr4d 2448	. . . . . . . 8 $/\$ $/\$
135	134	adantr 465	. . . . . . 7 $/\$ $/\$ $/\$
136		disjdif 3846	. . . . . . . . . . 11 $\$
137	136	a1i 11	. . . . . . . . . 10 $/\$ $/\$ $\$
138		ssun1 3608	. . . . . . . . . . . . . 14
139		sspwb 4642	. . . . . . . . . . . . . 14
140	138, 139	mpbi 210	. . . . . . . . . . . . 13
141		undif 3854	. . . . . . . . . . . . 13 $\$
142	140, 141	mpbi 210	. . . . . . . . . . . 12 $\$
143	142	eqcomi 2417	. . . . . . . . . . 11 $\$
144	143	a1i 11	. . . . . . . . . 10 $/\$ $/\$ $\$
145		simpll 754	. . . . . . . . . . . 12 $/\$ $/\$
146		snfi 7636	. . . . . . . . . . . 12
147		unfi 7823	. . . . . . . . . . . 12 $/\$
148	145, 146, 147	sylancl 662	. . . . . . . . . . 11 $/\$ $/\$
149		pwfi 7851	. . . . . . . . . . 11
150	148, 149	sylib 198	. . . . . . . . . 10 $/\$ $/\$
151	55	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152		elpwi 3966	. . . . . . . . . . . . . 14
153		ssfi 7777	. . . . . . . . . . . . . 14 $/\$
154	148, 152, 153	syl2an 477	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
155		hashcl 12477	. . . . . . . . . . . . 13
156	154, 155	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
157	151, 156	expcld 12356	. . . . . . . . . . 11 $/\$ $/\$ $/\$
158		simplr 756	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
159		inss1 3661	. . . . . . . . . . . . . 14
160		ssfi 7777	. . . . . . . . . . . . . 14 $/\$
161	158, 159, 160	sylancl 662	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
162		hashcl 12477	. . . . . . . . . . . . 13
163	161, 162	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
164	163	nn0cnd 10897	. . . . . . . . . . 11 $/\$ $/\$ $/\$
165	157, 164	mulcld 9648	. . . . . . . . . 10 $/\$ $/\$ $/\$
166	137, 144, 150, 165	fsumsplit 13713	. . . . . . . . 9 $/\$ $/\$ $\$
167		fveq2 5851	. . . . . . . . . . . . . 14
168	167	oveq2d 6296	. . . . . . . . . . . . 13
169		inteq 4232	. . . . . . . . . . . . . . . 16
170	27	intunsn 4269	. . . . . . . . . . . . . . . 16
171	169, 170	syl6eq 2461	. . . . . . . . . . . . . . 15
172	171	ineq2d 3643	. . . . . . . . . . . . . 14
173	172	fveq2d 5855	. . . . . . . . . . . . 13
174	168, 173	oveq12d 6298	. . . . . . . . . . . 12
175		pwfi 7851	. . . . . . . . . . . . 13
176	145, 175	sylib 198	. . . . . . . . . . . 12 $/\$ $/\$
177		eqid 2404	. . . . . . . . . . . . 13
178		elpwi 3966	. . . . . . . . . . . . . . . . 17
179	178	adantl 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
180		unss1 3614	. . . . . . . . . . . . . . . 16
181	179, 180	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
182		vex 3064	. . . . . . . . . . . . . . . . 17
183		snex 4634	. . . . . . . . . . . . . . . . 17
184	182, 183	unex 6582	. . . . . . . . . . . . . . . 16
185	184	elpw 3963	. . . . . . . . . . . . . . 15
186	181, 185	sylibr 214	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
187		simpllr 763	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
188		elpwi 3966	. . . . . . . . . . . . . . . 16
189		ssun2 3609	. . . . . . . . . . . . . . . . . . 19
190	27	snss 4098	. . . . . . . . . . . . . . . . . . 19
191	189, 190	mpbir 211	. . . . . . . . . . . . . . . . . 18
192	191	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
193		ssel 3438	. . . . . . . . . . . . . . . . 17
194	192, 193	syl5com 30	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
195	188, 194	syl5 32	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
196	187, 195	mtod 179	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
197	186, 196	eldifd 3427	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
198		eldifi 3567	. . . . . . . . . . . . . . . . . 18 $\$
199	198	adantl 466	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
200	199	elpwid 3967	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
201		uncom 3589	. . . . . . . . . . . . . . . 16
202	200, 201	syl6sseq 3490	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
203		ssundif 3857	. . . . . . . . . . . . . . 15 $\$
204	202, 203	sylib 198	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
205		vex 3064	. . . . . . . . . . . . . . 15
206	205	elpw2 4560	. . . . . . . . . . . . . 14 $\$ $\$
207	204, 206	sylibr 214	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
208		elpwunsn 4015	. . . . . . . . . . . . . . . . . . 19 $\$
209	208	ad2antll 729	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$
210	209	snssd 4119	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\$
211		ssequn2 3618	. . . . . . . . . . . . . . . . 17
212	210, 211	sylib 198	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $\$
213	212	eqcomd 2412	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$
214		uneq1 3592	. . . . . . . . . . . . . . . . 17 $\$ $\$
215		undif1 3849	. . . . . . . . . . . . . . . . 17 $\$
216	214, 215	syl6eq 2461	. . . . . . . . . . . . . . . 16 $\$
217	216	eqeq2d 2418	. . . . . . . . . . . . . . 15 $\$
218	213, 217	syl5ibrcom 224	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $\$ $\$
219	178	ad2antrl 728	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$
220		simpllr 763	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$
221	219, 220	ssneldd 3447	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\$
222		difsnb 4116	. . . . . . . . . . . . . . . . 17 $\$
223	221, 222	sylib 198	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $\$ $\$
224	223	eqcomd 2412	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$ $\$
225		difeq1 3556	. . . . . . . . . . . . . . . . 17 $\$ $\$
226		difun2 3853	. . . . . . . . . . . . . . . . 17 $\$ $\$
227	225, 226	syl6eq 2461	. . . . . . . . . . . . . . . 16 $\$ $\$
228	227	eqeq2d 2418	. . . . . . . . . . . . . . 15 $\$ $\$
229	224, 228	syl5ibrcom 224	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $\$ $\$
230	218, 229	impbid 192	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\$ $\$
231	177, 197, 207, 230	f1o2d 6510	. . . . . . . . . . . 12 $/\$ $/\$ $\$
232		uneq1 3592	. . . . . . . . . . . . . 14
233		vex 3064	. . . . . . . . . . . . . . 15
234	233, 183	unex 6582	. . . . . . . . . . . . . 14
235	232, 177, 234	fvmpt 5934	. . . . . . . . . . . . 13
236	235	adantl 466	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
237	198, 165	sylan2 474	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
238	174, 176, 231, 236, 237	fsumf1o 13696	. . . . . . . . . . 11 $/\$ $/\$ $\$
239		uneq1 3592	. . . . . . . . . . . . . . . 16
240	239	fveq2d 5855	. . . . . . . . . . . . . . 15
241	240	oveq2d 6296	. . . . . . . . . . . . . 14
242		inteq 4232	. . . . . . . . . . . . . . . . 17
243	242	ineq1d 3642	. . . . . . . . . . . . . . . 16
244	243	ineq2d 3643	. . . . . . . . . . . . . . 15
245	244	fveq2d 5855	. . . . . . . . . . . . . 14
246	241, 245	oveq12d 6298	. . . . . . . . . . . . 13
247	246	cbvsumv 13669	. . . . . . . . . . . 12
248		elpwi 3966	. . . . . . . . . . . . . . . . . . . 20
249		ssfi 7777	. . . . . . . . . . . . . . . . . . . 20 $/\$
250	145, 248, 249	syl2an 477	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
251	248	adantl 466	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
252		simpllr 763	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
253	251, 252	ssneldd 3447	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
254		hashunsng 12510	. . . . . . . . . . . . . . . . . . . 20 $/\$
255	27, 254	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 $/\$
256	250, 253, 255	syl2anc 661	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
257	256	oveq2d 6296	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
258	55	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
259	250, 155	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
260	258, 259	expp1d 12357	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
261	257, 260	eqtrd 2445	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
262	140	sseli 3440	. . . . . . . . . . . . . . . . . 18
263	262, 157	sylan2 474	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
264	258, 263	mulcomd 9649	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
265	263	mulm1d 10051	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
266	261, 264, 265	3eqtr2d 2451	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
267	266	oveq1d 6295	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
268		inss1 3661	. . . . . . . . . . . . . . . . . . 19
269		ssfi 7777	. . . . . . . . . . . . . . . . . . 19 $/\$
270	158, 268, 269	sylancl 662	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
271		hashcl 12477	. . . . . . . . . . . . . . . . . 18
272	270, 271	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
273	272	nn0cnd 10897	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
274	262, 273	sylan2 474	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
275	263, 274	mulneg1d 10052	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
276	267, 275	eqtrd 2445	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
277	276	sumeq2dv 13676	. . . . . . . . . . . 12 $/\$ $/\$
278	247, 277	syl5eq 2457	. . . . . . . . . . 11 $/\$ $/\$
279	157, 273	mulcld 9648	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
280	262, 279	sylan2 474	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
281	176, 280	fsumneg 13755	. . . . . . . . . . 11 $/\$ $/\$
282	238, 278, 281	3eqtrd 2449	. . . . . . . . . 10 $/\$ $/\$ $\$
283	282	oveq2d 6296	. . . . . . . . 9 $/\$ $/\$ $\$
284	140	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
285	284	sselda 3444	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
286	285, 165	syldan 470	. . . . . . . . . . 11 $/\$ $/\$ $/\$
287	176, 286	fsumcl 13706	. . . . . . . . . 10 $/\$ $/\$
288	285, 279	syldan 470	. . . . . . . . . . 11 $/\$ $/\$ $/\$
289	176, 288	fsumcl 13706	. . . . . . . . . 10 $/\$ $/\$
290	287, 289	negsubd 9975	. . . . . . . . 9 $/\$ $/\$
291	166, 283, 290	3eqtrd 2449	. . . . . . . 8 $/\$ $/\$
292	291	adantr 465	. . . . . . 7 $/\$ $/\$ $/\$
293	102, 135, 292	3eqtr4d 2455	. . . . . 6 $/\$ $/\$ $/\$
294	293	ex 434	. . . . 5 $/\$ $/\$
295	294	ralrimdva 2824	. . . 4 $/\$
296		ineq1 3636	. . . . . . . 8
297	296	fveq2d 5855	. . . . . . 7
298	67, 297	oveq12d 6298	. . . . . 6
299		ineq1 3636	. . . . . . . . 9
300	299	fveq2d 5855	. . . . . . . 8
301	300	oveq2d 6296	. . . . . . 7
302	301	sumeq2sdv 13677	. . . . . 6
303	298, 302	eqeq12d 2426	. . . . 5
304	303	cbvralv 3036	. . . 4
305	295, 304	syl6ibr 229	. . 3 $/\$
306	16, 24, 38, 46, 66, 305	findcard2s 7797	. 2
307		fveq2 5851	. . . . 5
308		ineq1 3636	. . . . . 6
309	308	fveq2d 5855	. . . . 5
310	307, 309	oveq12d 6298	. . . 4
311		simpl 457	. . . . . . . 8 $/\$
312	311	ineq1d 3642	. . . . . . 7 $/\$
313	312	fveq2d 5855	. . . . . 6 $/\$
314	313	oveq2d 6296	. . . . 5 $/\$
315	314	sumeq2dv 13676	. . . 4
316	310, 315	eqeq12d 2426	. . 3
317	316	rspccva 3161	. 2 $/\$
318	306, 317	sylan 471	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 369

wceq 1407

wcel 1844

wral 2756

cvv 3061 $\$ cdif 3413

cun 3414

cin 3415

wss 3416

c0 3740

cpw 3957

csn 3974

cuni 4193

cint 4229

cmpt 4455

cfv 5571 (class class class)co 6280

cfn 7556

cc 9522

cc0 9524

c1 9525

caddc 9527

cmul 9529

cmin 9843

cneg 9844

cn0 10838

cexp 12212

chash 12454

csu 13659

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1641 ax-4 1654 ax-5 1727 ax-6 1773 ax-7 1816 ax-8 1846 ax-9 1848 ax-10 1863 ax-11 1868 ax-12 1880 ax-13 2028 ax-ext 2382 ax-rep 4509 ax-sep 4519 ax-nul 4527 ax-pow 4574 ax-pr 4632 ax-un 6576 ax-inf2 8093 ax-cnex 9580 ax-resscn 9581 ax-1cn 9582 ax-icn 9583 ax-addcl 9584 ax-addrcl 9585 ax-mulcl 9586 ax-mulrcl 9587 ax-mulcom 9588 ax-addass 9589 ax-mulass 9590 ax-distr 9591 ax-i2m1 9592 ax-1ne0 9593 ax-1rid 9594 ax-rnegex 9595 ax-rrecex 9596 ax-cnre 9597 ax-pre-lttri 9598 ax-pre-lttrn 9599 ax-pre-ltadd 9600 ax-pre-mulgt0 9601 ax-pre-sup 9602

This theorem depends on definitions: df-bi 187 df-or 370 df-an 371 df-3or 977 df-3an 978 df-tru 1410 df-fal 1413 df-ex 1636 df-nf 1640 df-sb 1766 df-eu 2244 df-mo 2245 df-clab 2390 df-cleq 2396 df-clel 2399 df-nfc 2554 df-ne 2602 df-nel 2603 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3063 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-pss 3432 df-nul 3741 df-if 3888 df-pw 3959 df-sn 3975 df-pr 3977 df-tp 3979 df-op 3981 df-uni 4194 df-int 4230 df-iun 4275 df-br 4398 df-opab 4456 df-mpt 4457 df-tr 4492 df-eprel 4736 df-id 4740 df-po 4746 df-so 4747 df-fr 4784 df-se 4785 df-we 4786 df-xp 4831 df-rel 4832 df-cnv 4833 df-co 4834 df-dm 4835 df-rn 4836 df-res 4837 df-ima 4838 df-pred 5369 df-ord 5415 df-on 5416 df-lim 5417 df-suc 5418 df-iota 5535 df-fun 5573 df-fn 5574 df-f 5575 df-f1 5576 df-fo 5577 df-f1o 5578 df-fv 5579 df-isom 5580 df-riota 6242 df-ov 6283 df-oprab 6284 df-mpt2 6285 df-om 6686 df-1st 6786 df-2nd 6787 df-wrecs 7015 df-recs 7077 df-rdg 7115 df-1o 7169 df-2o 7170 df-oadd 7173 df-er 7350 df-map 7461 df-en 7557 df-dom 7558 df-sdom 7559 df-fin 7560 df-sup 7937 df-oi 7971 df-card 8354 df-cda 8582 df-pnf 9662 df-mnf 9663 df-xr 9664 df-ltxr 9665 df-le 9666 df-sub 9845 df-neg 9846 df-div 10250 df-nn 10579 df-2 10637 df-3 10638 df-n0 10839 df-z 10908 df-uz 11130 df-rp 11268 df-fz 11729 df-fzo 11857 df-seq 12154 df-exp 12213 df-hash 12455 df-cj 13083 df-re 13084 df-im 13085 df-sqrt 13219 df-abs 13220 df-clim 13462 df-sum 13660

This theorem is referenced by: incexc 13802

W3C validator