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 13894

Description: Lemma for incexc 13895. (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 4206	. . . . . . . . . . 11
2		uni0 4225	. . . . . . . . . . 11
3	1, 2	syl6eq 2501	. . . . . . . . . 10
4	3	ineq2d 3634	. . . . . . . . 9
5		in0 3760	. . . . . . . . 9
6	4, 5	syl6eq 2501	. . . . . . . 8
7	6	fveq2d 5869	. . . . . . 7
8		hash0 12548	. . . . . . 7
9	7, 8	syl6eq 2501	. . . . . 6
10	9	oveq2d 6306	. . . . 5
11		pweq 3954	. . . . . . 7
12		pw0 4119	. . . . . . 7
13	11, 12	syl6eq 2501	. . . . . 6
14	13	sumeq1d 13767	. . . . 5
15	10, 14	eqeq12d 2466	. . . 4
16	15	ralbidv 2827	. . 3
17		unieq 4206	. . . . . . . 8
18	17	ineq2d 3634	. . . . . . 7
19	18	fveq2d 5869	. . . . . 6
20	19	oveq2d 6306	. . . . 5
21		pweq 3954	. . . . . 6
22	21	sumeq1d 13767	. . . . 5
23	20, 22	eqeq12d 2466	. . . 4
24	23	ralbidv 2827	. . 3
25		unieq 4206	. . . . . . . . 9
26		uniun 4217	. . . . . . . . . 10
27		vex 3048	. . . . . . . . . . . 12
28	27	unisn 4213	. . . . . . . . . . 11
29	28	uneq2i 3585	. . . . . . . . . 10
30	26, 29	eqtri 2473	. . . . . . . . 9
31	25, 30	syl6eq 2501	. . . . . . . 8
32	31	ineq2d 3634	. . . . . . 7
33	32	fveq2d 5869	. . . . . 6
34	33	oveq2d 6306	. . . . 5
35		pweq 3954	. . . . . 6
36	35	sumeq1d 13767	. . . . 5
37	34, 36	eqeq12d 2466	. . . 4
38	37	ralbidv 2827	. . 3
39		unieq 4206	. . . . . . . 8
40	39	ineq2d 3634	. . . . . . 7
41	40	fveq2d 5869	. . . . . 6
42	41	oveq2d 6306	. . . . 5
43		pweq 3954	. . . . . 6
44	43	sumeq1d 13767	. . . . 5
45	42, 44	eqeq12d 2466	. . . 4
46	45	ralbidv 2827	. . 3
47		hashcl 12538	. . . . . . 7
48	47	nn0cnd 10927	. . . . . 6
49	48	mulid2d 9661	. . . . 5
50		0ex 4535	. . . . . 6
51	49, 48	eqeltrd 2529	. . . . . 6
52		fveq2 5865	. . . . . . . . . . 11
53	52, 8	syl6eq 2501	. . . . . . . . . 10
54	53	oveq2d 6306	. . . . . . . . 9
55		neg1cn 10713	. . . . . . . . . 10
56		exp0 12276	. . . . . . . . . 10
57	55, 56	ax-mp 5	. . . . . . . . 9
58	54, 57	syl6eq 2501	. . . . . . . 8
59		rint0 4275	. . . . . . . . 9
60	59	fveq2d 5869	. . . . . . . 8
61	58, 60	oveq12d 6308	. . . . . . 7
62	61	sumsn 13807	. . . . . 6 $/\$
63	50, 51, 62	sylancr 669	. . . . 5
64	48	subid1d 9975	. . . . 5
65	49, 63, 64	3eqtr4rd 2496	. . . 4
66	65	rgen 2747	. . 3
67		fveq2 5865	. . . . . . . . . . . 12
68		ineq1 3627	. . . . . . . . . . . . 13
69	68	fveq2d 5869	. . . . . . . . . . . 12
70	67, 69	oveq12d 6308	. . . . . . . . . . 11
71		simpl 459	. . . . . . . . . . . . . . 15 $/\$
72	71	ineq1d 3633	. . . . . . . . . . . . . 14 $/\$
73	72	fveq2d 5869	. . . . . . . . . . . . 13 $/\$
74	73	oveq2d 6306	. . . . . . . . . . . 12 $/\$
75	74	sumeq2dv 13769	. . . . . . . . . . 11
76	70, 75	eqeq12d 2466	. . . . . . . . . 10
77	76	rspcva 3148	. . . . . . . . 9 $/\$
78	77	adantll 720	. . . . . . . 8 $/\$ $/\$ $/\$
79		simpr 463	. . . . . . . . . 10 $/\$ $/\$
80		inss1 3652	. . . . . . . . . 10
81		ssfi 7792	. . . . . . . . . 10 $/\$
82	79, 80, 81	sylancl 668	. . . . . . . . 9 $/\$ $/\$
83		fveq2 5865	. . . . . . . . . . . 12
84		ineq1 3627	. . . . . . . . . . . . . 14
85		in32 3644	. . . . . . . . . . . . . . 15
86		inass 3642	. . . . . . . . . . . . . . 15
87	85, 86	eqtri 2473	. . . . . . . . . . . . . 14
88	84, 87	syl6eq 2501	. . . . . . . . . . . . 13
89	88	fveq2d 5869	. . . . . . . . . . . 12
90	83, 89	oveq12d 6308	. . . . . . . . . . 11
91		ineq1 3627	. . . . . . . . . . . . . . 15
92		in32 3644	. . . . . . . . . . . . . . . 16
93		inass 3642	. . . . . . . . . . . . . . . 16
94	92, 93	eqtri 2473	. . . . . . . . . . . . . . 15
95	91, 94	syl6eq 2501	. . . . . . . . . . . . . 14
96	95	fveq2d 5869	. . . . . . . . . . . . 13
97	96	oveq2d 6306	. . . . . . . . . . . 12
98	97	sumeq2sdv 13770	. . . . . . . . . . 11
99	90, 98	eqeq12d 2466	. . . . . . . . . 10
100	99	rspcva 3148	. . . . . . . . 9 $/\$
101	82, 100	sylan 474	. . . . . . . 8 $/\$ $/\$ $/\$
102	78, 101	oveq12d 6308	. . . . . . 7 $/\$ $/\$ $/\$
103		inss1 3652	. . . . . . . . . . . . . 14
104		ssfi 7792	. . . . . . . . . . . . . 14 $/\$
105	79, 103, 104	sylancl 668	. . . . . . . . . . . . 13 $/\$ $/\$
106		hashun3 12563	. . . . . . . . . . . . 13 $/\$
107	105, 82, 106	syl2anc 667	. . . . . . . . . . . 12 $/\$ $/\$
108		indi 3689	. . . . . . . . . . . . 13
109	108	fveq2i 5868	. . . . . . . . . . . 12
110		inindi 3649	. . . . . . . . . . . . . 14
111	110	fveq2i 5868	. . . . . . . . . . . . 13
112	111	oveq2i 6301	. . . . . . . . . . . 12
113	107, 109, 112	3eqtr4g 2510	. . . . . . . . . . 11 $/\$ $/\$
114		hashcl 12538	. . . . . . . . . . . . . 14
115	105, 114	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
116	115	nn0cnd 10927	. . . . . . . . . . . 12 $/\$ $/\$
117		hashcl 12538	. . . . . . . . . . . . . 14
118	82, 117	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
119	118	nn0cnd 10927	. . . . . . . . . . . 12 $/\$ $/\$
120		inss1 3652	. . . . . . . . . . . . . . 15
121		ssfi 7792	. . . . . . . . . . . . . . 15 $/\$
122	79, 120, 121	sylancl 668	. . . . . . . . . . . . . 14 $/\$ $/\$
123		hashcl 12538	. . . . . . . . . . . . . 14
124	122, 123	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
125	124	nn0cnd 10927	. . . . . . . . . . . 12 $/\$ $/\$
126	116, 119, 125	addsubassd 10006	. . . . . . . . . . 11 $/\$ $/\$
127	113, 126	eqtrd 2485	. . . . . . . . . 10 $/\$ $/\$
128	127	oveq2d 6306	. . . . . . . . 9 $/\$ $/\$
129		hashcl 12538	. . . . . . . . . . . 12
130	129	adantl 468	. . . . . . . . . . 11 $/\$ $/\$
131	130	nn0cnd 10927	. . . . . . . . . 10 $/\$ $/\$
132	119, 125	subcld 9986	. . . . . . . . . 10 $/\$ $/\$
133	131, 116, 132	subsub4d 10017	. . . . . . . . 9 $/\$ $/\$
134	128, 133	eqtr4d 2488	. . . . . . . 8 $/\$ $/\$
135	134	adantr 467	. . . . . . 7 $/\$ $/\$ $/\$
136		disjdif 3839	. . . . . . . . . . 11 $\$
137	136	a1i 11	. . . . . . . . . 10 $/\$ $/\$ $\$
138		ssun1 3597	. . . . . . . . . . . . . 14
139		sspwb 4649	. . . . . . . . . . . . . 14
140	138, 139	mpbi 212	. . . . . . . . . . . . 13
141		undif 3848	. . . . . . . . . . . . 13 $\$
142	140, 141	mpbi 212	. . . . . . . . . . . 12 $\$
143	142	eqcomi 2460	. . . . . . . . . . 11 $\$
144	143	a1i 11	. . . . . . . . . 10 $/\$ $/\$ $\$
145		simpll 760	. . . . . . . . . . . 12 $/\$ $/\$
146		snfi 7650	. . . . . . . . . . . 12
147		unfi 7838	. . . . . . . . . . . 12 $/\$
148	145, 146, 147	sylancl 668	. . . . . . . . . . 11 $/\$ $/\$
149		pwfi 7869	. . . . . . . . . . 11
150	148, 149	sylib 200	. . . . . . . . . 10 $/\$ $/\$
151	55	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152		elpwi 3960	. . . . . . . . . . . . . 14
153		ssfi 7792	. . . . . . . . . . . . . 14 $/\$
154	148, 152, 153	syl2an 480	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
155		hashcl 12538	. . . . . . . . . . . . 13
156	154, 155	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
157	151, 156	expcld 12416	. . . . . . . . . . 11 $/\$ $/\$ $/\$
158		simplr 762	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
159		inss1 3652	. . . . . . . . . . . . . 14
160		ssfi 7792	. . . . . . . . . . . . . 14 $/\$
161	158, 159, 160	sylancl 668	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
162		hashcl 12538	. . . . . . . . . . . . 13
163	161, 162	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
164	163	nn0cnd 10927	. . . . . . . . . . 11 $/\$ $/\$ $/\$
165	157, 164	mulcld 9663	. . . . . . . . . 10 $/\$ $/\$ $/\$
166	137, 144, 150, 165	fsumsplit 13806	. . . . . . . . 9 $/\$ $/\$ $\$
167		fveq2 5865	. . . . . . . . . . . . . 14
168	167	oveq2d 6306	. . . . . . . . . . . . 13
169		inteq 4237	. . . . . . . . . . . . . . . 16
170	27	intunsn 4274	. . . . . . . . . . . . . . . 16
171	169, 170	syl6eq 2501	. . . . . . . . . . . . . . 15
172	171	ineq2d 3634	. . . . . . . . . . . . . 14
173	172	fveq2d 5869	. . . . . . . . . . . . 13
174	168, 173	oveq12d 6308	. . . . . . . . . . . 12
175		pwfi 7869	. . . . . . . . . . . . 13
176	145, 175	sylib 200	. . . . . . . . . . . 12 $/\$ $/\$
177		eqid 2451	. . . . . . . . . . . . 13
178		elpwi 3960	. . . . . . . . . . . . . . . . 17
179	178	adantl 468	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
180		unss1 3603	. . . . . . . . . . . . . . . 16
181	179, 180	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
182		vex 3048	. . . . . . . . . . . . . . . . 17
183		snex 4641	. . . . . . . . . . . . . . . . 17
184	182, 183	unex 6589	. . . . . . . . . . . . . . . 16
185	184	elpw 3957	. . . . . . . . . . . . . . 15
186	181, 185	sylibr 216	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
187		simpllr 769	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
188		elpwi 3960	. . . . . . . . . . . . . . . 16
189		ssun2 3598	. . . . . . . . . . . . . . . . . . 19
190	27	snss 4096	. . . . . . . . . . . . . . . . . . 19
191	189, 190	mpbir 213	. . . . . . . . . . . . . . . . . 18
192	191	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
193		ssel 3426	. . . . . . . . . . . . . . . . 17
194	192, 193	syl5com 31	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
195	188, 194	syl5 33	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
196	187, 195	mtod 181	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
197	186, 196	eldifd 3415	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
198		eldifi 3555	. . . . . . . . . . . . . . . . . 18 $\$
199	198	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
200	199	elpwid 3961	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
201		uncom 3578	. . . . . . . . . . . . . . . 16
202	200, 201	syl6sseq 3478	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
203		ssundif 3851	. . . . . . . . . . . . . . 15 $\$
204	202, 203	sylib 200	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
205		vex 3048	. . . . . . . . . . . . . . 15
206	205	elpw2 4567	. . . . . . . . . . . . . 14 $\$ $\$
207	204, 206	sylibr 216	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
208		elpwunsn 4012	. . . . . . . . . . . . . . . . . . 19 $\$
209	208	ad2antll 735	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$
210	209	snssd 4117	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\$
211		ssequn2 3607	. . . . . . . . . . . . . . . . 17
212	210, 211	sylib 200	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $\$
213	212	eqcomd 2457	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$
214		uneq1 3581	. . . . . . . . . . . . . . . . 17 $\$ $\$
215		undif1 3842	. . . . . . . . . . . . . . . . 17 $\$
216	214, 215	syl6eq 2501	. . . . . . . . . . . . . . . 16 $\$
217	216	eqeq2d 2461	. . . . . . . . . . . . . . 15 $\$
218	213, 217	syl5ibrcom 226	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $\$ $\$
219	178	ad2antrl 734	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$
220		simpllr 769	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$
221	219, 220	ssneldd 3435	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\$
222		difsnb 4114	. . . . . . . . . . . . . . . . 17 $\$
223	221, 222	sylib 200	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $\$ $\$
224	223	eqcomd 2457	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$ $\$
225		difeq1 3544	. . . . . . . . . . . . . . . . 17 $\$ $\$
226		difun2 3847	. . . . . . . . . . . . . . . . 17 $\$ $\$
227	225, 226	syl6eq 2501	. . . . . . . . . . . . . . . 16 $\$ $\$
228	227	eqeq2d 2461	. . . . . . . . . . . . . . 15 $\$ $\$
229	224, 228	syl5ibrcom 226	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $\$ $\$
230	218, 229	impbid 194	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\$ $\$
231	177, 197, 207, 230	f1o2d 6521	. . . . . . . . . . . 12 $/\$ $/\$ $\$
232		uneq1 3581	. . . . . . . . . . . . . 14
233		vex 3048	. . . . . . . . . . . . . . 15
234	233, 183	unex 6589	. . . . . . . . . . . . . 14
235	232, 177, 234	fvmpt 5948	. . . . . . . . . . . . 13
236	235	adantl 468	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
237	198, 165	sylan2 477	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
238	174, 176, 231, 236, 237	fsumf1o 13789	. . . . . . . . . . 11 $/\$ $/\$ $\$
239		uneq1 3581	. . . . . . . . . . . . . . . 16
240	239	fveq2d 5869	. . . . . . . . . . . . . . 15
241	240	oveq2d 6306	. . . . . . . . . . . . . 14
242		inteq 4237	. . . . . . . . . . . . . . . . 17
243	242	ineq1d 3633	. . . . . . . . . . . . . . . 16
244	243	ineq2d 3634	. . . . . . . . . . . . . . 15
245	244	fveq2d 5869	. . . . . . . . . . . . . 14
246	241, 245	oveq12d 6308	. . . . . . . . . . . . 13
247	246	cbvsumv 13762	. . . . . . . . . . . 12
248		elpwi 3960	. . . . . . . . . . . . . . . . . . . 20
249		ssfi 7792	. . . . . . . . . . . . . . . . . . . 20 $/\$
250	145, 248, 249	syl2an 480	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
251	248	adantl 468	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
252		simpllr 769	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
253	251, 252	ssneldd 3435	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
254		hashunsng 12571	. . . . . . . . . . . . . . . . . . . 20 $/\$
255	27, 254	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 $/\$
256	250, 253, 255	syl2anc 667	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
257	256	oveq2d 6306	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
258	55	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
259	250, 155	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
260	258, 259	expp1d 12417	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
261	257, 260	eqtrd 2485	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
262	140	sseli 3428	. . . . . . . . . . . . . . . . . 18
263	262, 157	sylan2 477	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
264	258, 263	mulcomd 9664	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
265	263	mulm1d 10070	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
266	261, 264, 265	3eqtr2d 2491	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
267	266	oveq1d 6305	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
268		inss1 3652	. . . . . . . . . . . . . . . . . . 19
269		ssfi 7792	. . . . . . . . . . . . . . . . . . 19 $/\$
270	158, 268, 269	sylancl 668	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
271		hashcl 12538	. . . . . . . . . . . . . . . . . 18
272	270, 271	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
273	272	nn0cnd 10927	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
274	262, 273	sylan2 477	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
275	263, 274	mulneg1d 10071	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
276	267, 275	eqtrd 2485	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
277	276	sumeq2dv 13769	. . . . . . . . . . . 12 $/\$ $/\$
278	247, 277	syl5eq 2497	. . . . . . . . . . 11 $/\$ $/\$
279	157, 273	mulcld 9663	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
280	262, 279	sylan2 477	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
281	176, 280	fsumneg 13848	. . . . . . . . . . 11 $/\$ $/\$
282	238, 278, 281	3eqtrd 2489	. . . . . . . . . 10 $/\$ $/\$ $\$
283	282	oveq2d 6306	. . . . . . . . 9 $/\$ $/\$ $\$
284	140	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
285	284	sselda 3432	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
286	285, 165	syldan 473	. . . . . . . . . . 11 $/\$ $/\$ $/\$
287	176, 286	fsumcl 13799	. . . . . . . . . 10 $/\$ $/\$
288	285, 279	syldan 473	. . . . . . . . . . 11 $/\$ $/\$ $/\$
289	176, 288	fsumcl 13799	. . . . . . . . . 10 $/\$ $/\$
290	287, 289	negsubd 9992	. . . . . . . . 9 $/\$ $/\$
291	166, 283, 290	3eqtrd 2489	. . . . . . . 8 $/\$ $/\$
292	291	adantr 467	. . . . . . 7 $/\$ $/\$ $/\$
293	102, 135, 292	3eqtr4d 2495	. . . . . 6 $/\$ $/\$ $/\$
294	293	ex 436	. . . . 5 $/\$ $/\$
295	294	ralrimdva 2806	. . . 4 $/\$
296		ineq1 3627	. . . . . . . 8
297	296	fveq2d 5869	. . . . . . 7
298	67, 297	oveq12d 6308	. . . . . 6
299		ineq1 3627	. . . . . . . . 9
300	299	fveq2d 5869	. . . . . . . 8
301	300	oveq2d 6306	. . . . . . 7
302	301	sumeq2sdv 13770	. . . . . 6
303	298, 302	eqeq12d 2466	. . . . 5
304	303	cbvralv 3019	. . . 4
305	295, 304	syl6ibr 231	. . 3 $/\$
306	16, 24, 38, 46, 66, 305	findcard2s 7812	. 2
307		fveq2 5865	. . . . 5
308		ineq1 3627	. . . . . 6
309	308	fveq2d 5869	. . . . 5
310	307, 309	oveq12d 6308	. . . 4
311		simpl 459	. . . . . . . 8 $/\$
312	311	ineq1d 3633	. . . . . . 7 $/\$
313	312	fveq2d 5869	. . . . . 6 $/\$
314	313	oveq2d 6306	. . . . 5 $/\$
315	314	sumeq2dv 13769	. . . 4
316	310, 315	eqeq12d 2466	. . 3
317	316	rspccva 3149	. 2 $/\$
318	306, 317	sylan 474	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 371

wceq 1444

wcel 1887

wral 2737

cvv 3045 $\$ cdif 3401

cun 3402

cin 3403

wss 3404

c0 3731

cpw 3951

csn 3968

cuni 4198

cint 4234

cmpt 4461

cfv 5582 (class class class)co 6290

cfn 7569

cc 9537

cc0 9539

c1 9540

caddc 9542

cmul 9544

cmin 9860

cneg 9861

cn0 10869

cexp 12272

chash 12515

csu 13752

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-inf2 8146 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616 ax-pre-sup 9617

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-fal 1450 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-se 4794 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-isom 5591 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-om 6693 df-1st 6793 df-2nd 6794 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-2o 7183 df-oadd 7186 df-er 7363 df-map 7474 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-sup 7956 df-oi 8025 df-card 8373 df-cda 8598 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-div 10270 df-nn 10610 df-2 10668 df-3 10669 df-n0 10870 df-z 10938 df-uz 11160 df-rp 11303 df-fz 11785 df-fzo 11916 df-seq 12214 df-exp 12273 df-hash 12516 df-cj 13162 df-re 13163 df-im 13164 df-sqrt 13298 df-abs 13299 df-clim 13552 df-sum 13753

This theorem is referenced by: incexc 13895

W3C validator