aannenlem2 - Metamath Proof Explorer

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

Theorem aannenlem2 21775

Description: Lemma for aannen 21777. (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 3473	. . . . . . . . . . . . . 14 Poly $\$ Poly
3	2	adantr 465	. . . . . . . . . . . . 13 Poly $\$ $/\$ Poly
4	3	3adant2 1007	. . . . . . . . . . . 12 Poly $\$ $/\$ $/\$ Poly
5		eldifsni 3996	. . . . . . . . . . . . . . 15 Poly $\$
6	5	adantr 465	. . . . . . . . . . . . . 14 Poly $\$ $/\$
7		0nn0 10586	. . . . . . . . . . . . . . . . . 18
8		dgrcl 21681	. . . . . . . . . . . . . . . . . . 19 Poly deg
9	3, 8	syl 16	. . . . . . . . . . . . . . . . . 18 Poly $\$ $/\$ deg
10		prssi 4024	. . . . . . . . . . . . . . . . . 18 $/\$ deg deg
11	7, 9, 10	sylancr 663	. . . . . . . . . . . . . . . . 17 Poly $\$ $/\$ deg
12		ssrab2 3432	. . . . . . . . . . . . . . . . . 18 deg coeff
13	12	a1i 11	. . . . . . . . . . . . . . . . 17 Poly $\$ $/\$ deg coeff
14	11, 13	unssd 3527	. . . . . . . . . . . . . . . 16 Poly $\$ $/\$ deg deg coeff
15		nn0ssre 10575	. . . . . . . . . . . . . . . . 17
16		ressxr 9419	. . . . . . . . . . . . . . . . 17
17	15, 16	sstri 3360	. . . . . . . . . . . . . . . 16
18	14, 17	syl6ss 3363	. . . . . . . . . . . . . . 15 Poly $\$ $/\$ deg deg coeff
19		fvex 5696	. . . . . . . . . . . . . . . . 17 deg
20	19	prid2 3979	. . . . . . . . . . . . . . . 16 deg deg
21		elun1 3518	. . . . . . . . . . . . . . . 16 deg deg deg deg deg coeff
22	20, 21	ax-mp 5	. . . . . . . . . . . . . . 15 deg deg deg coeff
23		supxrub 11279	. . . . . . . . . . . . . . 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 5686	. . . . . . . . . . . . . . . . . . . 20 coeff coeff
27		abs0 12766	. . . . . . . . . . . . . . . . . . . 20
28	26, 27	syl6eq 2486	. . . . . . . . . . . . . . . . . . 19 coeff coeff
29		c0ex 9372	. . . . . . . . . . . . . . . . . . . . 21
30	29	prid1 3978	. . . . . . . . . . . . . . . . . . . 20 deg
31		elun1 3518	. . . . . . . . . . . . . . . . . . . 20 deg deg deg coeff
32	30, 31	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 deg deg coeff
33	28, 32	syl6eqel 2526	. . . . . . . . . . . . . . . . . 18 coeff coeff deg deg coeff
34	33	adantl 466	. . . . . . . . . . . . . . . . 17 Poly $\$ $/\$ $/\$ $/\$ coeff coeff deg deg coeff
35		0z 10649	. . . . . . . . . . . . . . . . . . . . . . 23
36		eqid 2438	. . . . . . . . . . . . . . . . . . . . . . . 24 coeff coeff
37	36	coef2 21679	. . . . . . . . . . . . . . . . . . . . . . 23 Poly $/\$ coeff
38	3, 35, 37	sylancl 662	. . . . . . . . . . . . . . . . . . . . . 22 Poly $\$ $/\$ coeff
39	38	ffvelrnda 5838	. . . . . . . . . . . . . . . . . . . . 21 Poly $\$ $/\$ $/\$ coeff
40		nn0abscl 12793	. . . . . . . . . . . . . . . . . . . . 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 2438	. . . . . . . . . . . . . . . . . . . . . . 23 deg deg
48	36, 47	dgrub 21682	. . . . . . . . . . . . . . . . . . . . . 22 Poly $/\$ $/\$ coeff deg
49	45, 43, 46, 48	syl3anc 1218	. . . . . . . . . . . . . . . . . . . . 21 Poly $\$ $/\$ $/\$ $/\$ coeff deg
50		elfz2nn0 11472	. . . . . . . . . . . . . . . . . . . . 21 deg $/\$ deg $/\$ deg
51	43, 44, 49, 50	syl3anbrc 1172	. . . . . . . . . . . . . . . . . . . 20 Poly $\$ $/\$ $/\$ $/\$ coeff deg
52		eqid 2438	. . . . . . . . . . . . . . . . . . . 20 coeff coeff
53		fveq2 5686	. . . . . . . . . . . . . . . . . . . . . . 23 coeff coeff
54	53	fveq2d 5690	. . . . . . . . . . . . . . . . . . . . . 22 coeff coeff
55	54	eqeq2d 2449	. . . . . . . . . . . . . . . . . . . . 21 coeff coeff coeff coeff
56	55	rspcev 3068	. . . . . . . . . . . . . . . . . . . 20 deg $/\$ coeff coeff degcoeff coeff
57	51, 52, 56	sylancl 662	. . . . . . . . . . . . . . . . . . 19 Poly $\$ $/\$ $/\$ $/\$ coeff degcoeff coeff
58		eqeq1 2444	. . . . . . . . . . . . . . . . . . . . 21 coeff coeff coeff coeff
59	58	rexbidv 2731	. . . . . . . . . . . . . . . . . . . 20 coeff deg coeff degcoeff coeff
60	59	elrab 3112	. . . . . . . . . . . . . . . . . . 19 coeff deg coeff coeff $/\$ degcoeff coeff
61	42, 57, 60	sylanbrc 664	. . . . . . . . . . . . . . . . . 18 Poly $\$ $/\$ $/\$ $/\$ coeff coeff deg coeff
62		elun2 3519	. . . . . . . . . . . . . . . . . 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 2684	. . . . . . . . . . . . . . . 16 Poly $\$ $/\$ $/\$ coeff deg deg coeff
65		supxrub 11279	. . . . . . . . . . . . . . . 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 2794	. . . . . . . . . . . . . 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 2611	. . . . . . . . . . . . . 14
71		fveq2 5686	. . . . . . . . . . . . . . 15 deg deg
72	71	breq1d 4297	. . . . . . . . . . . . . 14 deg deg deg coeff deg deg deg coeff
73		fveq2 5686	. . . . . . . . . . . . . . . . . 18 coeff coeff
74	73	fveq1d 5688	. . . . . . . . . . . . . . . . 17 coeff coeff
75	74	fveq2d 5690	. . . . . . . . . . . . . . . 16 coeff coeff
76	75	breq1d 4297	. . . . . . . . . . . . . . 15 coeff deg deg coeff coeff deg deg coeff
77	76	ralbidv 2730	. . . . . . . . . . . . . 14 coeff deg deg coeff coeff deg deg coeff
78	70, 72, 77	3anbi123d 1289	. . . . . . . . . . . . 13 $/\$ deg deg deg coeff $/\$ coeff deg deg coeff $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
79	78	elrab 3112	. . . . . . . . . . . 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 5685	. . . . . . . . . . . . 13
83	82	eqeq1d 2446	. . . . . . . . . . . 12
84	83	rspcev 3068	. . . . . . . . . . 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 5686	. . . . . . . . . . . . 13
87	86	eqeq1d 2446	. . . . . . . . . . . 12
88	87	rexbidv 2731	. . . . . . . . . . 11 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
89	88	elrab 3112	. . . . . . . . . 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 7578	. . . . . . . . . . . . . . 15 deg
92		fzfi 11786	. . . . . . . . . . . . . . . . 17 deg
93		abrexfi 7603	. . . . . . . . . . . . . . . . 17 deg deg coeff
94	92, 93	ax-mp 5	. . . . . . . . . . . . . . . 16 deg coeff
95		rabssab 3434	. . . . . . . . . . . . . . . 16 deg coeff deg coeff
96		ssfi 7525	. . . . . . . . . . . . . . . 16 deg coeff $/\$ deg coeff deg coeff deg coeff
97	94, 95, 96	mp2an 672	. . . . . . . . . . . . . . 15 deg coeff
98		unfi 7571	. . . . . . . . . . . . . . 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 3638	. . . . . . . . . . . . . . 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 11110	. . . . . . . . . . . . . 14
105		fisupcl 7709	. . . . . . . . . . . . . 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 1218	. . . . . . . . . . . 12 Poly $\$ $/\$ deg deg coeff deg deg coeff
108	14, 107	sseldd 3352	. . . . . . . . . . 11 Poly $\$ $/\$ deg deg coeff
109	108	3adant2 1007	. . . . . . . . . 10 Poly $\$ $/\$ $/\$ deg deg coeff
110		eqidd 2439	. . . . . . . . . 10 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
111		breq2 4291	. . . . . . . . . . . . . . . 16 deg deg coeff deg deg deg deg coeff
112		breq2 4291	. . . . . . . . . . . . . . . . 17 deg deg coeff coeff coeff deg deg coeff
113	112	ralbidv 2730	. . . . . . . . . . . . . . . 16 deg deg coeff coeff coeff deg deg coeff
114	111, 113	3anbi23d 1292	. . . . . . . . . . . . . . 15 deg deg coeff $/\$ deg $/\$ coeff $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
115	114	rabbidv 2959	. . . . . . . . . . . . . 14 deg deg coeff Poly $/\$ deg $/\$ coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
116	115	rexeqdv 2919	. . . . . . . . . . . . 13 deg deg coeff Poly $/\$ deg $/\$ coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
117	116	rabbidv 2959	. . . . . . . . . . . 12 deg deg coeff Poly $/\$ deg $/\$ coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
118	117	eqeq2d 2449	. . . . . . . . . . 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 3068	. . . . . . . . . 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 9355	. . . . . . . . . . 11
122	121	rabex 4438	. . . . . . . . . 10 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
123		eleq2 2499	. . . . . . . . . . 11 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
124		eqeq1 2444	. . . . . . . . . . . 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 2731	. . . . . . . . . . 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 3059	. . . . . . . . 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 1186	. . . . . . 7 Poly $\$ $/\$ Poly $/\$ deg $/\$ coeff
130	129	rexlimiv 2830	. . . . . 6 Poly $\$ $/\$ Poly $/\$ deg $/\$ coeff
131	130	impcom 430	. . . . 5 $/\$ Poly $\$ $/\$ Poly $/\$ deg $/\$ coeff
132		eleq2 2499	. . . . . . . . 9 Poly $/\$ deg $/\$ coeff Poly $/\$ deg $/\$ coeff
133	87	rexbidv 2731	. . . . . . . . . . 11 Poly $/\$ deg $/\$ coeff Poly $/\$ deg $/\$ coeff
134	133	elrab 3112	. . . . . . . . . 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 4297	. . . . . . . . . . . . . . . 16 deg deg
138	75	breq1d 4297	. . . . . . . . . . . . . . . . 17 coeff coeff
139	138	ralbidv 2730	. . . . . . . . . . . . . . . 16 coeff coeff
140	70, 137, 139	3anbi123d 1289	. . . . . . . . . . . . . . 15 $/\$ deg $/\$ coeff $/\$ deg $/\$ coeff
141	140	elrab 3112	. . . . . . . . . . . . . 14 Poly $/\$ deg $/\$ coeff Poly $/\$ $/\$ deg $/\$ coeff
142		eldifsn 3995	. . . . . . . . . . . . . 14 Poly $\$ Poly $/\$
143	136, 141, 142	3imtr4i 266	. . . . . . . . . . . . 13 Poly $/\$ deg $/\$ coeff Poly $\$
144	143	ssriv 3355	. . . . . . . . . . . 12 Poly $/\$ deg $/\$ coeff Poly $\$
145		ssrexv 3412	. . . . . . . . . . . . 13 Poly $/\$ deg $/\$ coeff Poly $\$ Poly $/\$ deg $/\$ coeff Poly $\$
146	83	cbvrexv 2943	. . . . . . . . . . . . 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 2832	. . . . . . 7 Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
153	152	impcom 430	. . . . . 6 $/\$ Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
154	153	exlimiv 1688	. . . . 5 $/\$ Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
155	131, 154	impbii 188	. . . 4 $/\$ Poly $\$ $/\$ Poly $/\$ deg $/\$ coeff
156		elaa 21762	. . . 4 $/\$ Poly $\$
157		eluniab 4097	. . . 4 Poly $/\$ deg $/\$ coeff $/\$ Poly $/\$ deg $/\$ coeff
158	155, 156, 157	3bitr4i 277	. . 3 Poly $/\$ deg $/\$ coeff
159	158	eqriv 2435	. 2 Poly $/\$ deg $/\$ coeff
160		aannenlem.a	. . . 4 Poly $/\$ deg $/\$ coeff
161	160	rnmpt 5080	. . 3 Poly $/\$ deg $/\$ coeff
162	161	unieqi 4095	. 2 Poly $/\$ deg $/\$ coeff
163	159, 162	eqtr4i 2461	1

Colors of variables: wff setvar class

Syntax hints:

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

wceq 1369

wex 1586

wcel 1756

cab 2424

wne 2601

wral 2710

wrex 2711

crab 2714 $\$ cdif 3320

cun 3321

wss 3323

c0 3632

csn 3872

cpr 3874

cuni 4086 class class class wbr 4287

cmpt 4345

wor 4635

crn 4836

wf 5409

cfv 5413 (class class class)co 6086

cfn 7302

csup 7682

cc 9272

cr 9273

cc0 9274

cxr 9409

clt 9410

cle 9411

cn0 10571

cz 10638

cfz 11429

cabs 12715

c0p 21127 Polycply 21632 coeffccoe 21634 degcdgr 21635

caa 21760

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-rep 4398 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367 ax-inf2 7839 ax-cnex 9330 ax-resscn 9331 ax-1cn 9332 ax-icn 9333 ax-addcl 9334 ax-addrcl 9335 ax-mulcl 9336 ax-mulrcl 9337 ax-mulcom 9338 ax-addass 9339 ax-mulass 9340 ax-distr 9341 ax-i2m1 9342 ax-1ne0 9343 ax-1rid 9344 ax-rnegex 9345 ax-rrecex 9346 ax-cnre 9347 ax-pre-lttri 9348 ax-pre-lttrn 9349 ax-pre-ltadd 9350 ax-pre-mulgt0 9351 ax-pre-sup 9352 ax-addf 9353

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-fal 1375 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2715 df-rex 2716 df-reu 2717 df-rmo 2718 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-pss 3339 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-tp 3877 df-op 3879 df-uni 4087 df-int 4124 df-iun 4168 df-br 4288 df-opab 4346 df-mpt 4347 df-tr 4381 df-eprel 4627 df-id 4631 df-po 4636 df-so 4637 df-fr 4674 df-se 4675 df-we 4676 df-ord 4717 df-on 4718 df-lim 4719 df-suc 4720 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 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-riota 6047 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-of 6315 df-om 6472 df-1st 6572 df-2nd 6573 df-recs 6824 df-rdg 6858 df-1o 6912 df-oadd 6916 df-er 7093 df-map 7208 df-pm 7209 df-en 7303 df-dom 7304 df-sdom 7305 df-fin 7306 df-sup 7683 df-oi 7716 df-card 8101 df-pnf 9412 df-mnf 9413 df-xr 9414 df-ltxr 9415 df-le 9416 df-sub 9589 df-neg 9590 df-div 9986 df-nn 10315 df-2 10372 df-3 10373 df-n0 10572 df-z 10639 df-uz 10854 df-rp 10984 df-fz 11430 df-fzo 11541 df-fl 11634 df-seq 11799 df-exp 11858 df-hash 12096 df-cj 12580 df-re 12581 df-im 12582 df-sqr 12716 df-abs 12717 df-clim 12958 df-rlim 12959 df-sum 13156 df-0p 21128 df-ply 21636 df-coe 21638 df-dgr 21639 df-aa 21761

This theorem is referenced by: aannenlem3 21776

W3C validator