bposlem1 - Metamath Proof Explorer

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

Theorem bposlem1 21021

Description: An upper bound on the prime powers dividing a central binomial coefficient. (Contributed by Mario Carneiro, 9-Mar-2014.)

**Assertion**
Ref	Expression
bposlem1	$/\$

Proof of Theorem bposlem1 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fzfid 11267	. . . 4 $/\$
2		2nn 10089	. . . . . . . . . . 11
3		nnmulcl 9979	. . . . . . . . . . 11 $/\$
4	2, 3	mpan 652	. . . . . . . . . 10
5	4	ad2antrr 707	. . . . . . . . 9 $/\$ $/\$
6		prmnn 13037	. . . . . . . . . . 11
7	6	ad2antlr 708	. . . . . . . . . 10 $/\$ $/\$
8		elfznn 11036	. . . . . . . . . . . 12
9	8	adantl 453	. . . . . . . . . . 11 $/\$ $/\$
10	9	nnnn0d 10230	. . . . . . . . . 10 $/\$ $/\$
11	7, 10	nnexpcld 11499	. . . . . . . . 9 $/\$ $/\$
12		nnrp 10577	. . . . . . . . . 10
13		nnrp 10577	. . . . . . . . . 10
14		rpdivcl 10590	. . . . . . . . . 10 $/\$
15	12, 13, 14	syl2an 464	. . . . . . . . 9 $/\$
16	5, 11, 15	syl2anc 643	. . . . . . . 8 $/\$ $/\$
17	16	rpred 10604	. . . . . . 7 $/\$ $/\$
18	17	flcld 11162	. . . . . 6 $/\$ $/\$
19		2z 10268	. . . . . . 7
20		simpll 731	. . . . . . . . . 10 $/\$ $/\$
21		nnrp 10577	. . . . . . . . . . 11
22		rpdivcl 10590	. . . . . . . . . . 11 $/\$
23	21, 13, 22	syl2an 464	. . . . . . . . . 10 $/\$
24	20, 11, 23	syl2anc 643	. . . . . . . . 9 $/\$ $/\$
25	24	rpred 10604	. . . . . . . 8 $/\$ $/\$
26	25	flcld 11162	. . . . . . 7 $/\$ $/\$
27		zmulcl 10280	. . . . . . 7 $/\$
28	19, 26, 27	sylancr 645	. . . . . 6 $/\$ $/\$
29	18, 28	zsubcld 10336	. . . . 5 $/\$ $/\$
30	29	zred 10331	. . . 4 $/\$ $/\$
31		1re 9046	. . . . . 6
32		0re 9047	. . . . . 6
33	31, 32	keepel 3756	. . . . 5
34	33	a1i 11	. . . 4 $/\$ $/\$
35	28	zred 10331	. . . . . . . . . 10 $/\$ $/\$
36	17, 35	resubcld 9421	. . . . . . . . 9 $/\$ $/\$
37		2re 10025	. . . . . . . . . 10
38	37	a1i 11	. . . . . . . . 9 $/\$ $/\$
39	18	zred 10331	. . . . . . . . . 10 $/\$ $/\$
40		flle 11163	. . . . . . . . . . 11
41	17, 40	syl 16	. . . . . . . . . 10 $/\$ $/\$
42	39, 17, 35, 41	lesub1dd 9598	. . . . . . . . 9 $/\$ $/\$
43		resubcl 9321	. . . . . . . . . . . . 13 $/\$
44	25, 31, 43	sylancl 644	. . . . . . . . . . . 12 $/\$ $/\$
45		remulcl 9031	. . . . . . . . . . . 12 $/\$
46	37, 44, 45	sylancr 645	. . . . . . . . . . 11 $/\$ $/\$
47		flltp1 11164	. . . . . . . . . . . . . 14
48	25, 47	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$
49	31	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
50	26	zred 10331	. . . . . . . . . . . . . 14 $/\$ $/\$
51	25, 49, 50	ltsubaddd 9578	. . . . . . . . . . . . 13 $/\$ $/\$
52	48, 51	mpbird 224	. . . . . . . . . . . 12 $/\$ $/\$
53		2pos 10038	. . . . . . . . . . . . . . 15
54	37, 53	pm3.2i 442	. . . . . . . . . . . . . 14 $/\$
55		ltmul2 9817	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
56	54, 55	mp3an3 1268	. . . . . . . . . . . . 13 $/\$
57	44, 50, 56	syl2anc 643	. . . . . . . . . . . 12 $/\$ $/\$
58	52, 57	mpbid 202	. . . . . . . . . . 11 $/\$ $/\$
59	46, 35, 17, 58	ltsub2dd 9595	. . . . . . . . . 10 $/\$ $/\$
60		2cn 10026	. . . . . . . . . . . . . 14
61	60	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
62		nncn 9964	. . . . . . . . . . . . . 14
63	62	ad2antrr 707	. . . . . . . . . . . . 13 $/\$ $/\$
64	11	nncnd 9972	. . . . . . . . . . . . 13 $/\$ $/\$
65	11	nnne0d 10000	. . . . . . . . . . . . 13 $/\$ $/\$
66	61, 63, 64, 65	divassd 9781	. . . . . . . . . . . 12 $/\$ $/\$
67	25	recnd 9070	. . . . . . . . . . . . . 14 $/\$ $/\$
68		ax-1cn 9004	. . . . . . . . . . . . . . 15
69	68	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
70	61, 67, 69	subdid 9445	. . . . . . . . . . . . 13 $/\$ $/\$
71	60	mulid1i 9048	. . . . . . . . . . . . . 14
72	71	oveq2i 6051	. . . . . . . . . . . . 13
73	70, 72	syl6eq 2452	. . . . . . . . . . . 12 $/\$ $/\$
74	66, 73	oveq12d 6058	. . . . . . . . . . 11 $/\$ $/\$
75		remulcl 9031	. . . . . . . . . . . . . 14 $/\$
76	37, 25, 75	sylancr 645	. . . . . . . . . . . . 13 $/\$ $/\$
77	76	recnd 9070	. . . . . . . . . . . 12 $/\$ $/\$
78		nncan 9286	. . . . . . . . . . . 12 $/\$
79	77, 60, 78	sylancl 644	. . . . . . . . . . 11 $/\$ $/\$
80	74, 79	eqtrd 2436	. . . . . . . . . 10 $/\$ $/\$
81	59, 80	breqtrd 4196	. . . . . . . . 9 $/\$ $/\$
82	30, 36, 38, 42, 81	lelttrd 9184	. . . . . . . 8 $/\$ $/\$
83		df-2 10014	. . . . . . . 8
84	82, 83	syl6breq 4211	. . . . . . 7 $/\$ $/\$
85		1z 10267	. . . . . . . 8
86		zleltp1 10282	. . . . . . . 8 $/\$
87	29, 85, 86	sylancl 644	. . . . . . 7 $/\$ $/\$
88	84, 87	mpbird 224	. . . . . 6 $/\$ $/\$
89		iftrue 3705	. . . . . . 7
90	89	breq2d 4184	. . . . . 6
91	88, 90	syl5ibrcom 214	. . . . 5 $/\$ $/\$
92	9	nnge1d 9998	. . . . . . . . . . 11 $/\$ $/\$
93	92	biantrurd 495	. . . . . . . . . 10 $/\$ $/\$ $/\$
94	6	adantl 453	. . . . . . . . . . . . . 14 $/\$
95	94	nnred 9971	. . . . . . . . . . . . 13 $/\$
96		prmuz2 13052	. . . . . . . . . . . . . . 15
97	96	adantl 453	. . . . . . . . . . . . . 14 $/\$
98		eluz2b1 10503	. . . . . . . . . . . . . . 15 $/\$
99	98	simprbi 451	. . . . . . . . . . . . . 14
100	97, 99	syl 16	. . . . . . . . . . . . 13 $/\$
101	95, 100	jca 519	. . . . . . . . . . . 12 $/\$ $/\$
102	101	adantr 452	. . . . . . . . . . 11 $/\$ $/\$ $/\$
103		elfzelz 11015	. . . . . . . . . . . 12
104	103	adantl 453	. . . . . . . . . . 11 $/\$ $/\$
105	4	adantr 452	. . . . . . . . . . . . 13 $/\$
106	105	nnrpd 10603	. . . . . . . . . . . 12 $/\$
107	106	adantr 452	. . . . . . . . . . 11 $/\$ $/\$
108		efexple 21018	. . . . . . . . . . 11 $/\$ $/\$ $/\$
109	102, 104, 107, 108	syl3anc 1184	. . . . . . . . . 10 $/\$ $/\$
110	9	nnzd 10330	. . . . . . . . . . 11 $/\$ $/\$
111	85	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
112	105	nnred 9971	. . . . . . . . . . . . . . . 16 $/\$
113	31	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
114	37	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
115		1lt2 10098	. . . . . . . . . . . . . . . . . 18
116	115	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
117		nnre 9963	. . . . . . . . . . . . . . . . . . . 20
118	117	adantr 452	. . . . . . . . . . . . . . . . . . 19 $/\$
119	32, 37, 53	ltleii 9152	. . . . . . . . . . . . . . . . . . . . 21
120	37, 119	pm3.2i 442	. . . . . . . . . . . . . . . . . . . 20 $/\$
121	120	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
122		nnge1 9982	. . . . . . . . . . . . . . . . . . . 20
123	122	adantr 452	. . . . . . . . . . . . . . . . . . 19 $/\$
124		lemul2a 9821	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
125	113, 118, 121, 123, 124	syl31anc 1187	. . . . . . . . . . . . . . . . . 18 $/\$
126	71, 125	syl5eqbrr 4206	. . . . . . . . . . . . . . . . 17 $/\$
127	113, 114, 112, 116, 126	ltletrd 9186	. . . . . . . . . . . . . . . 16 $/\$
128	112, 127	rplogcld 20477	. . . . . . . . . . . . . . 15 $/\$
129	95, 100	rplogcld 20477	. . . . . . . . . . . . . . 15 $/\$
130	128, 129	rpdivcld 10621	. . . . . . . . . . . . . 14 $/\$
131	130	rpred 10604	. . . . . . . . . . . . 13 $/\$
132	131	flcld 11162	. . . . . . . . . . . 12 $/\$
133	132	adantr 452	. . . . . . . . . . 11 $/\$ $/\$
134		elfz 11005	. . . . . . . . . . 11 $/\$ $/\$ $/\$
135	110, 111, 133, 134	syl3anc 1184	. . . . . . . . . 10 $/\$ $/\$ $/\$
136	93, 109, 135	3bitr4rd 278	. . . . . . . . 9 $/\$ $/\$
137	136	notbid 286	. . . . . . . 8 $/\$ $/\$
138	112	adantr 452	. . . . . . . . 9 $/\$ $/\$
139	11	nnred 9971	. . . . . . . . 9 $/\$ $/\$
140	138, 139	ltnled 9176	. . . . . . . 8 $/\$ $/\$
141	137, 140	bitr4d 248	. . . . . . 7 $/\$ $/\$
142	16	rpge0d 10608	. . . . . . . . . . . . 13 $/\$ $/\$
143	142	adantrr 698	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
144	11	nngt0d 9999	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
145		ltdivmul 9838	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
146	138, 49, 139, 144, 145	syl112anc 1188	. . . . . . . . . . . . . . . 16 $/\$ $/\$
147	64	mulid1d 9061	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
148	147	breq2d 4184	. . . . . . . . . . . . . . . 16 $/\$ $/\$
149	146, 148	bitrd 245	. . . . . . . . . . . . . . 15 $/\$ $/\$
150	149	biimprd 215	. . . . . . . . . . . . . 14 $/\$ $/\$
151	150	impr 603	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
152		0p1e1 10049	. . . . . . . . . . . . 13
153	151, 152	syl6breqr 4212	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
154	17	adantrr 698	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
155		0z 10249	. . . . . . . . . . . . 13
156		flbi 11178	. . . . . . . . . . . . 13 $/\$ $/\$
157	154, 155, 156	sylancl 644	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
158	143, 153, 157	mpbir2and 889	. . . . . . . . . . 11 $/\$ $/\$ $/\$
159	24	rpge0d 10608	. . . . . . . . . . . . . . 15 $/\$ $/\$
160	159	adantrr 698	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
161	117, 21	ltaddrp2d 10634	. . . . . . . . . . . . . . . . . . . 20
162	62	2timesd 10166	. . . . . . . . . . . . . . . . . . . 20
163	161, 162	breqtrrd 4198	. . . . . . . . . . . . . . . . . . 19
164	163	ad2antrr 707	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
165	117	ad2antrr 707	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
166		lttr 9108	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
167	165, 138, 139, 166	syl3anc 1184	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
168	164, 167	mpand 657	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
169		ltdivmul 9838	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
170	165, 49, 139, 144, 169	syl112anc 1188	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
171	147	breq2d 4184	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
172	170, 171	bitrd 245	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
173	168, 172	sylibrd 226	. . . . . . . . . . . . . . . 16 $/\$ $/\$
174	173	impr 603	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
175	174, 152	syl6breqr 4212	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
176	25	adantrr 698	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
177		flbi 11178	. . . . . . . . . . . . . . 15 $/\$ $/\$
178	176, 155, 177	sylancl 644	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
179	160, 175, 178	mpbir2and 889	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
180	179	oveq2d 6056	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
181	60	mul01i 9212	. . . . . . . . . . . 12
182	180, 181	syl6eq 2452	. . . . . . . . . . 11 $/\$ $/\$ $/\$
183	158, 182	oveq12d 6058	. . . . . . . . . 10 $/\$ $/\$ $/\$
184		0cn 9040	. . . . . . . . . . 11
185	184	subidi 9327	. . . . . . . . . 10
186	183, 185	syl6eq 2452	. . . . . . . . 9 $/\$ $/\$ $/\$
187		0le0 10037	. . . . . . . . 9
188	186, 187	syl6eqbr 4209	. . . . . . . 8 $/\$ $/\$ $/\$
189	188	expr 599	. . . . . . 7 $/\$ $/\$
190	141, 189	sylbid 207	. . . . . 6 $/\$ $/\$
191		iffalse 3706	. . . . . . . 8
192	191	eqcomd 2409	. . . . . . 7
193	192	breq2d 4184	. . . . . 6
194	190, 193	mpbidi 208	. . . . 5 $/\$ $/\$
195	91, 194	pm2.61d 152	. . . 4 $/\$ $/\$
196	1, 30, 34, 195	fsumle 12533	. . 3 $/\$
197		pcbcctr 21013	. . 3 $/\$
198	132	zred 10331	. . . . . . . 8 $/\$
199		flle 11163	. . . . . . . . 9
200	131, 199	syl 16	. . . . . . . 8 $/\$
201	105	nnnn0d 10230	. . . . . . . . . . . . . 14 $/\$
202	94, 201	nnexpcld 11499	. . . . . . . . . . . . 13 $/\$
203	202	nnred 9971	. . . . . . . . . . . 12 $/\$
204		bernneq3 11462	. . . . . . . . . . . . 13 $/\$
205	97, 201, 204	syl2anc 643	. . . . . . . . . . . 12 $/\$
206	112, 203, 205	ltled 9177	. . . . . . . . . . 11 $/\$
207	106	reeflogd 20472	. . . . . . . . . . 11 $/\$
208	94	nnrpd 10603	. . . . . . . . . . . . 13 $/\$
209	105	nnzd 10330	. . . . . . . . . . . . 13 $/\$
210		reexplog 20442	. . . . . . . . . . . . 13 $/\$
211	208, 209, 210	syl2anc 643	. . . . . . . . . . . 12 $/\$
212	211	eqcomd 2409	. . . . . . . . . . 11 $/\$
213	206, 207, 212	3brtr4d 4202	. . . . . . . . . 10 $/\$
214	106	relogcld 20471	. . . . . . . . . . 11 $/\$
215	129	rpred 10604	. . . . . . . . . . . 12 $/\$
216	112, 215	remulcld 9072	. . . . . . . . . . 11 $/\$
217		efle 12674	. . . . . . . . . . 11 $/\$
218	214, 216, 217	syl2anc 643	. . . . . . . . . 10 $/\$
219	213, 218	mpbird 224	. . . . . . . . 9 $/\$
220	214, 112, 129	ledivmul2d 10654	. . . . . . . . 9 $/\$
221	219, 220	mpbird 224	. . . . . . . 8 $/\$
222	198, 131, 112, 200, 221	letrd 9183	. . . . . . 7 $/\$
223		eluz 10455	. . . . . . . 8 $/\$
224	132, 209, 223	syl2anc 643	. . . . . . 7 $/\$
225	222, 224	mpbird 224	. . . . . 6 $/\$
226		fzss2 11048	. . . . . 6
227	225, 226	syl 16	. . . . 5 $/\$
228		sumhash 13220	. . . . 5 $/\$
229	1, 227, 228	syl2anc 643	. . . 4 $/\$
230	130	rprege0d 10611	. . . . 5 $/\$ $/\$
231		flge0nn0 11180	. . . . 5 $/\$
232		hashfz1 11585	. . . . 5
233	230, 231, 232	3syl 19	. . . 4 $/\$
234	229, 233	eqtr2d 2437	. . 3 $/\$
235	196, 197, 234	3brtr4d 4202	. 2 $/\$
236		simpr 448	. . . . 5 $/\$
237		nnnn0 10184	. . . . . . 7
238		fzctr 11072	. . . . . . 7
239		bccl2 11569	. . . . . . 7
240	237, 238, 239	3syl 19	. . . . . 6
241	240	adantr 452	. . . . 5 $/\$
242	236, 241	pccld 13179	. . . 4 $/\$
243	242	nn0zd 10329	. . 3 $/\$
244		efexple 21018	. . 3 $/\$ $/\$ $/\$
245	95, 100, 243, 106, 244	syl211anc 1190	. 2 $/\$
246	235, 245	mpbird 224	1 $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 177 $/\$ wa 359

