aannenlem2 - Metamath Proof Explorer

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

Theorem aannenlem2 21911

Description: Lemma for aannen 21913. (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 990	. . . . . . . . . 10 Poly $\$ $/\$ $/\$
2		eldifi 3576	. . . . . . . . . . . . . 14 Poly $\$ Poly
3	2	adantr 465	. . . . . . . . . . . . 13 Poly $\$ $/\$ Poly
4	3	3adant2 1007	. . . . . . . . . . . 12 Poly $\$ $/\$ $/\$ Poly
5		eldifsni 4099	. . . . . . . . . . . . . . 15 Poly $\$
6	5	adantr 465	. . . . . . . . . . . . . 14 Poly $\$ $/\$
7		0nn0 10695	. . . . . . . . . . . . . . . . . 18
8		dgrcl 21817	. . . . . . . . . . . . . . . . . . 19 Poly deg
9	3, 8	syl 16	. . . . . . . . . . . . . . . . . 18 Poly $\$ $/\$ deg
10		prssi 4127	. . . . . . . . . . . . . . . . . 18 $/\$ deg deg
11	7, 9, 10	sylancr 663	. . . . . . . . . . . . . . . . 17 Poly $\$ $/\$ deg
12		ssrab2 3535	. . . . . . . . . . . . . . . . . 18 deg coeff
13	12	a1i 11	. . . . . . . . . . . . . . . . 17 Poly $\$ $/\$ deg coeff
14	11, 13	unssd 3630	. . . . . . . . . . . . . . . 16 Poly $\$ $/\$ deg deg coeff
15		nn0ssre 10684	. . . . . . . . . . . . . . . . 17
16		ressxr 9528	. . . . . . . . . . . . . . . . 17
17	15, 16	sstri 3463	. . . . . . . . . . . . . . . 16
18	14, 17	syl6ss 3466	. . . . . . . . . . . . . . 15 Poly $\$ $/\$ deg deg coeff
19		fvex 5799	. . . . . . . . . . . . . . . . 17 deg
20	19	prid2 4082	. . . . . . . . . . . . . . . 16 deg deg
21		elun1 3621	. . . . . . . . . . . . . . . 16 deg deg deg deg deg coeff
22	20, 21	ax-mp 5	. . . . . . . . . . . . . . 15 deg deg deg coeff
23		supxrub 11388	. . . . . . . . . . . . . . 15 deg deg coeff $/\$ deg deg deg coeff deg deg deg coeff
24	18, 22, 23	sylancl 662	. . . . . . . . . . . . . 14 Poly $\$ $/\$ deg deg deg coeff
25	18	adantr 465	. . . . . . . . . . . . . . . 16 Poly $\$ $/\$ $/\$ deg deg coeff
26		fveq2 5789	. . . . . . . . . . . . . . . . . . . 20 coeff coeff
27		abs0 12876	. . . . . . . . . . . . . . . . . . . 20
28	26, 27	syl6eq 2508	. . . . . . . . . . . . . . . . . . 19 coeff coeff
29		c0ex 9481	. . . . . . . . . . . . . . . . . . . . 21
30	29	prid1 4081	. . . . . . . . . . . . . . . . . . . 20 deg
31		elun1 3621	. . . . . . . . . . . . . . . . . . . 20 deg deg deg coeff
32	30, 31	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 deg deg coeff
33	28, 32	syl6eqel 2547	. . . . . . . . . . . . . . . . . 18 coeff coeff deg deg coeff
34	33	adantl 466	. . . . . . . . . . . . . . . . 17 Poly $\$ $/\$ $/\$ $/\$ coeff coeff deg deg coeff
35		0z 10758	. . . . . . . . . . . . . . . . . . . . . . 23
36		eqid 2451	. . . . . . . . . . . . . . . . . . . . . . . 24 coeff coeff
37	36	coef2 21815	. . . . . . . . . . . . . . . . . . . . . . 23 Poly $/\$ coeff
38	3, 35, 37	sylancl 662	. . . . . . . . . . . . . . . . . . . . . 22 Poly $\$ $/\$ coeff
39	38	ffvelrnda 5942	. . . . . . . . . . . . . . . . . . . . 21 Poly $\$ $/\$ $/\$ coeff
40		nn0abscl 12903	. . . . . . . . . . . . . . . . . . . . 21 coeff coeff
41	39, 40	syl 16	. . . . . . . . . . . . . . . . . . . 20 Poly $\$ $/\$ $/\$ coeff
42	41	adantr 465	. . . . . . . . . . . . . . . . . . 19 Poly $\$ $/\$ $/\$ $/\$ coeff coeff
43		simplr 754	. . . . . . . . . . . . . . . . . . . . 21 Poly $\$ $/\$ $/\$ $/\$ coeff
44	9	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 Poly $\$ $/\$ $/\$ $/\$ coeff deg
45	3	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 22 Poly $\$ $/\$ $/\$ $/\$ coeff Poly
46		simpr 461	. . . . . . . . . . . . . . . . . . . . . 22 Poly $\$ $/\$ $/\$ $/\$ coeff coeff
47		eqid 2451	. . . . . . . . . . . . . . . . . . . . . . 23 deg deg
48	36, 47	dgrub 21818	. . . . . . . . . . . . . . . . . . . . . 22 Poly $/\$ $/\$ coeff deg
49	45, 43, 46, 48	syl3anc 1219	. . . . . . . . . . . . . . . . . . . . 21 Poly $\$ $/\$ $/\$ $/\$ coeff deg
50		elfz2nn0 11581	. . . . . . . . . . . . . . . . . . . . 21 deg $/\$ deg $/\$ deg
51	43, 44, 49, 50	syl3anbrc 1172	. . . . . . . . . . . . . . . . . . . 20 Poly $\$ $/\$ $/\$ $/\$ coeff deg
52		eqid 2451	. . . . . . . . . . . . . . . . . . . 20 coeff coeff
53		fveq2 5789	. . . . . . . . . . . . . . . . . . . . . . 23 coeff coeff
54	53	fveq2d 5793	. . . . . . . . . . . . . . . . . . . . . 22 coeff coeff
55	54	eqeq2d 2465	. . . . . . . . . . . . . . . . . . . . 21 coeff coeff coeff coeff
56	55	rspcev 3169	. . . . . . . . . . . . . . . . . . . 20 deg $/\$ coeff coeff degcoeff coeff
57	51, 52, 56	sylancl 662	. . . . . . . . . . . . . . . . . . 19 Poly $\$ $/\$ $/\$ $/\$ coeff degcoeff coeff
58		eqeq1 2455	. . . . . . . . . . . . . . . . . . . . 21 coeff coeff coeff coeff
59	58	rexbidv 2844	. . . . . . . . . . . . . . . . . . . 20 coeff deg coeff degcoeff coeff
60	59	elrab 3214	. . . . . . . . . . . . . . . . . . 19 coeff deg coeff coeff $/\$ degcoeff coeff
61	42, 57, 60	sylanbrc 664	. . . . . . . . . . . . . . . . . 18 Poly $\$ $/\$ $/\$ $/\$ coeff coeff deg coeff
62		elun2 3622	. . . . . . . . . . . . . . . . . 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 2766	. . . . . . . . . . . . . . . 16 Poly $\$ $/\$ $/\$ coeff deg deg coeff
65		supxrub 11388	. . . . . . . . . . . . . . . 16 deg deg coeff $/\$ coeff deg deg coeff coeff deg deg coeff
66	25, 64, 65	syl2anc 661	. . . . . . . . . . . . . . 15 Poly $\$ $/\$ $/\$ coeff deg deg coeff
67	66	ralrimiva 2822	. . . . . . . . . . . . . 14 Poly $\$ $/\$ coeff deg deg coeff
68	6, 24, 67	3jca 1168	. . . . . . . . . . . . 13 Poly $\$ $/\$ $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
69	68	3adant2 1007	. . . . . . . . . . . 12 Poly $\$ $/\$ $/\$ $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
70		neeq1 2729	. . . . . . . . . . . . . 14
71		fveq2 5789	. . . . . . . . . . . . . . 15 deg deg
72	71	breq1d 4400	. . . . . . . . . . . . . 14 deg deg deg coeff deg deg deg coeff
73		fveq2 5789	. . . . . . . . . . . . . . . . . 18 coeff coeff
74	73	fveq1d 5791	. . . . . . . . . . . . . . . . 17 coeff coeff
75	74	fveq2d 5793	. . . . . . . . . . . . . . . 16 coeff coeff
76	75	breq1d 4400	. . . . . . . . . . . . . . 15 coeff deg deg coeff coeff deg deg coeff
77	76	ralbidv 2839	. . . . . . . . . . . . . 14 coeff deg deg coeff coeff deg deg coeff
78	70, 72, 77	3anbi123d 1290	. . . . . . . . . . . . 13 $/\$ deg deg deg coeff $/\$ coeff deg deg coeff $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
79	78	elrab 3214	. . . . . . . . . . . 12 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
80	4, 69, 79	sylanbrc 664	. . . . . . . . . . 11 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
81		simp2 989	. . . . . . . . . . 11 Poly $\$ $/\$ $/\$
82		fveq1 5788	. . . . . . . . . . . . 13
83	82	eqeq1d 2453	. . . . . . . . . . . 12
84	83	rspcev 3169	. . . . . . . . . . 11 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
85	80, 81, 84	syl2anc 661	. . . . . . . . . 10 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
86		fveq2 5789	. . . . . . . . . . . . 13
87	86	eqeq1d 2453	. . . . . . . . . . . 12
88	87	rexbidv 2844	. . . . . . . . . . 11 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
89	88	elrab 3214	. . . . . . . . . 10 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
90	1, 85, 89	sylanbrc 664	. . . . . . . . 9 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
91		prfi 7687	. . . . . . . . . . . . . . 15 deg
92		fzfi 11895	. . . . . . . . . . . . . . . . 17 deg
93		abrexfi 7712	. . . . . . . . . . . . . . . . 17 deg deg coeff
94	92, 93	ax-mp 5	. . . . . . . . . . . . . . . 16 deg coeff
95		rabssab 3537	. . . . . . . . . . . . . . . 16 deg coeff deg coeff
96		ssfi 7634	. . . . . . . . . . . . . . . 16 deg coeff $/\$ deg coeff deg coeff deg coeff
97	94, 95, 96	mp2an 672	. . . . . . . . . . . . . . 15 deg coeff
98		unfi 7680	. . . . . . . . . . . . . . 15 deg $/\$ deg coeff deg deg coeff
99	91, 97, 98	mp2an 672	. . . . . . . . . . . . . 14 deg deg coeff
100	99	a1i 11	. . . . . . . . . . . . 13 Poly $\$ $/\$ deg deg coeff
101		ne0i 3741	. . . . . . . . . . . . . . 15 deg deg deg coeff deg deg coeff
102	22, 101	ax-mp 5	. . . . . . . . . . . . . 14 deg deg coeff
103	102	a1i 11	. . . . . . . . . . . . 13 Poly $\$ $/\$ deg deg coeff
104		xrltso 11219	. . . . . . . . . . . . . 14
105		fisupcl 7818	. . . . . . . . . . . . . 14 $/\$ deg deg coeff $/\$ deg deg coeff $/\$ deg deg coeff deg deg coeff deg deg coeff
106	104, 105	mpan 670	. . . . . . . . . . . . 13 deg deg coeff $/\$ deg deg coeff $/\$ deg deg coeff deg deg coeff deg deg coeff
107	100, 103, 18, 106	syl3anc 1219	. . . . . . . . . . . 12 Poly $\$ $/\$ deg deg coeff deg deg coeff
108	14, 107	sseldd 3455	. . . . . . . . . . 11 Poly $\$ $/\$ deg deg coeff
109	108	3adant2 1007	. . . . . . . . . 10 Poly $\$ $/\$ $/\$ deg deg coeff
110		eqidd 2452	. . . . . . . . . 10 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
111		breq2 4394	. . . . . . . . . . . . . . . 16 deg deg coeff deg deg deg deg coeff
112		breq2 4394	. . . . . . . . . . . . . . . . 17 deg deg coeff coeff coeff deg deg coeff
113	112	ralbidv 2839	. . . . . . . . . . . . . . . 16 deg deg coeff coeff coeff deg deg coeff
114	111, 113	3anbi23d 1293	. . . . . . . . . . . . . . 15 deg deg coeff $/\$ deg $/\$ coeff $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
115	114	rabbidv 3060	. . . . . . . . . . . . . 14 deg deg coeff Poly $/\$ deg $/\$ coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
116	115	rexeqdv 3020	. . . . . . . . . . . . 13 deg deg coeff Poly $/\$ deg $/\$ coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
117	116	rabbidv 3060	. . . . . . . . . . . 12 deg deg coeff Poly $/\$ deg $/\$ coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
118	117	eqeq2d 2465	. . . . . . . . . . 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 3169	. . . . . . . . . 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 661	. . . . . . . . 9 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg $/\$ coeff
121		cnex 9464	. . . . . . . . . . 11
122	121	rabex 4541	. . . . . . . . . 10 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
123		eleq2 2524	. . . . . . . . . . 11 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
124		eqeq1 2455	. . . . . . . . . . . 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 2844	. . . . . . . . . . 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 710	. . . . . . . . . 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 3160	. . . . . . . . 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 661	. . . . . . . 8 Poly $\$ $/\$ $/\$ $/\$ Poly $/\$ deg $/\$ coeff
129	128	3exp 1187	. . . . . . 7 Poly $\$ $/\$ Poly $/\$ deg $/\$ coeff
130	129	rexlimiv 2931	. . . . . 6 Poly $\$ $/\$ Poly $/\$ deg $/\$ coeff
131	130	impcom 430	. . . . 5 $/\$ Poly $\$ $/\$ Poly $/\$ deg $/\$ coeff
132		eleq2 2524	. . . . . . . . 9 Poly $/\$ deg $/\$ coeff Poly $/\$ deg $/\$ coeff
133	87	rexbidv 2844	. . . . . . . . . . 11 Poly $/\$ deg $/\$ coeff Poly $/\$ deg $/\$ coeff
134	133	elrab 3214	. . . . . . . . . 10 Poly $/\$ deg $/\$ coeff $/\$ Poly $/\$ deg $/\$ coeff
135		simp1 988	. . . . . . . . . . . . . . 15 $/\$ deg $/\$ coeff
136	135	anim2i 569	. . . . . . . . . . . . . 14 Poly $/\$ $/\$ deg $/\$ coeff Poly $/\$
137	71	breq1d 4400	. . . . . . . . . . . . . . . 16 deg deg
138	75	breq1d 4400	. . . . . . . . . . . . . . . . 17 coeff coeff
139	138	ralbidv 2839	. . . . . . . . . . . . . . . 16 coeff coeff
140	70, 137, 139	3anbi123d 1290	. . . . . . . . . . . . . . 15 $/\$ deg $/\$ coeff $/\$ deg $/\$ coeff
141	140	elrab 3214	. . . . . . . . . . . . . 14 Poly $/\$ deg $/\$ coeff Poly $/\$ $/\$ deg $/\$ coeff
142		eldifsn 4098	. . . . . . . . . . . . . 14 Poly $\$ Poly $/\$
143	136, 141, 142	3imtr4i 266	. . . . . . . . . . . . 13 Poly $/\$ deg $/\$ coeff Poly $\$
144	143	ssriv 3458	. . . . . . . . . . . 12 Poly $/\$ deg $/\$ coeff Poly $\$
145		ssrexv 3515	. . . . . . . . . . . . 13 Poly $/\$ deg $/\$ coeff Poly $\$ Poly $/\$ deg $/\$ coeff Poly $\$
146	83	cbvrexv 3044	. . . . . . . . . . . . 13 Poly $\$ Poly $\$
147	145, 146	syl6ib 226	. . . . . . . . . . . 12 Poly $/\$ deg $/\$ coeff Poly $\$ Poly $/\$ deg $/\$ coeff Poly $\$
148	144, 147	ax-mp 5	. . . . . . . . . . 11 Poly $/\$ deg $/\$ coeff Poly $\$
149	148	anim2i 569	. . . . . . . . . 10 $/\$ Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
150	134, 149	sylbi 195	. . . . . . . . 9 Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
151	132, 150	syl6bi 228	. . . . . . . 8 Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
152	151	rexlimivw 2933	. . . . . . 7 Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
153	152	impcom 430	. . . . . 6 $/\$ Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
154	153	exlimiv 1689	. . . . 5 $/\$ Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
155	131, 154	impbii 188	. . . 4 $/\$ Poly $\$ $/\$ Poly $/\$ deg $/\$ coeff
156		elaa 21898	. . . 4 $/\$ Poly $\$
157		eluniab 4200	. . . 4 Poly $/\$ deg $/\$ coeff $/\$ Poly $/\$ deg $/\$ coeff
158	155, 156, 157	3bitr4i 277	. . 3 Poly $/\$ deg $/\$ coeff
159	158	eqriv 2447	. 2 Poly $/\$ deg $/\$ coeff
160		aannenlem.a	. . . 4 Poly $/\$ deg $/\$ coeff
161	160	rnmpt 5183	. . 3 Poly $/\$ deg $/\$ coeff
162	161	unieqi 4198	. 2 Poly $/\$ deg $/\$ coeff
163	159, 162	eqtr4i 2483	1

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 369 $/\$ w3a 965

wceq 1370

wex 1587

wcel 1758

cab 2436

wne 2644

wral 2795

wrex 2796

crab 2799 $\$ cdif 3423

cun 3424

wss 3426

c0 3735

csn 3975

cpr 3977

cuni 4189 class class class wbr 4390

cmpt 4448

wor 4738

crn 4939

wf 5512

cfv 5516 (class class class)co 6190

cfn 7410

csup 7791

cc 9381

cr 9382

cc0 9383

cxr 9518

clt 9519

cle 9520

cn0 10680

cz 10747

cfz 11538

cabs 12825

c0p 21263 Polycply 21768 coeffccoe 21770 degcdgr 21771

caa 21896

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-rep 4501 ax-sep 4511 ax-nul 4519 ax-pow 4568 ax-pr 4629 ax-un 6472 ax-inf2 7948 ax-cnex 9439 ax-resscn 9440 ax-1cn 9441 ax-icn 9442 ax-addcl 9443 ax-addrcl 9444 ax-mulcl 9445 ax-mulrcl 9446 ax-mulcom 9447 ax-addass 9448 ax-mulass 9449 ax-distr 9450 ax-i2m1 9451 ax-1ne0 9452 ax-1rid 9453 ax-rnegex 9454 ax-rrecex 9455 ax-cnre 9456 ax-pre-lttri 9457 ax-pre-lttrn 9458 ax-pre-ltadd 9459 ax-pre-mulgt0 9460 ax-pre-sup 9461 ax-addf 9462

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-fal 1376 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-nel 2647 df-ral 2800 df-rex 2801 df-reu 2802 df-rmo 2803 df-rab 2804 df-v 3070 df-sbc 3285 df-csb 3387 df-dif 3429 df-un 3431 df-in 3433 df-ss 3440 df-pss 3442 df-nul 3736 df-if 3890 df-pw 3960 df-sn 3976 df-pr 3978 df-tp 3980 df-op 3982 df-uni 4190 df-int 4227 df-iun 4271 df-br 4391 df-opab 4449 df-mpt 4450 df-tr 4484 df-eprel 4730 df-id 4734 df-po 4739 df-so 4740 df-fr 4777 df-se 4778 df-we 4779 df-ord 4820 df-on 4821 df-lim 4822 df-suc 4823 df-xp 4944 df-rel 4945 df-cnv 4946 df-co 4947 df-dm 4948 df-rn 4949 df-res 4950 df-ima 4951 df-iota 5479 df-fun 5518 df-fn 5519 df-f 5520 df-f1 5521 df-fo 5522 df-f1o 5523 df-fv 5524 df-isom 5525 df-riota 6151 df-ov 6193 df-oprab 6194 df-mpt2 6195 df-of 6420 df-om 6577 df-1st 6677 df-2nd 6678 df-recs 6932 df-rdg 6966 df-1o 7020 df-oadd 7024 df-er 7201 df-map 7316 df-pm 7317 df-en 7411 df-dom 7412 df-sdom 7413 df-fin 7414 df-sup 7792 df-oi 7825 df-card 8210 df-pnf 9521 df-mnf 9522 df-xr 9523 df-ltxr 9524 df-le 9525 df-sub 9698 df-neg 9699 df-div 10095 df-nn 10424 df-2 10481 df-3 10482 df-n0 10681 df-z 10748 df-uz 10963 df-rp 11093 df-fz 11539 df-fzo 11650 df-fl 11743 df-seq 11908 df-exp 11967 df-hash 12205 df-cj 12690 df-re 12691 df-im 12692 df-sqr 12826 df-abs 12827 df-clim 13068 df-rlim 13069 df-sum 13266 df-0p 21264 df-ply 21772 df-coe 21774 df-dgr 21775 df-aa 21897

This theorem is referenced by: aannenlem3 21912

W3C validator