aannenlem2 - Metamath Proof Explorer

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

Theorem aannenlem2 23297

Description: Lemma for aannen 23299. (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 1011	. . . . . . . . . 10 Poly $\$ $/\$ $/\$
2		eldifi 3523	. . . . . . . . . . . . . 14 Poly $\$ Poly
3	2	adantr 471	. . . . . . . . . . . . 13 Poly $\$ $/\$ Poly
4	3	3adant2 1028	. . . . . . . . . . . 12 Poly $\$ $/\$ $/\$ Poly
5		eldifsni 4067	. . . . . . . . . . . . . . 15 Poly $\$
6	5	adantr 471	. . . . . . . . . . . . . 14 Poly $\$ $/\$
7		0nn0 10874	. . . . . . . . . . . . . . . . . 18
8		dgrcl 23199	. . . . . . . . . . . . . . . . . . 19 Poly deg
9	3, 8	syl 17	. . . . . . . . . . . . . . . . . 18 Poly $\$ $/\$ deg
10		prssi 4097	. . . . . . . . . . . . . . . . . 18 $/\$ deg deg
11	7, 9, 10	sylancr 674	. . . . . . . . . . . . . . . . 17 Poly $\$ $/\$ deg
12		ssrab2 3482	. . . . . . . . . . . . . . . . . 18 deg coeff
13	12	a1i 11	. . . . . . . . . . . . . . . . 17 Poly $\$ $/\$ deg coeff
14	11, 13	unssd 3578	. . . . . . . . . . . . . . . 16 Poly $\$ $/\$ deg deg coeff
15		nn0ssre 10863	. . . . . . . . . . . . . . . . 17
16		ressxr 9671	. . . . . . . . . . . . . . . . 17
17	15, 16	sstri 3409	. . . . . . . . . . . . . . . 16
18	14, 17	syl6ss 3412	. . . . . . . . . . . . . . 15 Poly $\$ $/\$ deg deg coeff
19		fvex 5858	. . . . . . . . . . . . . . . . 17 deg
20	19	prid2 4050	. . . . . . . . . . . . . . . 16 deg deg
21		elun1 3569	. . . . . . . . . . . . . . . 16 deg deg deg deg deg coeff
22	20, 21	ax-mp 5	. . . . . . . . . . . . . . 15 deg deg deg coeff
23		supxrub 11600	. . . . . . . . . . . . . . 15 deg deg coeff $/\$ deg deg deg coeff deg deg deg coeff
24	18, 22, 23	sylancl 673	. . . . . . . . . . . . . 14 Poly $\$ $/\$ deg deg deg coeff
25	18	adantr 471	. . . . . . . . . . . . . . . 16 Poly $\$ $/\$ $/\$ deg deg coeff
26		fveq2 5848	. . . . . . . . . . . . . . . . . . . 20 coeff coeff
27		abs0 13359	. . . . . . . . . . . . . . . . . . . 20
28	26, 27	syl6eq 2502	. . . . . . . . . . . . . . . . . . 19 coeff coeff
29		c0ex 9624	. . . . . . . . . . . . . . . . . . . . 21
30	29	prid1 4049	. . . . . . . . . . . . . . . . . . . 20 deg
31		elun1 3569	. . . . . . . . . . . . . . . . . . . 20 deg deg deg coeff
32	30, 31	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 deg deg coeff
33	28, 32	syl6eqel 2538	. . . . . . . . . . . . . . . . . 18 coeff coeff deg deg coeff
34	33	adantl 472	. . . . . . . . . . . . . . . . 17 Poly $\$ $/\$ $/\$ $/\$ coeff coeff deg deg coeff
35		0z 10938	. . . . . . . . . . . . . . . . . . . . . . 23
36		eqid 2452	. . . . . . . . . . . . . . . . . . . . . . . 24 coeff coeff
37	36	coef2 23197	. . . . . . . . . . . . . . . . . . . . . . 23 Poly $/\$ coeff
38	3, 35, 37	sylancl 673	. . . . . . . . . . . . . . . . . . . . . 22 Poly $\$ $/\$ coeff
39	38	ffvelrnda 6006	. . . . . . . . . . . . . . . . . . . . 21 Poly $\$ $/\$ $/\$ coeff
40		nn0abscl 13386	. . . . . . . . . . . . . . . . . . . . 21 coeff coeff
41	39, 40	syl 17	. . . . . . . . . . . . . . . . . . . 20 Poly $\$ $/\$ $/\$ coeff
42	41	adantr 471	. . . . . . . . . . . . . . . . . . 19 Poly $\$ $/\$ $/\$ $/\$ coeff coeff
43		simplr 767	. . . . . . . . . . . . . . . . . . . . 21 Poly $\$ $/\$ $/\$ $/\$ coeff
44	9	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . 21 Poly $\$ $/\$ $/\$ $/\$ coeff deg
45	3	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . . 22 Poly $\$ $/\$ $/\$ $/\$ coeff Poly
46		simpr 467	. . . . . . . . . . . . . . . . . . . . . 22 Poly $\$ $/\$ $/\$ $/\$ coeff coeff
47		eqid 2452	. . . . . . . . . . . . . . . . . . . . . . 23 deg deg
48	36, 47	dgrub 23200	. . . . . . . . . . . . . . . . . . . . . 22 Poly $/\$ $/\$ coeff deg
49	45, 43, 46, 48	syl3anc 1271	. . . . . . . . . . . . . . . . . . . . 21 Poly $\$ $/\$ $/\$ $/\$ coeff deg
50		elfz2nn0 11876	. . . . . . . . . . . . . . . . . . . . 21 deg $/\$ deg $/\$ deg
51	43, 44, 49, 50	syl3anbrc 1193	. . . . . . . . . . . . . . . . . . . 20 Poly $\$ $/\$ $/\$ $/\$ coeff deg
52		eqid 2452	. . . . . . . . . . . . . . . . . . . 20 coeff coeff
53		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . 23 coeff coeff
54	53	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . 22 coeff coeff
55	54	eqeq2d 2462	. . . . . . . . . . . . . . . . . . . . 21 coeff coeff coeff coeff
56	55	rspcev 3118	. . . . . . . . . . . . . . . . . . . 20 deg $/\$ coeff coeff degcoeff coeff
57	51, 52, 56	sylancl 673	. . . . . . . . . . . . . . . . . . 19 Poly $\$ $/\$ $/\$ $/\$ coeff degcoeff coeff
58		eqeq1 2456	. . . . . . . . . . . . . . . . . . . . 21 coeff coeff coeff coeff
59	58	rexbidv 2873	. . . . . . . . . . . . . . . . . . . 20 coeff deg coeff degcoeff coeff
60	59	elrab 3164	. . . . . . . . . . . . . . . . . . 19 coeff deg coeff coeff $/\$ degcoeff coeff
61	42, 57, 60	sylanbrc 675	. . . . . . . . . . . . . . . . . 18 Poly $\$ $/\$ $/\$ $/\$ coeff coeff deg coeff
62		elun2 3570	. . . . . . . . . . . . . . . . . 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 2711	. . . . . . . . . . . . . . . 16 Poly $\$ $/\$ $/\$ coeff deg deg coeff
65		supxrub 11600	. . . . . . . . . . . . . . . 16 deg deg coeff $/\$ coeff deg deg coeff coeff deg deg coeff
66	25, 64, 65	syl2anc 671	. . . . . . . . . . . . . . 15 Poly $\$ $/\$ $/\$ coeff deg deg coeff
67	66	ralrimiva 2790	. . . . . . . . . . . . . 14 Poly $\$ $/\$ coeff deg deg coeff
68	6, 24, 67	3jca 1189	. . . . . . . . . . . . 13 Poly $\$ $/\$ $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
69	68	3adant2 1028	. . . . . . . . . . . 12 Poly $\$ $/\$ $/\$ $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
70		neeq1 2686	. . . . . . . . . . . . . 14
71		fveq2 5848	. . . . . . . . . . . . . . 15 deg deg
72	71	breq1d 4384	. . . . . . . . . . . . . 14 deg deg deg coeff deg deg deg coeff
73		fveq2 5848	. . . . . . . . . . . . . . . . . 18 coeff coeff
74	73	fveq1d 5850	. . . . . . . . . . . . . . . . 17 coeff coeff
75	74	fveq2d 5852	. . . . . . . . . . . . . . . 16 coeff coeff
76	75	breq1d 4384	. . . . . . . . . . . . . . 15 coeff deg deg coeff coeff deg deg coeff
77	76	ralbidv 2810	. . . . . . . . . . . . . 14 coeff deg deg coeff coeff deg deg coeff
78	70, 72, 77	3anbi123d 1343	. . . . . . . . . . . . 13 $/\$ deg deg deg coeff $/\$ coeff deg deg coeff $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
79	78	elrab 3164	. . . . . . . . . . . 12 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
80	4, 69, 79	sylanbrc 675	. . . . . . . . . . 11 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
81		simp2 1010	. . . . . . . . . . 11 Poly $\$ $/\$ $/\$
82		fveq1 5847	. . . . . . . . . . . . 13
83	82	eqeq1d 2454	. . . . . . . . . . . 12
84	83	rspcev 3118	. . . . . . . . . . 11 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
85	80, 81, 84	syl2anc 671	. . . . . . . . . 10 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
86		fveq2 5848	. . . . . . . . . . . . 13
87	86	eqeq1d 2454	. . . . . . . . . . . 12
88	87	rexbidv 2873	. . . . . . . . . . 11 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
89	88	elrab 3164	. . . . . . . . . 10 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
90	1, 85, 89	sylanbrc 675	. . . . . . . . 9 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
91		prfi 7833	. . . . . . . . . . . . . . 15 deg
92		fzfi 12179	. . . . . . . . . . . . . . . . 17 deg
93		abrexfi 7861	. . . . . . . . . . . . . . . . 17 deg deg coeff
94	92, 93	ax-mp 5	. . . . . . . . . . . . . . . 16 deg coeff
95		rabssab 3484	. . . . . . . . . . . . . . . 16 deg coeff deg coeff
96		ssfi 7779	. . . . . . . . . . . . . . . 16 deg coeff $/\$ deg coeff deg coeff deg coeff
97	94, 95, 96	mp2an 683	. . . . . . . . . . . . . . 15 deg coeff
98		unfi 7825	. . . . . . . . . . . . . . 15 deg $/\$ deg coeff deg deg coeff
99	91, 97, 98	mp2an 683	. . . . . . . . . . . . . 14 deg deg coeff
100	99	a1i 11	. . . . . . . . . . . . 13 Poly $\$ $/\$ deg deg coeff
101	22	ne0ii 3706	. . . . . . . . . . . . . 14 deg deg coeff
102	101	a1i 11	. . . . . . . . . . . . 13 Poly $\$ $/\$ deg deg coeff
103		xrltso 11430	. . . . . . . . . . . . . 14
104		fisupcl 7972	. . . . . . . . . . . . . 14 $/\$ deg deg coeff $/\$ deg deg coeff $/\$ deg deg coeff deg deg coeff deg deg coeff
105	103, 104	mpan 681	. . . . . . . . . . . . 13 deg deg coeff $/\$ deg deg coeff $/\$ deg deg coeff deg deg coeff deg deg coeff
106	100, 102, 18, 105	syl3anc 1271	. . . . . . . . . . . 12 Poly $\$ $/\$ deg deg coeff deg deg coeff
107	14, 106	sseldd 3401	. . . . . . . . . . 11 Poly $\$ $/\$ deg deg coeff
108	107	3adant2 1028	. . . . . . . . . 10 Poly $\$ $/\$ $/\$ deg deg coeff
109		eqidd 2453	. . . . . . . . . 10 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
110		breq2 4378	. . . . . . . . . . . . . . . 16 deg deg coeff deg deg deg deg coeff
111		breq2 4378	. . . . . . . . . . . . . . . . 17 deg deg coeff coeff coeff deg deg coeff
112	111	ralbidv 2810	. . . . . . . . . . . . . . . 16 deg deg coeff coeff coeff deg deg coeff
113	110, 112	3anbi23d 1346	. . . . . . . . . . . . . . 15 deg deg coeff $/\$ deg $/\$ coeff $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
114	113	rabbidv 3004	. . . . . . . . . . . . . 14 deg deg coeff Poly $/\$ deg $/\$ coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
115	114	rexeqdv 2962	. . . . . . . . . . . . 13 deg deg coeff Poly $/\$ deg $/\$ coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
116	115	rabbidv 3004	. . . . . . . . . . . 12 deg deg coeff Poly $/\$ deg $/\$ coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
117	116	eqeq2d 2462	. . . . . . . . . . 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 3118	. . . . . . . . . 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 671	. . . . . . . . 9 Poly $\$ $/\$ $/\$ Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg $/\$ coeff
120		cnex 9607	. . . . . . . . . . 11
121	120	rabex 4527	. . . . . . . . . 10 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
122		eleq2 2519	. . . . . . . . . . 11 Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff Poly $/\$ deg deg deg coeff $/\$ coeff deg deg coeff
123		eqeq1 2456	. . . . . . . . . . . 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 2873	. . . . . . . . . . 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 722	. . . . . . . . . 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 3109	. . . . . . . . 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 671	. . . . . . . 8 Poly $\$ $/\$ $/\$ $/\$ Poly $/\$ deg $/\$ coeff
128	127	3exp 1209	. . . . . . 7 Poly $\$ $/\$ Poly $/\$ deg $/\$ coeff
129	128	rexlimiv 2848	. . . . . 6 Poly $\$ $/\$ Poly $/\$ deg $/\$ coeff
130	129	impcom 436	. . . . 5 $/\$ Poly $\$ $/\$ Poly $/\$ deg $/\$ coeff
131		eleq2 2519	. . . . . . . . 9 Poly $/\$ deg $/\$ coeff Poly $/\$ deg $/\$ coeff
132	87	rexbidv 2873	. . . . . . . . . . 11 Poly $/\$ deg $/\$ coeff Poly $/\$ deg $/\$ coeff
133	132	elrab 3164	. . . . . . . . . 10 Poly $/\$ deg $/\$ coeff $/\$ Poly $/\$ deg $/\$ coeff
134		simp1 1009	. . . . . . . . . . . . . . 15 $/\$ deg $/\$ coeff
135	134	anim2i 577	. . . . . . . . . . . . . 14 Poly $/\$ $/\$ deg $/\$ coeff Poly $/\$
136	71	breq1d 4384	. . . . . . . . . . . . . . . 16 deg deg
137	75	breq1d 4384	. . . . . . . . . . . . . . . . 17 coeff coeff
138	137	ralbidv 2810	. . . . . . . . . . . . . . . 16 coeff coeff
139	70, 136, 138	3anbi123d 1343	. . . . . . . . . . . . . . 15 $/\$ deg $/\$ coeff $/\$ deg $/\$ coeff
140	139	elrab 3164	. . . . . . . . . . . . . 14 Poly $/\$ deg $/\$ coeff Poly $/\$ $/\$ deg $/\$ coeff
141		eldifsn 4066	. . . . . . . . . . . . . 14 Poly $\$ Poly $/\$
142	135, 140, 141	3imtr4i 274	. . . . . . . . . . . . 13 Poly $/\$ deg $/\$ coeff Poly $\$
143	142	ssriv 3404	. . . . . . . . . . . 12 Poly $/\$ deg $/\$ coeff Poly $\$
144		ssrexv 3462	. . . . . . . . . . . . 13 Poly $/\$ deg $/\$ coeff Poly $\$ Poly $/\$ deg $/\$ coeff Poly $\$
145	83	cbvrexv 2988	. . . . . . . . . . . . 13 Poly $\$ Poly $\$
146	144, 145	syl6ib 234	. . . . . . . . . . . 12 Poly $/\$ deg $/\$ coeff Poly $\$ Poly $/\$ deg $/\$ coeff Poly $\$
147	143, 146	ax-mp 5	. . . . . . . . . . 11 Poly $/\$ deg $/\$ coeff Poly $\$
148	147	anim2i 577	. . . . . . . . . 10 $/\$ Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
149	133, 148	sylbi 200	. . . . . . . . 9 Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
150	131, 149	syl6bi 236	. . . . . . . 8 Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
151	150	rexlimivw 2850	. . . . . . 7 Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
152	151	impcom 436	. . . . . 6 $/\$ Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
153	152	exlimiv 1780	. . . . 5 $/\$ Poly $/\$ deg $/\$ coeff $/\$ Poly $\$
154	130, 153	impbii 192	. . . 4 $/\$ Poly $\$ $/\$ Poly $/\$ deg $/\$ coeff
155		elaa 23281	. . . 4 $/\$ Poly $\$
156		eluniab 4179	. . . 4 Poly $/\$ deg $/\$ coeff $/\$ Poly $/\$ deg $/\$ coeff
157	154, 155, 156	3bitr4i 285	. . 3 Poly $/\$ deg $/\$ coeff
158	157	eqriv 2449	. 2 Poly $/\$ deg $/\$ coeff
159		aannenlem.a	. . . 4 Poly $/\$ deg $/\$ coeff
160	159	rnmpt 5058	. . 3 Poly $/\$ deg $/\$ coeff
161	160	unieqi 4177	. 2 Poly $/\$ deg $/\$ coeff
162	158, 161	eqtr4i 2477	1

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 375 $/\$ w3a 986

wceq 1448

wex 1667

wcel 1891

cab 2438

wne 2622

wral 2737

wrex 2738

crab 2741 $\$ cdif 3369

cun 3370

wss 3372

c0 3699

csn 3936

cpr 3938

cuni 4168 class class class wbr 4374

cmpt 4433

wor 4732

crn 4813

wf 5557

cfv 5561 (class class class)co 6276

cfn 7556

csup 7941

cc 9524

cr 9525

cc0 9526

cxr 9661

clt 9662

cle 9663

cn0 10859

cz 10927

cfz 11775

cabs 13308

c0p 22639 Polycply 23150 coeffccoe 23152 degcdgr 23153

caa 23279

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1673 ax-4 1686 ax-5 1762 ax-6 1809 ax-7 1855 ax-8 1893 ax-9 1900 ax-10 1919 ax-11 1924 ax-12 1937 ax-13 2092 ax-ext 2432 ax-rep 4487 ax-sep 4497 ax-nul 4506 ax-pow 4554 ax-pr 4612 ax-un 6571 ax-inf2 8133 ax-cnex 9582 ax-resscn 9583 ax-1cn 9584 ax-icn 9585 ax-addcl 9586 ax-addrcl 9587 ax-mulcl 9588 ax-mulrcl 9589 ax-mulcom 9590 ax-addass 9591 ax-mulass 9592 ax-distr 9593 ax-i2m1 9594 ax-1ne0 9595 ax-1rid 9596 ax-rnegex 9597 ax-rrecex 9598 ax-cnre 9599 ax-pre-lttri 9600 ax-pre-lttrn 9601 ax-pre-ltadd 9602 ax-pre-mulgt0 9603 ax-pre-sup 9604 ax-addf 9605

This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 987 df-3an 988 df-tru 1451 df-fal 1454 df-ex 1668 df-nf 1672 df-sb 1802 df-eu 2304 df-mo 2305 df-clab 2439 df-cleq 2445 df-clel 2448 df-nfc 2582 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3015 df-sbc 3236 df-csb 3332 df-dif 3375 df-un 3377 df-in 3379 df-ss 3386 df-pss 3388 df-nul 3700 df-if 3850 df-pw 3921 df-sn 3937 df-pr 3939 df-tp 3941 df-op 3943 df-uni 4169 df-int 4205 df-iun 4250 df-br 4375 df-opab 4434 df-mpt 4435 df-tr 4470 df-eprel 4723 df-id 4727 df-po 4733 df-so 4734 df-fr 4771 df-se 4772 df-we 4773 df-xp 4818 df-rel 4819 df-cnv 4820 df-co 4821 df-dm 4822 df-rn 4823 df-res 4824 df-ima 4825 df-pred 5359 df-ord 5405 df-on 5406 df-lim 5407 df-suc 5408 df-iota 5525 df-fun 5563 df-fn 5564 df-f 5565 df-f1 5566 df-fo 5567 df-f1o 5568 df-fv 5569 df-isom 5570 df-riota 6238 df-ov 6279 df-oprab 6280 df-mpt2 6281 df-of 6519 df-om 6681 df-1st 6781 df-2nd 6782 df-wrecs 7015 df-recs 7077 df-rdg 7115 df-1o 7169 df-oadd 7173 df-er 7350 df-map 7461 df-pm 7462 df-en 7557 df-dom 7558 df-sdom 7559 df-fin 7560 df-sup 7943 df-inf 7944 df-oi 8012 df-card 8360 df-pnf 9664 df-mnf 9665 df-xr 9666 df-ltxr 9667 df-le 9668 df-sub 9849 df-neg 9850 df-div 10259 df-nn 10599 df-2 10657 df-3 10658 df-n0 10860 df-z 10928 df-uz 11150 df-rp 11293 df-fz 11776 df-fzo 11909 df-fl 12022 df-seq 12208 df-exp 12267 df-hash 12510 df-cj 13173 df-re 13174 df-im 13175 df-sqrt 13309 df-abs 13310 df-clim 13563 df-rlim 13564 df-sum 13764 df-0p 22640 df-ply 23154 df-coe 23156 df-dgr 23157 df-aa 23280

This theorem is referenced by: aannenlem3 23298

W3C validator