wceq 1649

wcel 1721

wss 3280

cif 3699 class class class wbr 4172

cfv 5413 (class class class)co 6040

cfn 7068

cc 8944

cr 8945

cc0 8946

c1 8947

caddc 8949

cmul 8951

clt 9076

cle 9077

cmin 9247

cdiv 9633

cn 9956

c2 10005

cn0 10177

cz 10238

cuz 10444

crp 10568

cfz 10999

cfl 11156

cexp 11337

cbc 11548

chash 11573

csu 12434

ce 12619

cprime 13034

cpc 13165

clog 20405

This theorem is referenced by: bposlem5 21025 bposlem6 21026 chebbnd1lem1 21116

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-inf2 7552 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024 ax-addf 9025 ax-mulf 9026

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-iin 4056 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-se 4502 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 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-ov 6043 df-oprab 6044 df-mpt2 6045 df-of 6264 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-2o 6684 df-oadd 6687 df-er 6864 df-map 6979 df-pm 6980 df-ixp 7023 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-fi 7374 df-sup 7404 df-oi 7435 df-card 7782 df-cda 8004 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-3 10015 df-4 10016 df-5 10017 df-6 10018 df-7 10019 df-8 10020 df-9 10021 df-10 10022 df-n0 10178 df-z 10239 df-dec 10339 df-uz 10445 df-q 10531 df-rp 10569 df-xneg 10666 df-xadd 10667 df-xmul 10668 df-ioo 10876 df-ioc 10877 df-ico 10878 df-icc 10879 df-fz 11000 df-fzo 11091 df-fl 11157 df-mod 11206 df-seq 11279 df-exp 11338 df-fac 11522 df-bc 11549 df-hash 11574 df-shft 11837 df-cj 11859 df-re 11860 df-im 11861 df-sqr 11995 df-abs 11996 df-limsup 12220 df-clim 12237 df-rlim 12238 df-sum 12435 df-ef 12625 df-sin 12627 df-cos 12628 df-pi 12630 df-dvds 12808 df-gcd 12962 df-prm 13035 df-pc 13166 df-struct 13426 df-ndx 13427 df-slot 13428 df-base 13429 df-sets 13430 df-ress 13431 df-plusg 13497 df-mulr 13498 df-starv 13499 df-sca 13500 df-vsca 13501 df-tset 13503 df-ple 13504 df-ds 13506 df-unif 13507 df-hom 13508 df-cco 13509 df-rest 13605 df-topn 13606 df-topgen 13622 df-pt 13623 df-prds 13626 df-xrs 13681 df-0g 13682 df-gsum 13683 df-qtop 13688 df-imas 13689 df-xps 13691 df-mre 13766 df-mrc 13767 df-acs 13769 df-mnd 14645 df-submnd 14694 df-mulg 14770 df-cntz 15071 df-cmn 15369 df-psmet 16649 df-xmet 16650 df-met 16651 df-bl 16652 df-mopn 16653 df-fbas 16654 df-fg 16655 df-cnfld 16659 df-top 16918 df-bases 16920 df-topon 16921 df-topsp 16922 df-cld 17038 df-ntr 17039 df-cls 17040 df-nei 17117 df-lp 17155 df-perf 17156 df-cn 17245 df-cnp 17246 df-haus 17333 df-tx 17547 df-hmeo 17740 df-fil 17831 df-fm 17923 df-flim 17924 df-flf 17925 df-xms 18303 df-ms 18304 df-tms 18305 df-cncf 18861 df-limc 19706 df-dv 19707 df-log 20407

W3C validator