aannenlem2 - Metamath Proof Explorer

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

Theorem aannenlem2 20199

Description: Lemma for aannen 20201. (Contributed by Stefan O'Rear, 16-Nov-2014.)

**Hypothesis**
Ref	Expression
aannenlem.a	Poly $/\$ deg $/\$ coeff

**Assertion**
Ref	Expression
aannenlem2

Distinct variable group:

Allowed substitution hints:

(

)

Proof of Theorem aannenlem2 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp3 959	. . . . . . . . . 10 Poly $\$ $/\$ $/\$
2		eldifi 3429	. . . . . . . . . . . . . 14 Poly $\$ Poly
3	2	adantr 452	. . . . . . . . . . . . 13 Poly $\$ $/\$ Poly
4	3	3adant2 976	. . . . . . . . . . . 12 Poly $\$ $/\$ $/\$ Poly
5		eldifsni 3888	. . . . . . . . . . . . . . 15 Poly $\$
6	5	adantr 452	. . . . . . . . . . . . . 14 Poly $\$ $/\$
7		0nn0 10192	. . . . . . . . . . . . . . . . . 18
8		dgrcl 20105	. . . . . . . . . . . . . . . . . . 19 Poly deg
9	3, 8	syl 16	. . . . . . . . . . . . . . . . . 18 Poly $\$ $/\$ deg
10		prssi 3914	. . . . . . . . . . . . . . . . . 18 $/\$ deg deg
11	7, 9, 10	sylancr 645	. . . . . . . . . . . . . . . . 17 Poly $\$ $/\$ deg
12		ssrab2 3388	. . . . . . . . . . . . . . . . . 18 deg coeff
13	12	a1i 11	. . . . . . . . . . . . . . . . 17 Poly $\$ $/\$ deg coeff
14	11, 13	unssd 3483	. . . . . . . . . . . . . . . 16 Poly $\$ $/\$ deg deg coeff
15		nn0ssre 10181	. . . . . . . . . . . . . . . . 17
16		ressxr 9085	. . . . . . . . . . . . . . . . 17
17	15, 16	sstri 3317	. . . . . . . . . . . . . . . 16
18	14, 17	syl6ss 3320	. . . . . . . . . . . . . . 15 Poly $\$ $/\$ deg deg coeff
19		fvex 5701	. . . . . . . . . . . . . . . . 17 deg
20	19	prid2 3873	. . . . . . . . . . . . . . . 16 deg deg
21		elun1 3474	. . . . . . . . . . . . . . . 16 deg deg deg deg deg coeff
22	20, 21	ax-mp 8	. . . . . . . . . . . . . . 15 deg deg deg coeff
23		supxrub 10859	. . . . . . . . . . . . . . 15 deg deg coeff $/\$ deg deg deg coeff deg deg deg coeff
24	18, 22, 23	sylancl 644	. . . . . . . . . . . . . 14 Poly $\$ $/\$ deg deg deg coeff
25	18	adantr 452	. . . . . . . . . . . . . . . 16 Poly $\$ $/\$ $/\$ deg deg coeff
26		fveq2 5687	. . . . . . . . . . . . . . . . . . . 20 coeff coeff
27		abs0 12045	. . . . . . . . . . . . . . . . . . . 20
28	26, 27	syl6eq 2452	. . . . . . . . . . . . . . . . . . 19 coeff coeff
29		c0ex 9041	. . . . . . . . . . . . . . . . . . . . 21
30	29	prid1 3872	. . . . . . . . . . . . . . . . . . . 20 deg
31		elun1 3474	. . . . . . . . . . . . . . . . . . . 20 deg deg deg coeff
32	30, 31	ax-mp 8	. . . . . . . . . . . . . . . . . . 19 deg deg coeff
33	28, 32	syl6eqel 2492	. . . . . . . . . . . . . . . . . 18 coeff coeff deg deg coeff
34	33	adantl 453	. . . . . . . . . . . . . . . . 17 Poly $\$ $/\$ $/\$ $/\$ coeff coeff deg deg coeff
35		0z 10249	. . . . . . . . . . . . . . . . . . . . . . 23
36		eqid 2404	. . . . . . . . . . . . . . . . . . . . . . . 24 coeff coeff
37	36	coef2 20103	. . . . . . . . . . . . . . . . . . . . . . 23 Poly $/\$ coeff
38	3, 35, 37	sylancl 644	. . . . . . . . . . . . . . . . . . . . . 22 Poly $\$ $/\$ coeff
39	38	ffvelrnda 5829	. . . . . . . . . . . . . . . . . . . . 21 Poly $\$ $/\$ $/\$ coeff
40		nn0abscl 12072	. . . . . . . . . . . . . . . . . . . . 21 coeff coeff
41	39, 40	syl 16	. . . . . . . . . . . . . . . . . . . 20 Poly $\$ $/\$ $/\$ coeff
42	41	adantr 452	. . . . . . . . . . . . . . . . . . 19 Poly $\$ $/\$ $/\$ $/\$ coeff coeff
43		simplr 732	. . . . . . . . . . . . . . . . . . . . 21 Poly $\$ $/\$ $/\$ $/\$ coeff
44	9	ad2antrr 707	. . . . . . . . . . . . . . . . . . . . 21 Poly $\$ $/\$ $/\$ $/\$ coeff deg
45	3	ad2antrr 707	. . . . . . . . . . . . . . . . . . . . . 22 Poly $\$ $/\$ $/\$ $/\$ coeff Poly
46		simpr 448	. . . . . . . . . . . . . . . . . . . . . 22 Poly $\$ $/\$ $/\$ $/\$ coeff coeff
47		eqid 2404	. . . . . . . . . . . . . . . . . . . . . . 23 deg deg
48	36, 47	dgrub 20106	. . . . . . . . . . . . . . . . . . . . . 22 Poly $/\$ $/\$ coeff deg
49	45, 43, 46, 48	syl3anc 1184	. . . . . . . . . . . . . . . . . . . . 21 Poly $\$ $/\$ $/\$ $/\$ coeff deg
50		elfz2nn0 11038	. . . . . . . . . . . . . . . . . . . . 21 deg $/\$ deg $/\$ deg
51	43, 44, 49, 50	syl3anbrc 1138	. . . . . . . . . . . . . . . . . . . 20 Poly $\$ $/\$ $/\$ $/\$ coeff deg
52		eqid 2404	. . . . . . . . . . . . . . . . . . . 20 coeff coeff
53		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . 23 coeff coeff
54	53	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . . 22 coeff coeff
55	54	eqeq2d 2415	. . . . . . . . . . . . . . . . . . . . 21 coeff coeff coeff coeff
56	55	rspcev 3012	. . . . . . . . . . . . . . . . . . . 20 deg $/\$ coeff coeff degcoeff coeff
57	51, 52, 56	sylancl 644	. . . . . . . . . . . . . . . . . . 19 Poly $\$ $/\$ $/\$ $/\$ coeff degcoeff coeff
58		eqeq1 2410	. . . . . . . . . . . . . . . . . . . . 21 coeff coeff coeff coeff
59	58	rexbidv 2687	. . . . . . . . . . . . . . . . . . . 20 coeff deg coeff degcoeff coeff
60	59	elrab 3052	. . . . . . . . . . . . . . . . . . 19 coeff deg coeff coeff $/\$ degcoeff coeff
61	42, 57, 60	sylanbrc 646	. . . . . . . . . . . . . . . . . 18 Poly $\$ $/\$ $/\$ $/\$ coeff coeff deg coeff
62		elun2 3475	. . . . . . . . . . . . . . . . . 18 coeff deg coeff coeff deg deg coeff
63	61, 62	syl 16	. . . . . . . . . . . . . . . . 17 Poly $\$ $/\$ $/\$ $/\$ coeff coeff deg deg coeff
64	34, 63	pm2.61dane 2645	. . . . . . . . . . . . . . . 16 Poly $\$ $/\$ $/\$ coeff deg deg coeff
65		supxrub 10859	. . . . . . . . . . . . . . . 16 deg deg coeff $/\$ coeff deg deg coeff coeff deg deg coeff
66	25, 64, 65	syl2anc 643	. . . . . . . . . . . . . . 15 Poly $\$ $/\$ $/\$ coeff deg deg coeff
67	66	ralrimiva 2749	. . . . . . . . . . . . . 14 Poly $\$ $/\$ coeff deg deg coeff
68	6, 24, 67	3jca 1134	. . . . . . . . . . . . 13 Poly $\$ $/\$ $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
69	68	3adant2 976	. . . . . . . . . . . 12 Poly $\$ $/\$ $/\$ $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
70		neeq1 2575	. . . . . . . . . . . . . 14
71		fveq2 5687	. . . . . . . . . . . . . . 15 deg deg
72	71	breq1d 4182	. . . . . . . . . . . . . 14 deg deg deg coeff deg deg deg coeff
73		fveq2 5687	. . . . . . . . . . . . . . . . . 18 coeff coeff
74	73	fveq1d 5689	. . . . . . . . . . . . . . . . 17 coeff coeff
75	74	fveq2d 5691	. . . . . . . . . . . . . . . 16 coeff coeff
76	75	breq1d 4182	. . . . . . . . . . . . . . 15 coeff deg deg coeff coeff deg deg coeff
77	76	ralbidv 2686	. . . . . . . . . . . . . 14 coeff deg deg coeff coeff deg deg coeff
78	70, 72, 77	3anbi123d 1254	. . . . . . . . . . . . 13 $/\$ deg deg deg coeff $/\$ coeff deg deg coeff $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
79	78	elrab 3052	. . . . . . . . . . . 12 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
80	4, 69, 79	sylanbrc 646	. . . . . . . . . . 11 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
81		simp2 958	. . . . . . . . . . 11 Poly $\$ $/\$ $/\$
82		fveq1 5686	. . . . . . . . . . . . 13
83	82	eqeq1d 2412	. . . . . . . . . . . 12
84	83	rspcev 3012	. . . . . . . . . . 11 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
85	80, 81, 84	syl2anc 643	. . . . . . . . . 10 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
86		fveq2 5687	. . . . . . . . . . . . 13
87	86	eqeq1d 2412	. . . . . . . . . . . 12
88	87	rexbidv 2687	. . . . . . . . . . 11 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
89	88	elrab 3052	. . . . . . . . . 10 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
90	1, 85, 89	sylanbrc 646	. . . . . . . . 9 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
91		prfi 7340	. . . . . . . . . . . . . . 15 deg
92		fzfi 11266	. . . . . . . . . . . . . . . . 17 deg
93		abrexfi 7365	. . . . . . . . . . . . . . . . 17 deg deg coeff
94	92, 93	ax-mp 8	. . . . . . . . . . . . . . . 16 deg coeff
95		rabssab 3390	. . . . . . . . . . . . . . . 16 deg coeff deg coeff
96		ssfi 7288	. . . . . . . . . . . . . . . 16 deg coeff $/\$ deg coeff deg coeff deg coeff
97	94, 95, 96	mp2an 654	. . . . . . . . . . . . . . 15 deg coeff
98		unfi 7333	. . . . . . . . . . . . . . 15 deg $/\$ deg coeff deg deg coeff
99	91, 97, 98	mp2an 654	. . . . . . . . . . . . . 14 deg deg coeff
100	99	a1i 11	. . . . . . . . . . . . 13 Poly $\$ $/\$ deg deg coeff
101		ne0i 3594	. . . . . . . . . . . . . . 15 deg deg deg coeff deg deg coeff
102	22, 101	ax-mp 8	. . . . . . . . . . . . . 14 deg deg coeff
103	102	a1i 11	. . . . . . . . . . . . 13 Poly $\$ $/\$ deg deg coeff
104		xrltso 10690	. . . . . . . . . . . . . 14
105		fisupcl 7428	. . . . . . . . . . . . . 14 $/\$ deg deg coeff $/\$ deg deg coeff $/\$ deg deg coeff deg deg coeff deg deg coeff
106	104, 105	mpan 652	. . . . . . . . . . . . 13 deg deg coeff $/\$ deg deg coeff $/\$ deg deg coeff deg deg coeff deg deg coeff
107	100, 103, 18, 106	syl3anc 1184	. . . . . . . . . . . 12 Poly $\$ $/\$ deg deg coeff deg deg coeff
108	14, 107	sseldd 3309	. . . . . . . . . . 11 Poly $\$ $/\$ deg deg coeff
109	108	3adant2 976	. . . . . . . . . 10 Poly $\$ $/\$ $/\$ deg deg coeff
110		eqidd 2405	. . . . . . . . . 10 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
111		breq2 4176	. . . . . . . . . . . . . . . 16 deg deg coeff deg deg deg deg coeff
112		breq2 4176	. . . . . . . . . . . . . . . . 17 deg deg coeff coeff coeff deg deg coeff
113	112	ralbidv 2686	. . . . . . . . . . . . . . . 16 deg deg coeff coeff coeff deg deg coeff
114	111, 113	3anbi23d 1257	. . . . . . . . . . . . . . 15 deg deg coeff $/\$ deg $/\$ coeff $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
115	114	rabbidv 2908	. . . . . . . . . . . . . 14 deg deg coeff Poly $/\$ deg $/\$ coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
116	115	rexeqdv 2871	. . . . . . . . . . . . 13 deg deg coeff Poly $/\$ deg $/\$ coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
117	116	rabbidv 2908	. . . . . . . . . . . 12 deg deg coeff Poly $/\$ deg $/\$ coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
118	117	eqeq2d 2415	. . . . . . . . . . 11 deg deg coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg $/\$ coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
119	118	rspcev 3012	. . . . . . . . . 10 deg deg coeff $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg $/\$ coeff
120	109, 110, 119	syl2anc 643	. . . . . . . . 9 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg $/\$ coeff
121		cnex 9027	. . . . . . . . . . 11
122	121	rabex 4314	. . . . . . . . . 10 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
123		eleq2 2465	. . . . . . . . . . 11 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
124		eqeq1 2410	. . . . . . . . . . . 12 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg $/\$ coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg $/\$ coeff
125	124	rexbidv 2687	. . . . . . . . . . 11 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg $/\$ coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg $/\$ coeff
126	123, 125	anbi12d 692	. . . . . . . . . 10 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff $/\$ Poly $/\$ deg $/\$ coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg $/\$ coeff
127	122, 126	spcev 3003	. . . . . . . . 9 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg $/\$ coeff $/\$ Poly $/\$ deg $/\$ coeff
128	90, 120, 127	syl2anc 643	. . . . . . . 8 Poly $\$ $/\$ $/\$ $/\$ Poly $/\$ deg $/\$ coeff
129	128	3exp 1152	. . . . . . 7 Poly $\$ $/\$ Poly $/\$ deg $/\$ coeff
130	129	rexlimiv 2784	. . . . . 6 Poly $\$ $/\$ Poly $/\$ deg $/\$ coeff
131	130	impcom 420	. . . . 5 $/\$ Poly $\$ $/\$ Poly $/\$ deg $/\$ coeff
132		eleq2 2465	. . . . . . . . 9 Poly $/\$ deg $/\$ coeff Poly $/\$ deg $/\$ coeff
133	87	rexbidv 2687	. . . . . . . . . . 11 Poly $/\$ deg $/\$ coeff Poly $/\$ deg $/\$ coeff
134	133	elrab 3052	. . . . . . . . . 10 Poly $/\$ deg $/\$ coeff $/\$ Poly $/\$ deg $/\$ coeff
135		simp1 957	. . . . . . . . . . . . . . 15 $/\$ deg $/\$ coeff
136	135	anim2i 553	. . . . . . . . . . . . . 14 Poly $/\$ $/\$ deg $/\$ coeff Poly $/\$
137	71	breq1d 4182	. . . . . . . . . . . . . . . 16 deg deg
138	75	breq1d 4182	. . . . . . . . . . . . . . . . 17 coeff coeff
139	138	ralbidv 2686	. . . . . . . . . . . . . . . 16 coeff coeff
140	70, 137, 139	3anbi123d 1254	. . . . . . . . . . . . . . 15 $/\$ deg $/\$ coeff $/\$ deg $/\$ coeff
141	140	elrab 3052	. . . . . . . . . . . . . 14 Poly $/\$ deg $/\$ coeff Poly $/\$ $/\$ deg $/\$ coeff
142		eldifsn 3887	. . . . . . . . . . . . . 14 Poly $\$ Poly $/\$
143	136, 141, 142	3imtr4i 258	. . . . . . . . . . . . 13 Poly $/\$ deg $/\$ coeff Poly $\$
144	143	ssriv 3312	. . . . . . . . . . . 12 Poly $/\$ deg $/\$ coeff Poly $\$
145		ssrexv 3368	. . . . . . . . . . . . 13 Poly $/\$ deg $/\$ coeff Poly $\$ Poly $/\$ deg $/\$ coeff Poly $\$
146	83	cbvrexv 2893	. . . . . . . . . . . . 13 Poly $\$ Poly $\$
147	145, 146	syl6ib 218	. . . . . . . . . . . 12 Poly $/\$ deg $/\$ coeff Poly $\$ Poly $/\$ deg $/\$ coeff Poly $\$
148	144, 147	ax-mp 8	. . . . . . . . . . 11 Poly $/\$ deg $/\$ coeff Poly $\$
149	148	anim2i 553	. . . . . . . . . 10 $/\$ Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
150	134, 149	sylbi 188	. . . . . . . . 9 Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
151	132, 150	syl6bi 220	. . . . . . . 8 Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
152	151	rexlimivw 2786	. . . . . . 7 Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
153	152	impcom 420	. . . . . 6 $/\$ Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
154	153	exlimiv 1641	. . . . 5 $/\$ Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
155	131, 154	impbii 181	. . . 4 $/\$ Poly $\$ $/\$ Poly $/\$ deg $/\$ coeff
156		elaa 20186	. . . 4 $/\$ Poly $\$
157		eluniab 3987	. . . 4 Poly $/\$ deg $/\$ coeff $/\$ Poly $/\$ deg $/\$ coeff
158	155, 156, 157	3bitr4i 269	. . 3 Poly $/\$ deg $/\$ coeff
159	158	eqriv 2401	. 2 Poly $/\$ deg $/\$ coeff
160		aannenlem.a	. . . 4 Poly $/\$ deg $/\$ coeff
161	160	rnmpt 5075	. . 3 Poly $/\$ deg $/\$ coeff
162	161	unieqi 3985	. 2 Poly $/\$ deg $/\$ coeff
163	159, 162	eqtr4i 2427	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 359 $/\$ w3a 936

wex 1547

wceq 1649

wcel 1721

cab 2390

wne 2567

wral 2666

wrex 2667

crab 2670 $\$ cdif 3277

cun 3278

wss 3280

c0 3588

csn 3774

cpr 3775

cuni 3975 class class class wbr 4172

cmpt 4226

wor 4462

crn 4838

wf 5409

cfv 5413 (class class class)co 6040

cfn 7068

csup 7403

cc 8944

cr 8945

cc0 8946

cxr 9075

clt 9076

cle 9077

cn0 10177

cz 10238

cfz 10999

cabs 11994

c0p 19514 Polycply 20056 coeffccoe 20058 degcdgr 20059

caa 20184

This theorem is referenced by: aannenlem3 20200

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-inf2 7552 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024 ax-addf 9025

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-se 4502 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-of 6264 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-oadd 6687 df-er 6864 df-map 6979 df-pm 6980 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-sup 7404 df-oi 7435 df-card 7782 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-3 10015 df-n0 10178 df-z 10239 df-uz 10445 df-rp 10569 df-fz 11000 df-fzo 11091 df-fl 11157 df-seq 11279 df-exp 11338 df-hash 11574 df-cj 11859 df-re 11860 df-im 11861 df-sqr 11995 df-abs 11996 df-clim 12237 df-rlim 12238 df-sum 12435 df-0p 19515 df-ply 20060 df-coe 20062 df-dgr 20063 df-aa 20185

W3C validator