aannenlem2 - Metamath Proof Explorer

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

Theorem aannenlem2 23283

Description: Lemma for aannen 23285. (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 1007	. . . . . . . . . 10 Poly $\$ $/\$ $/\$
2		eldifi 3587	. . . . . . . . . . . . . 14 Poly $\$ Poly
3	2	adantr 466	. . . . . . . . . . . . 13 Poly $\$ $/\$ Poly
4	3	3adant2 1024	. . . . . . . . . . . 12 Poly $\$ $/\$ $/\$ Poly
5		eldifsni 4126	. . . . . . . . . . . . . . 15 Poly $\$
6	5	adantr 466	. . . . . . . . . . . . . 14 Poly $\$ $/\$
7		0nn0 10891	. . . . . . . . . . . . . . . . . 18
8		dgrcl 23185	. . . . . . . . . . . . . . . . . . 19 Poly deg
9	3, 8	syl 17	. . . . . . . . . . . . . . . . . 18 Poly $\$ $/\$ deg
10		prssi 4156	. . . . . . . . . . . . . . . . . 18 $/\$ deg deg
11	7, 9, 10	sylancr 667	. . . . . . . . . . . . . . . . 17 Poly $\$ $/\$ deg
12		ssrab2 3546	. . . . . . . . . . . . . . . . . 18 deg coeff
13	12	a1i 11	. . . . . . . . . . . . . . . . 17 Poly $\$ $/\$ deg coeff
14	11, 13	unssd 3642	. . . . . . . . . . . . . . . 16 Poly $\$ $/\$ deg deg coeff
15		nn0ssre 10880	. . . . . . . . . . . . . . . . 17
16		ressxr 9691	. . . . . . . . . . . . . . . . 17
17	15, 16	sstri 3473	. . . . . . . . . . . . . . . 16
18	14, 17	syl6ss 3476	. . . . . . . . . . . . . . 15 Poly $\$ $/\$ deg deg coeff
19		fvex 5891	. . . . . . . . . . . . . . . . 17 deg
20	19	prid2 4109	. . . . . . . . . . . . . . . 16 deg deg
21		elun1 3633	. . . . . . . . . . . . . . . 16 deg deg deg deg deg coeff
22	20, 21	ax-mp 5	. . . . . . . . . . . . . . 15 deg deg deg coeff
23		supxrub 11617	. . . . . . . . . . . . . . 15 deg deg coeff $/\$ deg deg deg coeff deg deg deg coeff
24	18, 22, 23	sylancl 666	. . . . . . . . . . . . . 14 Poly $\$ $/\$ deg deg deg coeff
25	18	adantr 466	. . . . . . . . . . . . . . . 16 Poly $\$ $/\$ $/\$ deg deg coeff
26		fveq2 5881	. . . . . . . . . . . . . . . . . . . 20 coeff coeff
27		abs0 13348	. . . . . . . . . . . . . . . . . . . 20
28	26, 27	syl6eq 2479	. . . . . . . . . . . . . . . . . . 19 coeff coeff
29		c0ex 9644	. . . . . . . . . . . . . . . . . . . . 21
30	29	prid1 4108	. . . . . . . . . . . . . . . . . . . 20 deg
31		elun1 3633	. . . . . . . . . . . . . . . . . . . 20 deg deg deg coeff
32	30, 31	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 deg deg coeff
33	28, 32	syl6eqel 2515	. . . . . . . . . . . . . . . . . 18 coeff coeff deg deg coeff
34	33	adantl 467	. . . . . . . . . . . . . . . . 17 Poly $\$ $/\$ $/\$ $/\$ coeff coeff deg deg coeff
35		0z 10955	. . . . . . . . . . . . . . . . . . . . . . 23
36		eqid 2422	. . . . . . . . . . . . . . . . . . . . . . . 24 coeff coeff
37	36	coef2 23183	. . . . . . . . . . . . . . . . . . . . . . 23 Poly $/\$ coeff
38	3, 35, 37	sylancl 666	. . . . . . . . . . . . . . . . . . . . . 22 Poly $\$ $/\$ coeff
39	38	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . . . 21 Poly $\$ $/\$ $/\$ coeff
40		nn0abscl 13375	. . . . . . . . . . . . . . . . . . . . 21 coeff coeff
41	39, 40	syl 17	. . . . . . . . . . . . . . . . . . . 20 Poly $\$ $/\$ $/\$ coeff
42	41	adantr 466	. . . . . . . . . . . . . . . . . . 19 Poly $\$ $/\$ $/\$ $/\$ coeff coeff
43		simplr 760	. . . . . . . . . . . . . . . . . . . . 21 Poly $\$ $/\$ $/\$ $/\$ coeff
44	9	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . 21 Poly $\$ $/\$ $/\$ $/\$ coeff deg
45	3	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . . 22 Poly $\$ $/\$ $/\$ $/\$ coeff Poly
46		simpr 462	. . . . . . . . . . . . . . . . . . . . . 22 Poly $\$ $/\$ $/\$ $/\$ coeff coeff
47		eqid 2422	. . . . . . . . . . . . . . . . . . . . . . 23 deg deg
48	36, 47	dgrub 23186	. . . . . . . . . . . . . . . . . . . . . 22 Poly $/\$ $/\$ coeff deg
49	45, 43, 46, 48	syl3anc 1264	. . . . . . . . . . . . . . . . . . . . 21 Poly $\$ $/\$ $/\$ $/\$ coeff deg
50		elfz2nn0 11892	. . . . . . . . . . . . . . . . . . . . 21 deg $/\$ deg $/\$ deg
51	43, 44, 49, 50	syl3anbrc 1189	. . . . . . . . . . . . . . . . . . . 20 Poly $\$ $/\$ $/\$ $/\$ coeff deg
52		eqid 2422	. . . . . . . . . . . . . . . . . . . 20 coeff coeff
53		fveq2 5881	. . . . . . . . . . . . . . . . . . . . . . 23 coeff coeff
54	53	fveq2d 5885	. . . . . . . . . . . . . . . . . . . . . 22 coeff coeff
55	54	eqeq2d 2436	. . . . . . . . . . . . . . . . . . . . 21 coeff coeff coeff coeff
56	55	rspcev 3182	. . . . . . . . . . . . . . . . . . . 20 deg $/\$ coeff coeff degcoeff coeff
57	51, 52, 56	sylancl 666	. . . . . . . . . . . . . . . . . . 19 Poly $\$ $/\$ $/\$ $/\$ coeff degcoeff coeff
58		eqeq1 2426	. . . . . . . . . . . . . . . . . . . . 21 coeff coeff coeff coeff
59	58	rexbidv 2936	. . . . . . . . . . . . . . . . . . . 20 coeff deg coeff degcoeff coeff
60	59	elrab 3228	. . . . . . . . . . . . . . . . . . 19 coeff deg coeff coeff $/\$ degcoeff coeff
61	42, 57, 60	sylanbrc 668	. . . . . . . . . . . . . . . . . 18 Poly $\$ $/\$ $/\$ $/\$ coeff coeff deg coeff
62		elun2 3634	. . . . . . . . . . . . . . . . . 18 coeff deg coeff coeff deg deg coeff
63	61, 62	syl 17	. . . . . . . . . . . . . . . . 17 Poly $\$ $/\$ $/\$ $/\$ coeff coeff deg deg coeff
64	34, 63	pm2.61dane 2738	. . . . . . . . . . . . . . . 16 Poly $\$ $/\$ $/\$ coeff deg deg coeff
65		supxrub 11617	. . . . . . . . . . . . . . . 16 deg deg coeff $/\$ coeff deg deg coeff coeff deg deg coeff
66	25, 64, 65	syl2anc 665	. . . . . . . . . . . . . . 15 Poly $\$ $/\$ $/\$ coeff deg deg coeff
67	66	ralrimiva 2836	. . . . . . . . . . . . . 14 Poly $\$ $/\$ coeff deg deg coeff
68	6, 24, 67	3jca 1185	. . . . . . . . . . . . 13 Poly $\$ $/\$ $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
69	68	3adant2 1024	. . . . . . . . . . . 12 Poly $\$ $/\$ $/\$ $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
70		neeq1 2701	. . . . . . . . . . . . . 14
71		fveq2 5881	. . . . . . . . . . . . . . 15 deg deg
72	71	breq1d 4433	. . . . . . . . . . . . . 14 deg deg deg coeff deg deg deg coeff
73		fveq2 5881	. . . . . . . . . . . . . . . . . 18 coeff coeff
74	73	fveq1d 5883	. . . . . . . . . . . . . . . . 17 coeff coeff
75	74	fveq2d 5885	. . . . . . . . . . . . . . . 16 coeff coeff
76	75	breq1d 4433	. . . . . . . . . . . . . . 15 coeff deg deg coeff coeff deg deg coeff
77	76	ralbidv 2861	. . . . . . . . . . . . . 14 coeff deg deg coeff coeff deg deg coeff
78	70, 72, 77	3anbi123d 1335	. . . . . . . . . . . . 13 $/\$ deg deg deg coeff $/\$ coeff deg deg coeff $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
79	78	elrab 3228	. . . . . . . . . . . 12 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
80	4, 69, 79	sylanbrc 668	. . . . . . . . . . 11 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
81		simp2 1006	. . . . . . . . . . 11 Poly $\$ $/\$ $/\$
82		fveq1 5880	. . . . . . . . . . . . 13
83	82	eqeq1d 2424	. . . . . . . . . . . 12
84	83	rspcev 3182	. . . . . . . . . . 11 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
85	80, 81, 84	syl2anc 665	. . . . . . . . . 10 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
86		fveq2 5881	. . . . . . . . . . . . 13
87	86	eqeq1d 2424	. . . . . . . . . . . 12
88	87	rexbidv 2936	. . . . . . . . . . 11 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
89	88	elrab 3228	. . . . . . . . . 10 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
90	1, 85, 89	sylanbrc 668	. . . . . . . . 9 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
91		prfi 7855	. . . . . . . . . . . . . . 15 deg
92		fzfi 12191	. . . . . . . . . . . . . . . . 17 deg
93		abrexfi 7883	. . . . . . . . . . . . . . . . 17 deg deg coeff
94	92, 93	ax-mp 5	. . . . . . . . . . . . . . . 16 deg coeff
95		rabssab 3548	. . . . . . . . . . . . . . . 16 deg coeff deg coeff
96		ssfi 7801	. . . . . . . . . . . . . . . 16 deg coeff $/\$ deg coeff deg coeff deg coeff
97	94, 95, 96	mp2an 676	. . . . . . . . . . . . . . 15 deg coeff
98		unfi 7847	. . . . . . . . . . . . . . 15 deg $/\$ deg coeff deg deg coeff
99	91, 97, 98	mp2an 676	. . . . . . . . . . . . . 14 deg deg coeff
100	99	a1i 11	. . . . . . . . . . . . 13 Poly $\$ $/\$ deg deg coeff
101	22	ne0ii 3768	. . . . . . . . . . . . . 14 deg deg coeff
102	101	a1i 11	. . . . . . . . . . . . 13 Poly $\$ $/\$ deg deg coeff
103		xrltso 11447	. . . . . . . . . . . . . 14
104		fisupcl 7994	. . . . . . . . . . . . . 14 $/\$ deg deg coeff $/\$ deg deg coeff $/\$ deg deg coeff deg deg coeff deg deg coeff
105	103, 104	mpan 674	. . . . . . . . . . . . 13 deg deg coeff $/\$ deg deg coeff $/\$ deg deg coeff deg deg coeff deg deg coeff
106	100, 102, 18, 105	syl3anc 1264	. . . . . . . . . . . 12 Poly $\$ $/\$ deg deg coeff deg deg coeff
107	14, 106	sseldd 3465	. . . . . . . . . . 11 Poly $\$ $/\$ deg deg coeff
108	107	3adant2 1024	. . . . . . . . . 10 Poly $\$ $/\$ $/\$ deg deg coeff
109		eqidd 2423	. . . . . . . . . 10 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
110		breq2 4427	. . . . . . . . . . . . . . . 16 deg deg coeff deg deg deg deg coeff
111		breq2 4427	. . . . . . . . . . . . . . . . 17 deg deg coeff coeff coeff deg deg coeff
112	111	ralbidv 2861	. . . . . . . . . . . . . . . 16 deg deg coeff coeff coeff deg deg coeff
113	110, 112	3anbi23d 1338	. . . . . . . . . . . . . . 15 deg deg coeff $/\$ deg $/\$ coeff $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
114	113	rabbidv 3071	. . . . . . . . . . . . . 14 deg deg coeff Poly $/\$ deg $/\$ coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
115	114	rexeqdv 3029	. . . . . . . . . . . . 13 deg deg coeff Poly $/\$ deg $/\$ coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
116	115	rabbidv 3071	. . . . . . . . . . . 12 deg deg coeff Poly $/\$ deg $/\$ coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
117	116	eqeq2d 2436	. . . . . . . . . . 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
118	117	rspcev 3182	. . . . . . . . . 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
119	108, 109, 118	syl2anc 665	. . . . . . . . 9 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg $/\$ coeff
120		cnex 9627	. . . . . . . . . . 11
121	120	rabex 4575	. . . . . . . . . 10 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
122		eleq2 2496	. . . . . . . . . . 11 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
123		eqeq1 2426	. . . . . . . . . . . 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
124	123	rexbidv 2936	. . . . . . . . . . 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
125	122, 124	anbi12d 715	. . . . . . . . . 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
126	121, 125	spcev 3173	. . . . . . . . 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
127	90, 119, 126	syl2anc 665	. . . . . . . 8 Poly $\$ $/\$ $/\$ $/\$ Poly $/\$ deg $/\$ coeff
128	127	3exp 1204	. . . . . . 7 Poly $\$ $/\$ Poly $/\$ deg $/\$ coeff
129	128	rexlimiv 2908	. . . . . 6 Poly $\$ $/\$ Poly $/\$ deg $/\$ coeff
130	129	impcom 431	. . . . 5 $/\$ Poly $\$ $/\$ Poly $/\$ deg $/\$ coeff
131		eleq2 2496	. . . . . . . . 9 Poly $/\$ deg $/\$ coeff Poly $/\$ deg $/\$ coeff
132	87	rexbidv 2936	. . . . . . . . . . 11 Poly $/\$ deg $/\$ coeff Poly $/\$ deg $/\$ coeff
133	132	elrab 3228	. . . . . . . . . 10 Poly $/\$ deg $/\$ coeff $/\$ Poly $/\$ deg $/\$ coeff
134		simp1 1005	. . . . . . . . . . . . . . 15 $/\$ deg $/\$ coeff
135	134	anim2i 571	. . . . . . . . . . . . . 14 Poly $/\$ $/\$ deg $/\$ coeff Poly $/\$
136	71	breq1d 4433	. . . . . . . . . . . . . . . 16 deg deg
137	75	breq1d 4433	. . . . . . . . . . . . . . . . 17 coeff coeff
138	137	ralbidv 2861	. . . . . . . . . . . . . . . 16 coeff coeff
139	70, 136, 138	3anbi123d 1335	. . . . . . . . . . . . . . 15 $/\$ deg $/\$ coeff $/\$ deg $/\$ coeff
140	139	elrab 3228	. . . . . . . . . . . . . 14 Poly $/\$ deg $/\$ coeff Poly $/\$ $/\$ deg $/\$ coeff
141		eldifsn 4125	. . . . . . . . . . . . . 14 Poly $\$ Poly $/\$
142	135, 140, 141	3imtr4i 269	. . . . . . . . . . . . 13 Poly $/\$ deg $/\$ coeff Poly $\$
143	142	ssriv 3468	. . . . . . . . . . . 12 Poly $/\$ deg $/\$ coeff Poly $\$
144		ssrexv 3526	. . . . . . . . . . . . 13 Poly $/\$ deg $/\$ coeff Poly $\$ Poly $/\$ deg $/\$ coeff Poly $\$
145	83	cbvrexv 3055	. . . . . . . . . . . . 13 Poly $\$ Poly $\$
146	144, 145	syl6ib 229	. . . . . . . . . . . 12 Poly $/\$ deg $/\$ coeff Poly $\$ Poly $/\$ deg $/\$ coeff Poly $\$
147	143, 146	ax-mp 5	. . . . . . . . . . 11 Poly $/\$ deg $/\$ coeff Poly $\$
148	147	anim2i 571	. . . . . . . . . 10 $/\$ Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
149	133, 148	sylbi 198	. . . . . . . . 9 Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
150	131, 149	syl6bi 231	. . . . . . . 8 Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
151	150	rexlimivw 2911	. . . . . . 7 Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
152	151	impcom 431	. . . . . 6 $/\$ Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
153	152	exlimiv 1770	. . . . 5 $/\$ Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
154	130, 153	impbii 190	. . . 4 $/\$ Poly $\$ $/\$ Poly $/\$ deg $/\$ coeff
155		elaa 23267	. . . 4 $/\$ Poly $\$
156		eluniab 4230	. . . 4 Poly $/\$ deg $/\$ coeff $/\$ Poly $/\$ deg $/\$ coeff
157	154, 155, 156	3bitr4i 280	. . 3 Poly $/\$ deg $/\$ coeff
158	157	eqriv 2418	. 2 Poly $/\$ deg $/\$ coeff
159		aannenlem.a	. . . 4 Poly $/\$ deg $/\$ coeff
160	159	rnmpt 5099	. . 3 Poly $/\$ deg $/\$ coeff
161	160	unieqi 4228	. 2 Poly $/\$ deg $/\$ coeff
162	158, 161	eqtr4i 2454	1

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wex 1657

wcel 1872

cab 2407

wne 2614

wral 2771

wrex 2772

crab 2775 $\$ cdif 3433

cun 3434

wss 3436

c0 3761

csn 3998

cpr 4000

cuni 4219 class class class wbr 4423

cmpt 4482

wor 4773

crn 4854

wf 5597

cfv 5601 (class class class)co 6305

cfn 7580

csup 7963

cc 9544

cr 9545

cc0 9546

cxr 9681

clt 9682

cle 9683

cn0 10876

cz 10944

cfz 11791

cabs 13297

c0p 22625 Polycply 23136 coeffccoe 23138 degcdgr 23139

caa 23265

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2057 ax-ext 2401 ax-rep 4536 ax-sep 4546 ax-nul 4555 ax-pow 4602 ax-pr 4660 ax-un 6597 ax-inf2 8155 ax-cnex 9602 ax-resscn 9603 ax-1cn 9604 ax-icn 9605 ax-addcl 9606 ax-addrcl 9607 ax-mulcl 9608 ax-mulrcl 9609 ax-mulcom 9610 ax-addass 9611 ax-mulass 9612 ax-distr 9613 ax-i2m1 9614 ax-1ne0 9615 ax-1rid 9616 ax-rnegex 9617 ax-rrecex 9618 ax-cnre 9619 ax-pre-lttri 9620 ax-pre-lttrn 9621 ax-pre-ltadd 9622 ax-pre-mulgt0 9623 ax-pre-sup 9624 ax-addf 9625

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1658 df-nf 1662 df-sb 1791 df-eu 2273 df-mo 2274 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2568 df-ne 2616 df-nel 2617 df-ral 2776 df-rex 2777 df-reu 2778 df-rmo 2779 df-rab 2780 df-v 3082 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-pss 3452 df-nul 3762 df-if 3912 df-pw 3983 df-sn 3999 df-pr 4001 df-tp 4003 df-op 4005 df-uni 4220 df-int 4256 df-iun 4301 df-br 4424 df-opab 4483 df-mpt 4484 df-tr 4519 df-eprel 4764 df-id 4768 df-po 4774 df-so 4775 df-fr 4812 df-se 4813 df-we 4814 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-pred 5399 df-ord 5445 df-on 5446 df-lim 5447 df-suc 5448 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-isom 5610 df-riota 6267 df-ov 6308 df-oprab 6309 df-mpt2 6310 df-of 6545 df-om 6707 df-1st 6807 df-2nd 6808 df-wrecs 7039 df-recs 7101 df-rdg 7139 df-1o 7193 df-oadd 7197 df-er 7374 df-map 7485 df-pm 7486 df-en 7581 df-dom 7582 df-sdom 7583 df-fin 7584 df-sup 7965 df-inf 7966 df-oi 8034 df-card 8381 df-pnf 9684 df-mnf 9685 df-xr 9686 df-ltxr 9687 df-le 9688 df-sub 9869 df-neg 9870 df-div 10277 df-nn 10617 df-2 10675 df-3 10676 df-n0 10877 df-z 10945 df-uz 11167 df-rp 11310 df-fz 11792 df-fzo 11923 df-fl 12034 df-seq 12220 df-exp 12279 df-hash 12522 df-cj 13162 df-re 13163 df-im 13164 df-sqrt 13298 df-abs 13299 df-clim 13551 df-rlim 13552 df-sum 13752 df-0p 22626 df-ply 23140 df-coe 23142 df-dgr 23143 df-aa 23266

This theorem is referenced by: aannenlem3 23284

W3C validator