incexclem - Metamath Proof Explorer

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

Theorem incexclem 13887

Description: Lemma for incexc 13888. (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 4225	. . . . . . . . . . 11
2		uni0 4244	. . . . . . . . . . 11
3	1, 2	syl6eq 2480	. . . . . . . . . 10
4	3	ineq2d 3665	. . . . . . . . 9
5		in0 3789	. . . . . . . . 9
6	4, 5	syl6eq 2480	. . . . . . . 8
7	6	fveq2d 5883	. . . . . . 7
8		hash0 12549	. . . . . . 7
9	7, 8	syl6eq 2480	. . . . . 6
10	9	oveq2d 6319	. . . . 5
11		pweq 3983	. . . . . . 7
12		pw0 4145	. . . . . . 7
13	11, 12	syl6eq 2480	. . . . . 6
14	13	sumeq1d 13760	. . . . 5
15	10, 14	eqeq12d 2445	. . . 4
16	15	ralbidv 2865	. . 3
17		unieq 4225	. . . . . . . 8
18	17	ineq2d 3665	. . . . . . 7
19	18	fveq2d 5883	. . . . . 6
20	19	oveq2d 6319	. . . . 5
21		pweq 3983	. . . . . 6
22	21	sumeq1d 13760	. . . . 5
23	20, 22	eqeq12d 2445	. . . 4
24	23	ralbidv 2865	. . 3
25		unieq 4225	. . . . . . . . 9
26		uniun 4236	. . . . . . . . . 10
27		vex 3085	. . . . . . . . . . . 12
28	27	unisn 4232	. . . . . . . . . . 11
29	28	uneq2i 3618	. . . . . . . . . 10
30	26, 29	eqtri 2452	. . . . . . . . 9
31	25, 30	syl6eq 2480	. . . . . . . 8
32	31	ineq2d 3665	. . . . . . 7
33	32	fveq2d 5883	. . . . . 6
34	33	oveq2d 6319	. . . . 5
35		pweq 3983	. . . . . 6
36	35	sumeq1d 13760	. . . . 5
37	34, 36	eqeq12d 2445	. . . 4
38	37	ralbidv 2865	. . 3
39		unieq 4225	. . . . . . . 8
40	39	ineq2d 3665	. . . . . . 7
41	40	fveq2d 5883	. . . . . 6
42	41	oveq2d 6319	. . . . 5
43		pweq 3983	. . . . . 6
44	43	sumeq1d 13760	. . . . 5
45	42, 44	eqeq12d 2445	. . . 4
46	45	ralbidv 2865	. . 3
47		hashcl 12539	. . . . . . 7
48	47	nn0cnd 10929	. . . . . 6
49	48	mulid2d 9663	. . . . 5
50		0ex 4554	. . . . . 6
51	49, 48	eqeltrd 2511	. . . . . 6
52		fveq2 5879	. . . . . . . . . . 11
53	52, 8	syl6eq 2480	. . . . . . . . . 10
54	53	oveq2d 6319	. . . . . . . . 9
55		neg1cn 10715	. . . . . . . . . 10
56		exp0 12277	. . . . . . . . . 10
57	55, 56	ax-mp 5	. . . . . . . . 9
58	54, 57	syl6eq 2480	. . . . . . . 8
59		rint0 4294	. . . . . . . . 9
60	59	fveq2d 5883	. . . . . . . 8
61	58, 60	oveq12d 6321	. . . . . . 7
62	61	sumsn 13800	. . . . . 6 $/\$
63	50, 51, 62	sylancr 668	. . . . 5
64	48	subid1d 9977	. . . . 5
65	49, 63, 64	3eqtr4rd 2475	. . . 4
66	65	rgen 2786	. . 3
67		fveq2 5879	. . . . . . . . . . . 12
68		ineq1 3658	. . . . . . . . . . . . 13
69	68	fveq2d 5883	. . . . . . . . . . . 12
70	67, 69	oveq12d 6321	. . . . . . . . . . 11
71		simpl 459	. . . . . . . . . . . . . . 15 $/\$
72	71	ineq1d 3664	. . . . . . . . . . . . . 14 $/\$
73	72	fveq2d 5883	. . . . . . . . . . . . 13 $/\$
74	73	oveq2d 6319	. . . . . . . . . . . 12 $/\$
75	74	sumeq2dv 13762	. . . . . . . . . . 11
76	70, 75	eqeq12d 2445	. . . . . . . . . 10
77	76	rspcva 3181	. . . . . . . . 9 $/\$
78	77	adantll 719	. . . . . . . 8 $/\$ $/\$ $/\$
79		simpr 463	. . . . . . . . . 10 $/\$ $/\$
80		inss1 3683	. . . . . . . . . 10
81		ssfi 7796	. . . . . . . . . 10 $/\$
82	79, 80, 81	sylancl 667	. . . . . . . . 9 $/\$ $/\$
83		fveq2 5879	. . . . . . . . . . . 12
84		ineq1 3658	. . . . . . . . . . . . . 14
85		in32 3675	. . . . . . . . . . . . . . 15
86		inass 3673	. . . . . . . . . . . . . . 15
87	85, 86	eqtri 2452	. . . . . . . . . . . . . 14
88	84, 87	syl6eq 2480	. . . . . . . . . . . . 13
89	88	fveq2d 5883	. . . . . . . . . . . 12
90	83, 89	oveq12d 6321	. . . . . . . . . . 11
91		ineq1 3658	. . . . . . . . . . . . . . 15
92		in32 3675	. . . . . . . . . . . . . . . 16
93		inass 3673	. . . . . . . . . . . . . . . 16
94	92, 93	eqtri 2452	. . . . . . . . . . . . . . 15
95	91, 94	syl6eq 2480	. . . . . . . . . . . . . 14
96	95	fveq2d 5883	. . . . . . . . . . . . 13
97	96	oveq2d 6319	. . . . . . . . . . . 12
98	97	sumeq2sdv 13763	. . . . . . . . . . 11
99	90, 98	eqeq12d 2445	. . . . . . . . . 10
100	99	rspcva 3181	. . . . . . . . 9 $/\$
101	82, 100	sylan 474	. . . . . . . 8 $/\$ $/\$ $/\$
102	78, 101	oveq12d 6321	. . . . . . 7 $/\$ $/\$ $/\$
103		inss1 3683	. . . . . . . . . . . . . 14
104		ssfi 7796	. . . . . . . . . . . . . 14 $/\$
105	79, 103, 104	sylancl 667	. . . . . . . . . . . . 13 $/\$ $/\$
106		hashun3 12564	. . . . . . . . . . . . 13 $/\$
107	105, 82, 106	syl2anc 666	. . . . . . . . . . . 12 $/\$ $/\$
108		indi 3720	. . . . . . . . . . . . 13
109	108	fveq2i 5882	. . . . . . . . . . . 12
110		inindi 3680	. . . . . . . . . . . . . 14
111	110	fveq2i 5882	. . . . . . . . . . . . 13
112	111	oveq2i 6314	. . . . . . . . . . . 12
113	107, 109, 112	3eqtr4g 2489	. . . . . . . . . . 11 $/\$ $/\$
114		hashcl 12539	. . . . . . . . . . . . . 14
115	105, 114	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
116	115	nn0cnd 10929	. . . . . . . . . . . 12 $/\$ $/\$
117		hashcl 12539	. . . . . . . . . . . . . 14
118	82, 117	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
119	118	nn0cnd 10929	. . . . . . . . . . . 12 $/\$ $/\$
120		inss1 3683	. . . . . . . . . . . . . . 15
121		ssfi 7796	. . . . . . . . . . . . . . 15 $/\$
122	79, 120, 121	sylancl 667	. . . . . . . . . . . . . 14 $/\$ $/\$
123		hashcl 12539	. . . . . . . . . . . . . 14
124	122, 123	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
125	124	nn0cnd 10929	. . . . . . . . . . . 12 $/\$ $/\$
126	116, 119, 125	addsubassd 10008	. . . . . . . . . . 11 $/\$ $/\$
127	113, 126	eqtrd 2464	. . . . . . . . . 10 $/\$ $/\$
128	127	oveq2d 6319	. . . . . . . . 9 $/\$ $/\$
129		hashcl 12539	. . . . . . . . . . . 12
130	129	adantl 468	. . . . . . . . . . 11 $/\$ $/\$
131	130	nn0cnd 10929	. . . . . . . . . 10 $/\$ $/\$
132	119, 125	subcld 9988	. . . . . . . . . 10 $/\$ $/\$
133	131, 116, 132	subsub4d 10019	. . . . . . . . 9 $/\$ $/\$
134	128, 133	eqtr4d 2467	. . . . . . . 8 $/\$ $/\$
135	134	adantr 467	. . . . . . 7 $/\$ $/\$ $/\$
136		disjdif 3868	. . . . . . . . . . 11 $\$
137	136	a1i 11	. . . . . . . . . 10 $/\$ $/\$ $\$
138		ssun1 3630	. . . . . . . . . . . . . 14
139		sspwb 4668	. . . . . . . . . . . . . 14
140	138, 139	mpbi 212	. . . . . . . . . . . . 13
141		undif 3877	. . . . . . . . . . . . 13 $\$
142	140, 141	mpbi 212	. . . . . . . . . . . 12 $\$
143	142	eqcomi 2436	. . . . . . . . . . 11 $\$
144	143	a1i 11	. . . . . . . . . 10 $/\$ $/\$ $\$
145		simpll 759	. . . . . . . . . . . 12 $/\$ $/\$
146		snfi 7655	. . . . . . . . . . . 12
147		unfi 7842	. . . . . . . . . . . 12 $/\$
148	145, 146, 147	sylancl 667	. . . . . . . . . . 11 $/\$ $/\$
149		pwfi 7873	. . . . . . . . . . 11
150	148, 149	sylib 200	. . . . . . . . . 10 $/\$ $/\$
151	55	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152		elpwi 3989	. . . . . . . . . . . . . 14
153		ssfi 7796	. . . . . . . . . . . . . 14 $/\$
154	148, 152, 153	syl2an 480	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
155		hashcl 12539	. . . . . . . . . . . . 13
156	154, 155	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
157	151, 156	expcld 12417	. . . . . . . . . . 11 $/\$ $/\$ $/\$
158		simplr 761	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
159		inss1 3683	. . . . . . . . . . . . . 14
160		ssfi 7796	. . . . . . . . . . . . . 14 $/\$
161	158, 159, 160	sylancl 667	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
162		hashcl 12539	. . . . . . . . . . . . 13
163	161, 162	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
164	163	nn0cnd 10929	. . . . . . . . . . 11 $/\$ $/\$ $/\$
165	157, 164	mulcld 9665	. . . . . . . . . 10 $/\$ $/\$ $/\$
166	137, 144, 150, 165	fsumsplit 13799	. . . . . . . . 9 $/\$ $/\$ $\$
167		fveq2 5879	. . . . . . . . . . . . . 14
168	167	oveq2d 6319	. . . . . . . . . . . . 13
169		inteq 4256	. . . . . . . . . . . . . . . 16
170	27	intunsn 4293	. . . . . . . . . . . . . . . 16
171	169, 170	syl6eq 2480	. . . . . . . . . . . . . . 15
172	171	ineq2d 3665	. . . . . . . . . . . . . 14
173	172	fveq2d 5883	. . . . . . . . . . . . 13
174	168, 173	oveq12d 6321	. . . . . . . . . . . 12
175		pwfi 7873	. . . . . . . . . . . . 13
176	145, 175	sylib 200	. . . . . . . . . . . 12 $/\$ $/\$
177		eqid 2423	. . . . . . . . . . . . 13
178		elpwi 3989	. . . . . . . . . . . . . . . . 17
179	178	adantl 468	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
180		unss1 3636	. . . . . . . . . . . . . . . 16
181	179, 180	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
182		vex 3085	. . . . . . . . . . . . . . . . 17
183		snex 4660	. . . . . . . . . . . . . . . . 17
184	182, 183	unex 6601	. . . . . . . . . . . . . . . 16
185	184	elpw 3986	. . . . . . . . . . . . . . 15
186	181, 185	sylibr 216	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
187		simpllr 768	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
188		elpwi 3989	. . . . . . . . . . . . . . . 16
189		ssun2 3631	. . . . . . . . . . . . . . . . . . 19
190	27	snss 4122	. . . . . . . . . . . . . . . . . . 19
191	189, 190	mpbir 213	. . . . . . . . . . . . . . . . . 18
192	191	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
193		ssel 3459	. . . . . . . . . . . . . . . . 17
194	192, 193	syl5com 32	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
195	188, 194	syl5 34	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
196	187, 195	mtod 181	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
197	186, 196	eldifd 3448	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
198		eldifi 3588	. . . . . . . . . . . . . . . . . 18 $\$
199	198	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
200	199	elpwid 3990	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
201		uncom 3611	. . . . . . . . . . . . . . . 16
202	200, 201	syl6sseq 3511	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
203		ssundif 3880	. . . . . . . . . . . . . . 15 $\$
204	202, 203	sylib 200	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
205		vex 3085	. . . . . . . . . . . . . . 15
206	205	elpw2 4586	. . . . . . . . . . . . . 14 $\$ $\$
207	204, 206	sylibr 216	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
208		elpwunsn 4038	. . . . . . . . . . . . . . . . . . 19 $\$
209	208	ad2antll 734	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$
210	209	snssd 4143	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\$
211		ssequn2 3640	. . . . . . . . . . . . . . . . 17
212	210, 211	sylib 200	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $\$
213	212	eqcomd 2431	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$
214		uneq1 3614	. . . . . . . . . . . . . . . . 17 $\$ $\$
215		undif1 3871	. . . . . . . . . . . . . . . . 17 $\$
216	214, 215	syl6eq 2480	. . . . . . . . . . . . . . . 16 $\$
217	216	eqeq2d 2437	. . . . . . . . . . . . . . 15 $\$
218	213, 217	syl5ibrcom 226	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $\$ $\$
219	178	ad2antrl 733	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$
220		simpllr 768	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$
221	219, 220	ssneldd 3468	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\$
222		difsnb 4140	. . . . . . . . . . . . . . . . 17 $\$
223	221, 222	sylib 200	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $\$ $\$
224	223	eqcomd 2431	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$ $\$
225		difeq1 3577	. . . . . . . . . . . . . . . . 17 $\$ $\$
226		difun2 3876	. . . . . . . . . . . . . . . . 17 $\$ $\$
227	225, 226	syl6eq 2480	. . . . . . . . . . . . . . . 16 $\$ $\$
228	227	eqeq2d 2437	. . . . . . . . . . . . . . 15 $\$ $\$
229	224, 228	syl5ibrcom 226	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $\$ $\$
230	218, 229	impbid 194	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\$ $\$
231	177, 197, 207, 230	f1o2d 6533	. . . . . . . . . . . 12 $/\$ $/\$ $\$
232		uneq1 3614	. . . . . . . . . . . . . 14
233		vex 3085	. . . . . . . . . . . . . . 15
234	233, 183	unex 6601	. . . . . . . . . . . . . 14
235	232, 177, 234	fvmpt 5962	. . . . . . . . . . . . 13
236	235	adantl 468	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
237	198, 165	sylan2 477	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
238	174, 176, 231, 236, 237	fsumf1o 13782	. . . . . . . . . . 11 $/\$ $/\$ $\$
239		uneq1 3614	. . . . . . . . . . . . . . . 16
240	239	fveq2d 5883	. . . . . . . . . . . . . . 15
241	240	oveq2d 6319	. . . . . . . . . . . . . 14
242		inteq 4256	. . . . . . . . . . . . . . . . 17
243	242	ineq1d 3664	. . . . . . . . . . . . . . . 16
244	243	ineq2d 3665	. . . . . . . . . . . . . . 15
245	244	fveq2d 5883	. . . . . . . . . . . . . 14
246	241, 245	oveq12d 6321	. . . . . . . . . . . . 13
247	246	cbvsumv 13755	. . . . . . . . . . . 12
248		elpwi 3989	. . . . . . . . . . . . . . . . . . . 20
249		ssfi 7796	. . . . . . . . . . . . . . . . . . . 20 $/\$
250	145, 248, 249	syl2an 480	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
251	248	adantl 468	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
252		simpllr 768	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
253	251, 252	ssneldd 3468	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
254		hashunsng 12572	. . . . . . . . . . . . . . . . . . . 20 $/\$
255	27, 254	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 $/\$
256	250, 253, 255	syl2anc 666	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
257	256	oveq2d 6319	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
258	55	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
259	250, 155	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
260	258, 259	expp1d 12418	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
261	257, 260	eqtrd 2464	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
262	140	sseli 3461	. . . . . . . . . . . . . . . . . 18
263	262, 157	sylan2 477	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
264	258, 263	mulcomd 9666	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
265	263	mulm1d 10072	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
266	261, 264, 265	3eqtr2d 2470	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
267	266	oveq1d 6318	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
268		inss1 3683	. . . . . . . . . . . . . . . . . . 19
269		ssfi 7796	. . . . . . . . . . . . . . . . . . 19 $/\$
270	158, 268, 269	sylancl 667	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
271		hashcl 12539	. . . . . . . . . . . . . . . . . 18
272	270, 271	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
273	272	nn0cnd 10929	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
274	262, 273	sylan2 477	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
275	263, 274	mulneg1d 10073	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
276	267, 275	eqtrd 2464	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
277	276	sumeq2dv 13762	. . . . . . . . . . . 12 $/\$ $/\$
278	247, 277	syl5eq 2476	. . . . . . . . . . 11 $/\$ $/\$
279	157, 273	mulcld 9665	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
280	262, 279	sylan2 477	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
281	176, 280	fsumneg 13841	. . . . . . . . . . 11 $/\$ $/\$
282	238, 278, 281	3eqtrd 2468	. . . . . . . . . 10 $/\$ $/\$ $\$
283	282	oveq2d 6319	. . . . . . . . 9 $/\$ $/\$ $\$
284	140	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
285	284	sselda 3465	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
286	285, 165	syldan 473	. . . . . . . . . . 11 $/\$ $/\$ $/\$
287	176, 286	fsumcl 13792	. . . . . . . . . 10 $/\$ $/\$
288	285, 279	syldan 473	. . . . . . . . . . 11 $/\$ $/\$ $/\$
289	176, 288	fsumcl 13792	. . . . . . . . . 10 $/\$ $/\$
290	287, 289	negsubd 9994	. . . . . . . . 9 $/\$ $/\$
291	166, 283, 290	3eqtrd 2468	. . . . . . . 8 $/\$ $/\$
292	291	adantr 467	. . . . . . 7 $/\$ $/\$ $/\$
293	102, 135, 292	3eqtr4d 2474	. . . . . 6 $/\$ $/\$ $/\$
294	293	ex 436	. . . . 5 $/\$ $/\$
295	294	ralrimdva 2844	. . . 4 $/\$
296		ineq1 3658	. . . . . . . 8
297	296	fveq2d 5883	. . . . . . 7
298	67, 297	oveq12d 6321	. . . . . 6
299		ineq1 3658	. . . . . . . . 9
300	299	fveq2d 5883	. . . . . . . 8
301	300	oveq2d 6319	. . . . . . 7
302	301	sumeq2sdv 13763	. . . . . 6
303	298, 302	eqeq12d 2445	. . . . 5
304	303	cbvralv 3056	. . . 4
305	295, 304	syl6ibr 231	. . 3 $/\$
306	16, 24, 38, 46, 66, 305	findcard2s 7816	. 2
307		fveq2 5879	. . . . 5
308		ineq1 3658	. . . . . 6
309	308	fveq2d 5883	. . . . 5
310	307, 309	oveq12d 6321	. . . 4
311		simpl 459	. . . . . . . 8 $/\$
312	311	ineq1d 3664	. . . . . . 7 $/\$
313	312	fveq2d 5883	. . . . . 6 $/\$
314	313	oveq2d 6319	. . . . 5 $/\$
315	314	sumeq2dv 13762	. . . 4
316	310, 315	eqeq12d 2445	. . 3
317	316	rspccva 3182	. 2 $/\$
318	306, 317	sylan 474	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 371

wceq 1438

wcel 1869

wral 2776

cvv 3082 $\$ cdif 3434

cun 3435

cin 3436

wss 3437

c0 3762

cpw 3980

csn 3997

cuni 4217

cint 4253

cmpt 4480

cfv 5599 (class class class)co 6303

cfn 7575

cc 9539

cc0 9541

c1 9542

caddc 9544

cmul 9546

cmin 9862

cneg 9863

cn0 10871

cexp 12273

chash 12516

csu 13745

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1666 ax-4 1679 ax-5 1749 ax-6 1795 ax-7 1840 ax-8 1871 ax-9 1873 ax-10 1888 ax-11 1893 ax-12 1906 ax-13 2054 ax-ext 2401 ax-rep 4534 ax-sep 4544 ax-nul 4553 ax-pow 4600 ax-pr 4658 ax-un 6595 ax-inf2 8150 ax-cnex 9597 ax-resscn 9598 ax-1cn 9599 ax-icn 9600 ax-addcl 9601 ax-addrcl 9602 ax-mulcl 9603 ax-mulrcl 9604 ax-mulcom 9605 ax-addass 9606 ax-mulass 9607 ax-distr 9608 ax-i2m1 9609 ax-1ne0 9610 ax-1rid 9611 ax-rnegex 9612 ax-rrecex 9613 ax-cnre 9614 ax-pre-lttri 9615 ax-pre-lttrn 9616 ax-pre-ltadd 9617 ax-pre-mulgt0 9618 ax-pre-sup 9619

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 984 df-3an 985 df-tru 1441 df-fal 1444 df-ex 1661 df-nf 1665 df-sb 1788 df-eu 2270 df-mo 2271 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2573 df-ne 2621 df-nel 2622 df-ral 2781 df-rex 2782 df-reu 2783 df-rmo 2784 df-rab 2785 df-v 3084 df-sbc 3301 df-csb 3397 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-pss 3453 df-nul 3763 df-if 3911 df-pw 3982 df-sn 3998 df-pr 4000 df-tp 4002 df-op 4004 df-uni 4218 df-int 4254 df-iun 4299 df-br 4422 df-opab 4481 df-mpt 4482 df-tr 4517 df-eprel 4762 df-id 4766 df-po 4772 df-so 4773 df-fr 4810 df-se 4811 df-we 4812 df-xp 4857 df-rel 4858 df-cnv 4859 df-co 4860 df-dm 4861 df-rn 4862 df-res 4863 df-ima 4864 df-pred 5397 df-ord 5443 df-on 5444 df-lim 5445 df-suc 5446 df-iota 5563 df-fun 5601 df-fn 5602 df-f 5603 df-f1 5604 df-fo 5605 df-f1o 5606 df-fv 5607 df-isom 5608 df-riota 6265 df-ov 6306 df-oprab 6307 df-mpt2 6308 df-om 6705 df-1st 6805 df-2nd 6806 df-wrecs 7034 df-recs 7096 df-rdg 7134 df-1o 7188 df-2o 7189 df-oadd 7192 df-er 7369 df-map 7480 df-en 7576 df-dom 7577 df-sdom 7578 df-fin 7579 df-sup 7960 df-oi 8029 df-card 8376 df-cda 8600 df-pnf 9679 df-mnf 9680 df-xr 9681 df-ltxr 9682 df-le 9683 df-sub 9864 df-neg 9865 df-div 10272 df-nn 10612 df-2 10670 df-3 10671 df-n0 10872 df-z 10940 df-uz 11162 df-rp 11305 df-fz 11787 df-fzo 11918 df-seq 12215 df-exp 12274 df-hash 12517 df-cj 13156 df-re 13157 df-im 13158 df-sqrt 13292 df-abs 13293 df-clim 13545 df-sum 13746

This theorem is referenced by: incexc 13888

W3C validator