aannenlem2 - Metamath Proof Explorer

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

Theorem aannenlem2 21680

Description: Lemma for aannen 21682. (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 983	. . . . . . . . . 10 Poly $\$ $/\$ $/\$
2		eldifi 3466	. . . . . . . . . . . . . 14 Poly $\$ Poly
3	2	adantr 462	. . . . . . . . . . . . 13 Poly $\$ $/\$ Poly
4	3	3adant2 1000	. . . . . . . . . . . 12 Poly $\$ $/\$ $/\$ Poly
5		eldifsni 3989	. . . . . . . . . . . . . . 15 Poly $\$
6	5	adantr 462	. . . . . . . . . . . . . 14 Poly $\$ $/\$
7		0nn0 10582	. . . . . . . . . . . . . . . . . 18
8		dgrcl 21586	. . . . . . . . . . . . . . . . . . 19 Poly deg
9	3, 8	syl 16	. . . . . . . . . . . . . . . . . 18 Poly $\$ $/\$ deg
10		prssi 4017	. . . . . . . . . . . . . . . . . 18 $/\$ deg deg
11	7, 9, 10	sylancr 656	. . . . . . . . . . . . . . . . 17 Poly $\$ $/\$ deg
12		ssrab2 3425	. . . . . . . . . . . . . . . . . 18 deg coeff
13	12	a1i 11	. . . . . . . . . . . . . . . . 17 Poly $\$ $/\$ deg coeff
14	11, 13	unssd 3520	. . . . . . . . . . . . . . . 16 Poly $\$ $/\$ deg deg coeff
15		nn0ssre 10571	. . . . . . . . . . . . . . . . 17
16		ressxr 9415	. . . . . . . . . . . . . . . . 17
17	15, 16	sstri 3353	. . . . . . . . . . . . . . . 16
18	14, 17	syl6ss 3356	. . . . . . . . . . . . . . 15 Poly $\$ $/\$ deg deg coeff
19		fvex 5689	. . . . . . . . . . . . . . . . 17 deg
20	19	prid2 3972	. . . . . . . . . . . . . . . 16 deg deg
21		elun1 3511	. . . . . . . . . . . . . . . 16 deg deg deg deg deg coeff
22	20, 21	ax-mp 5	. . . . . . . . . . . . . . 15 deg deg deg coeff
23		supxrub 11275	. . . . . . . . . . . . . . 15 deg deg coeff $/\$ deg deg deg coeff deg deg deg coeff
24	18, 22, 23	sylancl 655	. . . . . . . . . . . . . 14 Poly $\$ $/\$ deg deg deg coeff
25	18	adantr 462	. . . . . . . . . . . . . . . 16 Poly $\$ $/\$ $/\$ deg deg coeff
26		fveq2 5679	. . . . . . . . . . . . . . . . . . . 20 coeff coeff
27		abs0 12758	. . . . . . . . . . . . . . . . . . . 20
28	26, 27	syl6eq 2481	. . . . . . . . . . . . . . . . . . 19 coeff coeff
29		c0ex 9368	. . . . . . . . . . . . . . . . . . . . 21
30	29	prid1 3971	. . . . . . . . . . . . . . . . . . . 20 deg
31		elun1 3511	. . . . . . . . . . . . . . . . . . . 20 deg deg deg coeff
32	30, 31	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 deg deg coeff
33	28, 32	syl6eqel 2521	. . . . . . . . . . . . . . . . . 18 coeff coeff deg deg coeff
34	33	adantl 463	. . . . . . . . . . . . . . . . 17 Poly $\$ $/\$ $/\$ $/\$ coeff coeff deg deg coeff
35		0z 10645	. . . . . . . . . . . . . . . . . . . . . . 23
36		eqid 2433	. . . . . . . . . . . . . . . . . . . . . . . 24 coeff coeff
37	36	coef2 21584	. . . . . . . . . . . . . . . . . . . . . . 23 Poly $/\$ coeff
38	3, 35, 37	sylancl 655	. . . . . . . . . . . . . . . . . . . . . 22 Poly $\$ $/\$ coeff
39	38	ffvelrnda 5831	. . . . . . . . . . . . . . . . . . . . 21 Poly $\$ $/\$ $/\$ coeff
40		nn0abscl 12785	. . . . . . . . . . . . . . . . . . . . 21 coeff coeff
41	39, 40	syl 16	. . . . . . . . . . . . . . . . . . . 20 Poly $\$ $/\$ $/\$ coeff
42	41	adantr 462	. . . . . . . . . . . . . . . . . . 19 Poly $\$ $/\$ $/\$ $/\$ coeff coeff
43		simplr 747	. . . . . . . . . . . . . . . . . . . . 21 Poly $\$ $/\$ $/\$ $/\$ coeff
44	9	ad2antrr 718	. . . . . . . . . . . . . . . . . . . . 21 Poly $\$ $/\$ $/\$ $/\$ coeff deg
45	3	ad2antrr 718	. . . . . . . . . . . . . . . . . . . . . 22 Poly $\$ $/\$ $/\$ $/\$ coeff Poly
46		simpr 458	. . . . . . . . . . . . . . . . . . . . . 22 Poly $\$ $/\$ $/\$ $/\$ coeff coeff
47		eqid 2433	. . . . . . . . . . . . . . . . . . . . . . 23 deg deg
48	36, 47	dgrub 21587	. . . . . . . . . . . . . . . . . . . . . 22 Poly $/\$ $/\$ coeff deg
49	45, 43, 46, 48	syl3anc 1211	. . . . . . . . . . . . . . . . . . . . 21 Poly $\$ $/\$ $/\$ $/\$ coeff deg
50		elfz2nn0 11467	. . . . . . . . . . . . . . . . . . . . 21 deg $/\$ deg $/\$ deg
51	43, 44, 49, 50	syl3anbrc 1165	. . . . . . . . . . . . . . . . . . . 20 Poly $\$ $/\$ $/\$ $/\$ coeff deg
52		eqid 2433	. . . . . . . . . . . . . . . . . . . 20 coeff coeff
53		fveq2 5679	. . . . . . . . . . . . . . . . . . . . . . 23 coeff coeff
54	53	fveq2d 5683	. . . . . . . . . . . . . . . . . . . . . 22 coeff coeff
55	54	eqeq2d 2444	. . . . . . . . . . . . . . . . . . . . 21 coeff coeff coeff coeff
56	55	rspcev 3062	. . . . . . . . . . . . . . . . . . . 20 deg $/\$ coeff coeff degcoeff coeff
57	51, 52, 56	sylancl 655	. . . . . . . . . . . . . . . . . . 19 Poly $\$ $/\$ $/\$ $/\$ coeff degcoeff coeff
58		eqeq1 2439	. . . . . . . . . . . . . . . . . . . . 21 coeff coeff coeff coeff
59	58	rexbidv 2726	. . . . . . . . . . . . . . . . . . . 20 coeff deg coeff degcoeff coeff
60	59	elrab 3106	. . . . . . . . . . . . . . . . . . 19 coeff deg coeff coeff $/\$ degcoeff coeff
61	42, 57, 60	sylanbrc 657	. . . . . . . . . . . . . . . . . 18 Poly $\$ $/\$ $/\$ $/\$ coeff coeff deg coeff
62		elun2 3512	. . . . . . . . . . . . . . . . . 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 2679	. . . . . . . . . . . . . . . 16 Poly $\$ $/\$ $/\$ coeff deg deg coeff
65		supxrub 11275	. . . . . . . . . . . . . . . 16 deg deg coeff $/\$ coeff deg deg coeff coeff deg deg coeff
66	25, 64, 65	syl2anc 654	. . . . . . . . . . . . . . 15 Poly $\$ $/\$ $/\$ coeff deg deg coeff
67	66	ralrimiva 2789	. . . . . . . . . . . . . 14 Poly $\$ $/\$ coeff deg deg coeff
68	6, 24, 67	3jca 1161	. . . . . . . . . . . . 13 Poly $\$ $/\$ $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
69	68	3adant2 1000	. . . . . . . . . . . 12 Poly $\$ $/\$ $/\$ $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
70		neeq1 2606	. . . . . . . . . . . . . 14
71		fveq2 5679	. . . . . . . . . . . . . . 15 deg deg
72	71	breq1d 4290	. . . . . . . . . . . . . 14 deg deg deg coeff deg deg deg coeff
73		fveq2 5679	. . . . . . . . . . . . . . . . . 18 coeff coeff
74	73	fveq1d 5681	. . . . . . . . . . . . . . . . 17 coeff coeff
75	74	fveq2d 5683	. . . . . . . . . . . . . . . 16 coeff coeff
76	75	breq1d 4290	. . . . . . . . . . . . . . 15 coeff deg deg coeff coeff deg deg coeff
77	76	ralbidv 2725	. . . . . . . . . . . . . 14 coeff deg deg coeff coeff deg deg coeff
78	70, 72, 77	3anbi123d 1282	. . . . . . . . . . . . 13 $/\$ deg deg deg coeff $/\$ coeff deg deg coeff $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
79	78	elrab 3106	. . . . . . . . . . . 12 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
80	4, 69, 79	sylanbrc 657	. . . . . . . . . . 11 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
81		simp2 982	. . . . . . . . . . 11 Poly $\$ $/\$ $/\$
82		fveq1 5678	. . . . . . . . . . . . 13
83	82	eqeq1d 2441	. . . . . . . . . . . 12
84	83	rspcev 3062	. . . . . . . . . . 11 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
85	80, 81, 84	syl2anc 654	. . . . . . . . . 10 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
86		fveq2 5679	. . . . . . . . . . . . 13
87	86	eqeq1d 2441	. . . . . . . . . . . 12
88	87	rexbidv 2726	. . . . . . . . . . 11 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
89	88	elrab 3106	. . . . . . . . . 10 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
90	1, 85, 89	sylanbrc 657	. . . . . . . . 9 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
91		prfi 7574	. . . . . . . . . . . . . . 15 deg
92		fzfi 11778	. . . . . . . . . . . . . . . . 17 deg
93		abrexfi 7599	. . . . . . . . . . . . . . . . 17 deg deg coeff
94	92, 93	ax-mp 5	. . . . . . . . . . . . . . . 16 deg coeff
95		rabssab 3427	. . . . . . . . . . . . . . . 16 deg coeff deg coeff
96		ssfi 7521	. . . . . . . . . . . . . . . 16 deg coeff $/\$ deg coeff deg coeff deg coeff
97	94, 95, 96	mp2an 665	. . . . . . . . . . . . . . 15 deg coeff
98		unfi 7567	. . . . . . . . . . . . . . 15 deg $/\$ deg coeff deg deg coeff
99	91, 97, 98	mp2an 665	. . . . . . . . . . . . . 14 deg deg coeff
100	99	a1i 11	. . . . . . . . . . . . 13 Poly $\$ $/\$ deg deg coeff
101		ne0i 3631	. . . . . . . . . . . . . . 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 11106	. . . . . . . . . . . . . 14
105		fisupcl 7705	. . . . . . . . . . . . . 14 $/\$ deg deg coeff $/\$ deg deg coeff $/\$ deg deg coeff deg deg coeff deg deg coeff
106	104, 105	mpan 663	. . . . . . . . . . . . 13 deg deg coeff $/\$ deg deg coeff $/\$ deg deg coeff deg deg coeff deg deg coeff
107	100, 103, 18, 106	syl3anc 1211	. . . . . . . . . . . 12 Poly $\$ $/\$ deg deg coeff deg deg coeff
108	14, 107	sseldd 3345	. . . . . . . . . . 11 Poly $\$ $/\$ deg deg coeff
109	108	3adant2 1000	. . . . . . . . . 10 Poly $\$ $/\$ $/\$ deg deg coeff
110		eqidd 2434	. . . . . . . . . 10 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
111		breq2 4284	. . . . . . . . . . . . . . . 16 deg deg coeff deg deg deg deg coeff
112		breq2 4284	. . . . . . . . . . . . . . . . 17 deg deg coeff coeff coeff deg deg coeff
113	112	ralbidv 2725	. . . . . . . . . . . . . . . 16 deg deg coeff coeff coeff deg deg coeff
114	111, 113	3anbi23d 1285	. . . . . . . . . . . . . . 15 deg deg coeff $/\$ deg $/\$ coeff $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
115	114	rabbidv 2954	. . . . . . . . . . . . . 14 deg deg coeff Poly $/\$ deg $/\$ coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
116	115	rexeqdv 2914	. . . . . . . . . . . . 13 deg deg coeff Poly $/\$ deg $/\$ coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
117	116	rabbidv 2954	. . . . . . . . . . . 12 deg deg coeff Poly $/\$ deg $/\$ coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
118	117	eqeq2d 2444	. . . . . . . . . . 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 3062	. . . . . . . . . 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 654	. . . . . . . . 9 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg $/\$ coeff
121		cnex 9351	. . . . . . . . . . 11
122	121	rabex 4431	. . . . . . . . . 10 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
123		eleq2 2494	. . . . . . . . . . 11 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
124		eqeq1 2439	. . . . . . . . . . . 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 2726	. . . . . . . . . . 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 703	. . . . . . . . . 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 3053	. . . . . . . . 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 654	. . . . . . . 8 Poly $\$ $/\$ $/\$ $/\$ Poly $/\$ deg $/\$ coeff
129	128	3exp 1179	. . . . . . 7 Poly $\$ $/\$ Poly $/\$ deg $/\$ coeff
130	129	rexlimiv 2825	. . . . . 6 Poly $\$ $/\$ Poly $/\$ deg $/\$ coeff
131	130	impcom 430	. . . . 5 $/\$ Poly $\$ $/\$ Poly $/\$ deg $/\$ coeff
132		eleq2 2494	. . . . . . . . 9 Poly $/\$ deg $/\$ coeff Poly $/\$ deg $/\$ coeff
133	87	rexbidv 2726	. . . . . . . . . . 11 Poly $/\$ deg $/\$ coeff Poly $/\$ deg $/\$ coeff
134	133	elrab 3106	. . . . . . . . . 10 Poly $/\$ deg $/\$ coeff $/\$ Poly $/\$ deg $/\$ coeff
135		simp1 981	. . . . . . . . . . . . . . 15 $/\$ deg $/\$ coeff
136	135	anim2i 564	. . . . . . . . . . . . . 14 Poly $/\$ $/\$ deg $/\$ coeff Poly $/\$
137	71	breq1d 4290	. . . . . . . . . . . . . . . 16 deg deg
138	75	breq1d 4290	. . . . . . . . . . . . . . . . 17 coeff coeff
139	138	ralbidv 2725	. . . . . . . . . . . . . . . 16 coeff coeff
140	70, 137, 139	3anbi123d 1282	. . . . . . . . . . . . . . 15 $/\$ deg $/\$ coeff $/\$ deg $/\$ coeff
141	140	elrab 3106	. . . . . . . . . . . . . 14 Poly $/\$ deg $/\$ coeff Poly $/\$ $/\$ deg $/\$ coeff
142		eldifsn 3988	. . . . . . . . . . . . . 14 Poly $\$ Poly $/\$
143	136, 141, 142	3imtr4i 266	. . . . . . . . . . . . 13 Poly $/\$ deg $/\$ coeff Poly $\$
144	143	ssriv 3348	. . . . . . . . . . . 12 Poly $/\$ deg $/\$ coeff Poly $\$
145		ssrexv 3405	. . . . . . . . . . . . 13 Poly $/\$ deg $/\$ coeff Poly $\$ Poly $/\$ deg $/\$ coeff Poly $\$
146	83	cbvrexv 2938	. . . . . . . . . . . . 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 564	. . . . . . . . . 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 2827	. . . . . . 7 Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
153	152	impcom 430	. . . . . 6 $/\$ Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
154	153	exlimiv 1687	. . . . 5 $/\$ Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
155	131, 154	impbii 188	. . . 4 $/\$ Poly $\$ $/\$ Poly $/\$ deg $/\$ coeff
156		elaa 21667	. . . 4 $/\$ Poly $\$
157		eluniab 4090	. . . 4 Poly $/\$ deg $/\$ coeff $/\$ Poly $/\$ deg $/\$ coeff
158	155, 156, 157	3bitr4i 277	. . 3 Poly $/\$ deg $/\$ coeff
159	158	eqriv 2430	. 2 Poly $/\$ deg $/\$ coeff
160		aannenlem.a	. . . 4 Poly $/\$ deg $/\$ coeff
161	160	rnmpt 5072	. . 3 Poly $/\$ deg $/\$ coeff
162	161	unieqi 4088	. 2 Poly $/\$ deg $/\$ coeff
163	159, 162	eqtr4i 2456	1

Colors of variables: wff setvar class

Syntax hints:

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

wceq 1362

wex 1589

wcel 1755

cab 2419

wne 2596

wral 2705

wrex 2706

crab 2709 $\$ cdif 3313

cun 3314

wss 3316

c0 3625

csn 3865

cpr 3867

cuni 4079 class class class wbr 4280

cmpt 4338

wor 4627

crn 4828

wf 5402

cfv 5406 (class class class)co 6080

cfn 7298

csup 7678

cc 9268

cr 9269

cc0 9270

cxr 9405

clt 9406

cle 9407

cn0 10567

cz 10634

cfz 11424

cabs 12707

c0p 20989 Polycply 21537 coeffccoe 21539 degcdgr 21540

caa 21665

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1594 ax-4 1605 ax-5 1669 ax-6 1707 ax-7 1727 ax-8 1757 ax-9 1759 ax-10 1774 ax-11 1779 ax-12 1791 ax-13 1942 ax-ext 2414 ax-rep 4391 ax-sep 4401 ax-nul 4409 ax-pow 4458 ax-pr 4519 ax-un 6361 ax-inf2 7835 ax-cnex 9326 ax-resscn 9327 ax-1cn 9328 ax-icn 9329 ax-addcl 9330 ax-addrcl 9331 ax-mulcl 9332 ax-mulrcl 9333 ax-mulcom 9334 ax-addass 9335 ax-mulass 9336 ax-distr 9337 ax-i2m1 9338 ax-1ne0 9339 ax-1rid 9340 ax-rnegex 9341 ax-rrecex 9342 ax-cnre 9343 ax-pre-lttri 9344 ax-pre-lttrn 9345 ax-pre-ltadd 9346 ax-pre-mulgt0 9347 ax-pre-sup 9348 ax-addf 9349

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 959 df-3an 960 df-tru 1365 df-fal 1368 df-ex 1590 df-nf 1593 df-sb 1700 df-eu 2258 df-mo 2259 df-clab 2420 df-cleq 2426 df-clel 2429 df-nfc 2558 df-ne 2598 df-nel 2599 df-ral 2710 df-rex 2711 df-reu 2712 df-rmo 2713 df-rab 2714 df-v 2964 df-sbc 3176 df-csb 3277 df-dif 3319 df-un 3321 df-in 3323 df-ss 3330 df-pss 3332 df-nul 3626 df-if 3780 df-pw 3850 df-sn 3866 df-pr 3868 df-tp 3870 df-op 3872 df-uni 4080 df-int 4117 df-iun 4161 df-br 4281 df-opab 4339 df-mpt 4340 df-tr 4374 df-eprel 4619 df-id 4623 df-po 4628 df-so 4629 df-fr 4666 df-se 4667 df-we 4668 df-ord 4709 df-on 4710 df-lim 4711 df-suc 4712 df-xp 4833 df-rel 4834 df-cnv 4835 df-co 4836 df-dm 4837 df-rn 4838 df-res 4839 df-ima 4840 df-iota 5369 df-fun 5408 df-fn 5409 df-f 5410 df-f1 5411 df-fo 5412 df-f1o 5413 df-fv 5414 df-isom 5415 df-riota 6039 df-ov 6083 df-oprab 6084 df-mpt2 6085 df-of 6309 df-om 6466 df-1st 6566 df-2nd 6567 df-recs 6818 df-rdg 6852 df-1o 6908 df-oadd 6912 df-er 7089 df-map 7204 df-pm 7205 df-en 7299 df-dom 7300 df-sdom 7301 df-fin 7302 df-sup 7679 df-oi 7712 df-card 8097 df-pnf 9408 df-mnf 9409 df-xr 9410 df-ltxr 9411 df-le 9412 df-sub 9585 df-neg 9586 df-div 9982 df-nn 10311 df-2 10368 df-3 10369 df-n0 10568 df-z 10635 df-uz 10850 df-rp 10980 df-fz 11425 df-fzo 11533 df-fl 11626 df-seq 11791 df-exp 11850 df-hash 12088 df-cj 12572 df-re 12573 df-im 12574 df-sqr 12708 df-abs 12709 df-clim 12950 df-rlim 12951 df-sum 13148 df-0p 20990 df-ply 21541 df-coe 21543 df-dgr 21544 df-aa 21666

This theorem is referenced by: aannenlem3 21681

W3C validator