incexclem - Metamath Proof Explorer

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

Theorem incexclem 13971

Description: Lemma for incexc 13972. (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 4198	. . . . . . . . . . 11
2		uni0 4217	. . . . . . . . . . 11
3	1, 2	syl6eq 2521	. . . . . . . . . 10
4	3	ineq2d 3625	. . . . . . . . 9
5		in0 3763	. . . . . . . . 9
6	4, 5	syl6eq 2521	. . . . . . . 8
7	6	fveq2d 5883	. . . . . . 7
8		hash0 12586	. . . . . . 7
9	7, 8	syl6eq 2521	. . . . . 6
10	9	oveq2d 6324	. . . . 5
11		pweq 3945	. . . . . . 7
12		pw0 4110	. . . . . . 7
13	11, 12	syl6eq 2521	. . . . . 6
14	13	sumeq1d 13844	. . . . 5
15	10, 14	eqeq12d 2486	. . . 4
16	15	ralbidv 2829	. . 3
17		unieq 4198	. . . . . . . 8
18	17	ineq2d 3625	. . . . . . 7
19	18	fveq2d 5883	. . . . . 6
20	19	oveq2d 6324	. . . . 5
21		pweq 3945	. . . . . 6
22	21	sumeq1d 13844	. . . . 5
23	20, 22	eqeq12d 2486	. . . 4
24	23	ralbidv 2829	. . 3
25		unieq 4198	. . . . . . . . 9
26		uniun 4209	. . . . . . . . . 10
27		vex 3034	. . . . . . . . . . . 12
28	27	unisn 4205	. . . . . . . . . . 11
29	28	uneq2i 3576	. . . . . . . . . 10
30	26, 29	eqtri 2493	. . . . . . . . 9
31	25, 30	syl6eq 2521	. . . . . . . 8
32	31	ineq2d 3625	. . . . . . 7
33	32	fveq2d 5883	. . . . . 6
34	33	oveq2d 6324	. . . . 5
35		pweq 3945	. . . . . 6
36	35	sumeq1d 13844	. . . . 5
37	34, 36	eqeq12d 2486	. . . 4
38	37	ralbidv 2829	. . 3
39		unieq 4198	. . . . . . . 8
40	39	ineq2d 3625	. . . . . . 7
41	40	fveq2d 5883	. . . . . 6
42	41	oveq2d 6324	. . . . 5
43		pweq 3945	. . . . . 6
44	43	sumeq1d 13844	. . . . 5
45	42, 44	eqeq12d 2486	. . . 4
46	45	ralbidv 2829	. . 3
47		hashcl 12576	. . . . . . 7
48	47	nn0cnd 10951	. . . . . 6
49	48	mulid2d 9679	. . . . 5
50		0ex 4528	. . . . . 6
51	49, 48	eqeltrd 2549	. . . . . 6
52		fveq2 5879	. . . . . . . . . . 11
53	52, 8	syl6eq 2521	. . . . . . . . . 10
54	53	oveq2d 6324	. . . . . . . . 9
55		neg1cn 10735	. . . . . . . . . 10
56		exp0 12314	. . . . . . . . . 10
57	55, 56	ax-mp 5	. . . . . . . . 9
58	54, 57	syl6eq 2521	. . . . . . . 8
59		rint0 4266	. . . . . . . . 9
60	59	fveq2d 5883	. . . . . . . 8
61	58, 60	oveq12d 6326	. . . . . . 7
62	61	sumsn 13884	. . . . . 6 $/\$
63	50, 51, 62	sylancr 676	. . . . 5
64	48	subid1d 9994	. . . . 5
65	49, 63, 64	3eqtr4rd 2516	. . . 4
66	65	rgen 2766	. . 3
67		fveq2 5879	. . . . . . . . . . . 12
68		ineq1 3618	. . . . . . . . . . . . 13
69	68	fveq2d 5883	. . . . . . . . . . . 12
70	67, 69	oveq12d 6326	. . . . . . . . . . 11
71		simpl 464	. . . . . . . . . . . . . . 15 $/\$
72	71	ineq1d 3624	. . . . . . . . . . . . . 14 $/\$
73	72	fveq2d 5883	. . . . . . . . . . . . 13 $/\$
74	73	oveq2d 6324	. . . . . . . . . . . 12 $/\$
75	74	sumeq2dv 13846	. . . . . . . . . . 11
76	70, 75	eqeq12d 2486	. . . . . . . . . 10
77	76	rspcva 3134	. . . . . . . . 9 $/\$
78	77	adantll 728	. . . . . . . 8 $/\$ $/\$ $/\$
79		simpr 468	. . . . . . . . . 10 $/\$ $/\$
80		inss1 3643	. . . . . . . . . 10
81		ssfi 7810	. . . . . . . . . 10 $/\$
82	79, 80, 81	sylancl 675	. . . . . . . . 9 $/\$ $/\$
83		fveq2 5879	. . . . . . . . . . . 12
84		ineq1 3618	. . . . . . . . . . . . . 14
85		in32 3635	. . . . . . . . . . . . . . 15
86		inass 3633	. . . . . . . . . . . . . . 15
87	85, 86	eqtri 2493	. . . . . . . . . . . . . 14
88	84, 87	syl6eq 2521	. . . . . . . . . . . . 13
89	88	fveq2d 5883	. . . . . . . . . . . 12
90	83, 89	oveq12d 6326	. . . . . . . . . . 11
91		ineq1 3618	. . . . . . . . . . . . . . 15
92		in32 3635	. . . . . . . . . . . . . . . 16
93		inass 3633	. . . . . . . . . . . . . . . 16
94	92, 93	eqtri 2493	. . . . . . . . . . . . . . 15
95	91, 94	syl6eq 2521	. . . . . . . . . . . . . 14
96	95	fveq2d 5883	. . . . . . . . . . . . 13
97	96	oveq2d 6324	. . . . . . . . . . . 12
98	97	sumeq2sdv 13847	. . . . . . . . . . 11
99	90, 98	eqeq12d 2486	. . . . . . . . . 10
100	99	rspcva 3134	. . . . . . . . 9 $/\$
101	82, 100	sylan 479	. . . . . . . 8 $/\$ $/\$ $/\$
102	78, 101	oveq12d 6326	. . . . . . 7 $/\$ $/\$ $/\$
103		inss1 3643	. . . . . . . . . . . . . 14
104		ssfi 7810	. . . . . . . . . . . . . 14 $/\$
105	79, 103, 104	sylancl 675	. . . . . . . . . . . . 13 $/\$ $/\$
106		hashun3 12601	. . . . . . . . . . . . 13 $/\$
107	105, 82, 106	syl2anc 673	. . . . . . . . . . . 12 $/\$ $/\$
108		indi 3680	. . . . . . . . . . . . 13
109	108	fveq2i 5882	. . . . . . . . . . . 12
110		inindi 3640	. . . . . . . . . . . . . 14
111	110	fveq2i 5882	. . . . . . . . . . . . 13
112	111	oveq2i 6319	. . . . . . . . . . . 12
113	107, 109, 112	3eqtr4g 2530	. . . . . . . . . . 11 $/\$ $/\$
114		hashcl 12576	. . . . . . . . . . . . . 14
115	105, 114	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
116	115	nn0cnd 10951	. . . . . . . . . . . 12 $/\$ $/\$
117		hashcl 12576	. . . . . . . . . . . . . 14
118	82, 117	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
119	118	nn0cnd 10951	. . . . . . . . . . . 12 $/\$ $/\$
120		inss1 3643	. . . . . . . . . . . . . . 15
121		ssfi 7810	. . . . . . . . . . . . . . 15 $/\$
122	79, 120, 121	sylancl 675	. . . . . . . . . . . . . 14 $/\$ $/\$
123		hashcl 12576	. . . . . . . . . . . . . 14
124	122, 123	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
125	124	nn0cnd 10951	. . . . . . . . . . . 12 $/\$ $/\$
126	116, 119, 125	addsubassd 10025	. . . . . . . . . . 11 $/\$ $/\$
127	113, 126	eqtrd 2505	. . . . . . . . . 10 $/\$ $/\$
128	127	oveq2d 6324	. . . . . . . . 9 $/\$ $/\$
129		hashcl 12576	. . . . . . . . . . . 12
130	129	adantl 473	. . . . . . . . . . 11 $/\$ $/\$
131	130	nn0cnd 10951	. . . . . . . . . 10 $/\$ $/\$
132	119, 125	subcld 10005	. . . . . . . . . 10 $/\$ $/\$
133	131, 116, 132	subsub4d 10036	. . . . . . . . 9 $/\$ $/\$
134	128, 133	eqtr4d 2508	. . . . . . . 8 $/\$ $/\$
135	134	adantr 472	. . . . . . 7 $/\$ $/\$ $/\$
136		disjdif 3830	. . . . . . . . . . 11 $\$
137	136	a1i 11	. . . . . . . . . 10 $/\$ $/\$ $\$
138		ssun1 3588	. . . . . . . . . . . . . 14
139		sspwb 4649	. . . . . . . . . . . . . 14
140	138, 139	mpbi 213	. . . . . . . . . . . . 13
141		undif 3839	. . . . . . . . . . . . 13 $\$
142	140, 141	mpbi 213	. . . . . . . . . . . 12 $\$
143	142	eqcomi 2480	. . . . . . . . . . 11 $\$
144	143	a1i 11	. . . . . . . . . 10 $/\$ $/\$ $\$
145		simpll 768	. . . . . . . . . . . 12 $/\$ $/\$
146		snfi 7668	. . . . . . . . . . . 12
147		unfi 7856	. . . . . . . . . . . 12 $/\$
148	145, 146, 147	sylancl 675	. . . . . . . . . . 11 $/\$ $/\$
149		pwfi 7887	. . . . . . . . . . 11
150	148, 149	sylib 201	. . . . . . . . . 10 $/\$ $/\$
151	55	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152		elpwi 3951	. . . . . . . . . . . . . 14
153		ssfi 7810	. . . . . . . . . . . . . 14 $/\$
154	148, 152, 153	syl2an 485	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
155		hashcl 12576	. . . . . . . . . . . . 13
156	154, 155	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
157	151, 156	expcld 12454	. . . . . . . . . . 11 $/\$ $/\$ $/\$
158		simplr 770	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
159		inss1 3643	. . . . . . . . . . . . . 14
160		ssfi 7810	. . . . . . . . . . . . . 14 $/\$
161	158, 159, 160	sylancl 675	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
162		hashcl 12576	. . . . . . . . . . . . 13
163	161, 162	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
164	163	nn0cnd 10951	. . . . . . . . . . 11 $/\$ $/\$ $/\$
165	157, 164	mulcld 9681	. . . . . . . . . 10 $/\$ $/\$ $/\$
166	137, 144, 150, 165	fsumsplit 13883	. . . . . . . . 9 $/\$ $/\$ $\$
167		fveq2 5879	. . . . . . . . . . . . . 14
168	167	oveq2d 6324	. . . . . . . . . . . . 13
169		inteq 4229	. . . . . . . . . . . . . . . 16
170	27	intunsn 4265	. . . . . . . . . . . . . . . 16
171	169, 170	syl6eq 2521	. . . . . . . . . . . . . . 15
172	171	ineq2d 3625	. . . . . . . . . . . . . 14
173	172	fveq2d 5883	. . . . . . . . . . . . 13
174	168, 173	oveq12d 6326	. . . . . . . . . . . 12
175		pwfi 7887	. . . . . . . . . . . . 13
176	145, 175	sylib 201	. . . . . . . . . . . 12 $/\$ $/\$
177		eqid 2471	. . . . . . . . . . . . 13
178		elpwi 3951	. . . . . . . . . . . . . . . . 17
179	178	adantl 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
180		unss1 3594	. . . . . . . . . . . . . . . 16
181	179, 180	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
182		vex 3034	. . . . . . . . . . . . . . . . 17
183		snex 4641	. . . . . . . . . . . . . . . . 17
184	182, 183	unex 6608	. . . . . . . . . . . . . . . 16
185	184	elpw 3948	. . . . . . . . . . . . . . 15
186	181, 185	sylibr 217	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
187		simpllr 777	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
188		elpwi 3951	. . . . . . . . . . . . . . . 16
189		ssun2 3589	. . . . . . . . . . . . . . . . . . 19
190	27	snss 4087	. . . . . . . . . . . . . . . . . . 19
191	189, 190	mpbir 214	. . . . . . . . . . . . . . . . . 18
192	191	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
193		ssel 3412	. . . . . . . . . . . . . . . . 17
194	192, 193	syl5com 30	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
195	188, 194	syl5 32	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
196	187, 195	mtod 182	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
197	186, 196	eldifd 3401	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
198		eldifi 3544	. . . . . . . . . . . . . . . . . 18 $\$
199	198	adantl 473	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
200	199	elpwid 3952	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
201		uncom 3569	. . . . . . . . . . . . . . . 16
202	200, 201	syl6sseq 3464	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
203		ssundif 3842	. . . . . . . . . . . . . . 15 $\$
204	202, 203	sylib 201	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
205		vex 3034	. . . . . . . . . . . . . . 15
206	205	elpw2 4565	. . . . . . . . . . . . . 14 $\$ $\$
207	204, 206	sylibr 217	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
208		elpwunsn 4003	. . . . . . . . . . . . . . . . . . 19 $\$
209	208	ad2antll 743	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$
210	209	snssd 4108	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\$
211		ssequn2 3598	. . . . . . . . . . . . . . . . 17
212	210, 211	sylib 201	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $\$
213	212	eqcomd 2477	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$
214		uneq1 3572	. . . . . . . . . . . . . . . . 17 $\$ $\$
215		undif1 3833	. . . . . . . . . . . . . . . . 17 $\$
216	214, 215	syl6eq 2521	. . . . . . . . . . . . . . . 16 $\$
217	216	eqeq2d 2481	. . . . . . . . . . . . . . 15 $\$
218	213, 217	syl5ibrcom 230	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $\$ $\$
219	178	ad2antrl 742	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$
220		simpllr 777	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$
221	219, 220	ssneldd 3421	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\$
222		difsnb 4105	. . . . . . . . . . . . . . . . 17 $\$
223	221, 222	sylib 201	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $\$ $\$
224	223	eqcomd 2477	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$ $\$
225		difeq1 3533	. . . . . . . . . . . . . . . . 17 $\$ $\$
226		difun2 3838	. . . . . . . . . . . . . . . . 17 $\$ $\$
227	225, 226	syl6eq 2521	. . . . . . . . . . . . . . . 16 $\$ $\$
228	227	eqeq2d 2481	. . . . . . . . . . . . . . 15 $\$ $\$
229	224, 228	syl5ibrcom 230	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $\$ $\$
230	218, 229	impbid 195	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\$ $\$
231	177, 197, 207, 230	f1o2d 6540	. . . . . . . . . . . 12 $/\$ $/\$ $\$
232		uneq1 3572	. . . . . . . . . . . . . 14
233		vex 3034	. . . . . . . . . . . . . . 15
234	233, 183	unex 6608	. . . . . . . . . . . . . 14
235	232, 177, 234	fvmpt 5963	. . . . . . . . . . . . 13
236	235	adantl 473	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
237	198, 165	sylan2 482	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
238	174, 176, 231, 236, 237	fsumf1o 13866	. . . . . . . . . . 11 $/\$ $/\$ $\$
239		uneq1 3572	. . . . . . . . . . . . . . . 16
240	239	fveq2d 5883	. . . . . . . . . . . . . . 15
241	240	oveq2d 6324	. . . . . . . . . . . . . 14
242		inteq 4229	. . . . . . . . . . . . . . . . 17
243	242	ineq1d 3624	. . . . . . . . . . . . . . . 16
244	243	ineq2d 3625	. . . . . . . . . . . . . . 15
245	244	fveq2d 5883	. . . . . . . . . . . . . 14
246	241, 245	oveq12d 6326	. . . . . . . . . . . . 13
247	246	cbvsumv 13839	. . . . . . . . . . . 12
248		elpwi 3951	. . . . . . . . . . . . . . . . . . . 20
249		ssfi 7810	. . . . . . . . . . . . . . . . . . . 20 $/\$
250	145, 248, 249	syl2an 485	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
251	248	adantl 473	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
252		simpllr 777	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
253	251, 252	ssneldd 3421	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
254		hashunsng 12609	. . . . . . . . . . . . . . . . . . . 20 $/\$
255	27, 254	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 $/\$
256	250, 253, 255	syl2anc 673	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
257	256	oveq2d 6324	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
258	55	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
259	250, 155	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
260	258, 259	expp1d 12455	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
261	257, 260	eqtrd 2505	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
262	140	sseli 3414	. . . . . . . . . . . . . . . . . 18
263	262, 157	sylan2 482	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
264	258, 263	mulcomd 9682	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
265	263	mulm1d 10091	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
266	261, 264, 265	3eqtr2d 2511	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
267	266	oveq1d 6323	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
268		inss1 3643	. . . . . . . . . . . . . . . . . . 19
269		ssfi 7810	. . . . . . . . . . . . . . . . . . 19 $/\$
270	158, 268, 269	sylancl 675	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
271		hashcl 12576	. . . . . . . . . . . . . . . . . 18
272	270, 271	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
273	272	nn0cnd 10951	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
274	262, 273	sylan2 482	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
275	263, 274	mulneg1d 10092	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
276	267, 275	eqtrd 2505	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
277	276	sumeq2dv 13846	. . . . . . . . . . . 12 $/\$ $/\$
278	247, 277	syl5eq 2517	. . . . . . . . . . 11 $/\$ $/\$
279	157, 273	mulcld 9681	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
280	262, 279	sylan2 482	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
281	176, 280	fsumneg 13925	. . . . . . . . . . 11 $/\$ $/\$
282	238, 278, 281	3eqtrd 2509	. . . . . . . . . 10 $/\$ $/\$ $\$
283	282	oveq2d 6324	. . . . . . . . 9 $/\$ $/\$ $\$
284	140	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
285	284	sselda 3418	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
286	285, 165	syldan 478	. . . . . . . . . . 11 $/\$ $/\$ $/\$
287	176, 286	fsumcl 13876	. . . . . . . . . 10 $/\$ $/\$
288	285, 279	syldan 478	. . . . . . . . . . 11 $/\$ $/\$ $/\$
289	176, 288	fsumcl 13876	. . . . . . . . . 10 $/\$ $/\$
290	287, 289	negsubd 10011	. . . . . . . . 9 $/\$ $/\$
291	166, 283, 290	3eqtrd 2509	. . . . . . . 8 $/\$ $/\$
292	291	adantr 472	. . . . . . 7 $/\$ $/\$ $/\$
293	102, 135, 292	3eqtr4d 2515	. . . . . 6 $/\$ $/\$ $/\$
294	293	ex 441	. . . . 5 $/\$ $/\$
295	294	ralrimdva 2812	. . . 4 $/\$
296		ineq1 3618	. . . . . . . 8
297	296	fveq2d 5883	. . . . . . 7
298	67, 297	oveq12d 6326	. . . . . 6
299		ineq1 3618	. . . . . . . . 9
300	299	fveq2d 5883	. . . . . . . 8
301	300	oveq2d 6324	. . . . . . 7
302	301	sumeq2sdv 13847	. . . . . 6
303	298, 302	eqeq12d 2486	. . . . 5
304	303	cbvralv 3005	. . . 4
305	295, 304	syl6ibr 235	. . 3 $/\$
306	16, 24, 38, 46, 66, 305	findcard2s 7830	. 2
307		fveq2 5879	. . . . 5
308		ineq1 3618	. . . . . 6
309	308	fveq2d 5883	. . . . 5
310	307, 309	oveq12d 6326	. . . 4
311		simpl 464	. . . . . . . 8 $/\$
312	311	ineq1d 3624	. . . . . . 7 $/\$
313	312	fveq2d 5883	. . . . . 6 $/\$
314	313	oveq2d 6324	. . . . 5 $/\$
315	314	sumeq2dv 13846	. . . 4
316	310, 315	eqeq12d 2486	. . 3
317	316	rspccva 3135	. 2 $/\$
318	306, 317	sylan 479	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 376

wceq 1452

wcel 1904

wral 2756

cvv 3031 $\$ cdif 3387

cun 3388

cin 3389

wss 3390

c0 3722

cpw 3942

csn 3959

cuni 4190

cint 4226

cmpt 4454

cfv 5589 (class class class)co 6308

cfn 7587

cc 9555

cc0 9557

c1 9558

caddc 9560

cmul 9562

cmin 9880

cneg 9881

cn0 10893

cexp 12310

chash 12553

csu 13829

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-er 7381 df-map 7492 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-sup 7974 df-oi 8043 df-card 8391 df-cda 8616 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-n0 10894 df-z 10962 df-uz 11183 df-rp 11326 df-fz 11811 df-fzo 11943 df-seq 12252 df-exp 12311 df-hash 12554 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-clim 13629 df-sum 13830

This theorem is referenced by: incexc 13972

W3C validator