bposlem1 - Metamath Proof Explorer

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

Theorem bposlem1 24291

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 12224	. . . 4 $/\$
2		2nn 10790	. . . . . . . . . . 11
3		nnmulcl 10654	. . . . . . . . . . 11 $/\$
4	2, 3	mpan 684	. . . . . . . . . 10
5	4	ad2antrr 740	. . . . . . . . 9 $/\$ $/\$
6		prmnn 14704	. . . . . . . . . . 11
7	6	ad2antlr 741	. . . . . . . . . 10 $/\$ $/\$
8		elfznn 11854	. . . . . . . . . . . 12
9	8	adantl 473	. . . . . . . . . . 11 $/\$ $/\$
10	9	nnnn0d 10949	. . . . . . . . . 10 $/\$ $/\$
11	7, 10	nnexpcld 12475	. . . . . . . . 9 $/\$ $/\$
12		nnrp 11334	. . . . . . . . . 10
13		nnrp 11334	. . . . . . . . . 10
14		rpdivcl 11348	. . . . . . . . . 10 $/\$
15	12, 13, 14	syl2an 485	. . . . . . . . 9 $/\$
16	5, 11, 15	syl2anc 673	. . . . . . . 8 $/\$ $/\$
17	16	rpred 11364	. . . . . . 7 $/\$ $/\$
18	17	flcld 12067	. . . . . 6 $/\$ $/\$
19		2z 10993	. . . . . . 7
20		simpll 768	. . . . . . . . . 10 $/\$ $/\$
21		nnrp 11334	. . . . . . . . . . 11
22		rpdivcl 11348	. . . . . . . . . . 11 $/\$
23	21, 13, 22	syl2an 485	. . . . . . . . . 10 $/\$
24	20, 11, 23	syl2anc 673	. . . . . . . . 9 $/\$ $/\$
25	24	rpred 11364	. . . . . . . 8 $/\$ $/\$
26	25	flcld 12067	. . . . . . 7 $/\$ $/\$
27		zmulcl 11009	. . . . . . 7 $/\$
28	19, 26, 27	sylancr 676	. . . . . 6 $/\$ $/\$
29	18, 28	zsubcld 11068	. . . . 5 $/\$ $/\$
30	29	zred 11063	. . . 4 $/\$ $/\$
31		1re 9660	. . . . . 6
32		0re 9661	. . . . . 6
33	31, 32	keepel 3939	. . . . 5
34	33	a1i 11	. . . 4 $/\$ $/\$
35	28	zred 11063	. . . . . . . . . 10 $/\$ $/\$
36	17, 35	resubcld 10068	. . . . . . . . 9 $/\$ $/\$
37		2re 10701	. . . . . . . . . 10
38	37	a1i 11	. . . . . . . . 9 $/\$ $/\$
39	18	zred 11063	. . . . . . . . . 10 $/\$ $/\$
40		flle 12068	. . . . . . . . . . 11
41	17, 40	syl 17	. . . . . . . . . 10 $/\$ $/\$
42	39, 17, 35, 41	lesub1dd 10250	. . . . . . . . 9 $/\$ $/\$
43		resubcl 9958	. . . . . . . . . . . . 13 $/\$
44	25, 31, 43	sylancl 675	. . . . . . . . . . . 12 $/\$ $/\$
45		remulcl 9642	. . . . . . . . . . . 12 $/\$
46	37, 44, 45	sylancr 676	. . . . . . . . . . 11 $/\$ $/\$
47		flltp1 12069	. . . . . . . . . . . . . 14
48	25, 47	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
49		1red 9676	. . . . . . . . . . . . . 14 $/\$ $/\$
50	26	zred 11063	. . . . . . . . . . . . . 14 $/\$ $/\$
51	25, 49, 50	ltsubaddd 10230	. . . . . . . . . . . . 13 $/\$ $/\$
52	48, 51	mpbird 240	. . . . . . . . . . . 12 $/\$ $/\$
53		2pos 10723	. . . . . . . . . . . . . . 15
54	37, 53	pm3.2i 462	. . . . . . . . . . . . . 14 $/\$
55		ltmul2 10478	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
56	54, 55	mp3an3 1379	. . . . . . . . . . . . 13 $/\$
57	44, 50, 56	syl2anc 673	. . . . . . . . . . . 12 $/\$ $/\$
58	52, 57	mpbid 215	. . . . . . . . . . 11 $/\$ $/\$
59	46, 35, 17, 58	ltsub2dd 10247	. . . . . . . . . 10 $/\$ $/\$
60		2cnd 10704	. . . . . . . . . . . . 13 $/\$ $/\$
61		nncn 10639	. . . . . . . . . . . . . 14
62	61	ad2antrr 740	. . . . . . . . . . . . 13 $/\$ $/\$
63	11	nncnd 10647	. . . . . . . . . . . . 13 $/\$ $/\$
64	11	nnne0d 10676	. . . . . . . . . . . . 13 $/\$ $/\$
65	60, 62, 63, 64	divassd 10440	. . . . . . . . . . . 12 $/\$ $/\$
66	25	recnd 9687	. . . . . . . . . . . . . 14 $/\$ $/\$
67		1cnd 9677	. . . . . . . . . . . . . 14 $/\$ $/\$
68	60, 66, 67	subdid 10095	. . . . . . . . . . . . 13 $/\$ $/\$
69		2t1e2 10781	. . . . . . . . . . . . . 14
70	69	oveq2i 6319	. . . . . . . . . . . . 13
71	68, 70	syl6eq 2521	. . . . . . . . . . . 12 $/\$ $/\$
72	65, 71	oveq12d 6326	. . . . . . . . . . 11 $/\$ $/\$
73		remulcl 9642	. . . . . . . . . . . . . 14 $/\$
74	37, 25, 73	sylancr 676	. . . . . . . . . . . . 13 $/\$ $/\$
75	74	recnd 9687	. . . . . . . . . . . 12 $/\$ $/\$
76		2cn 10702	. . . . . . . . . . . 12
77		nncan 9923	. . . . . . . . . . . 12 $/\$
78	75, 76, 77	sylancl 675	. . . . . . . . . . 11 $/\$ $/\$
79	72, 78	eqtrd 2505	. . . . . . . . . 10 $/\$ $/\$
80	59, 79	breqtrd 4420	. . . . . . . . 9 $/\$ $/\$
81	30, 36, 38, 42, 80	lelttrd 9810	. . . . . . . 8 $/\$ $/\$
82		df-2 10690	. . . . . . . 8
83	81, 82	syl6breq 4435	. . . . . . 7 $/\$ $/\$
84		1z 10991	. . . . . . . 8
85		zleltp1 11011	. . . . . . . 8 $/\$
86	29, 84, 85	sylancl 675	. . . . . . 7 $/\$ $/\$
87	83, 86	mpbird 240	. . . . . 6 $/\$ $/\$
88		iftrue 3878	. . . . . . 7
89	88	breq2d 4407	. . . . . 6
90	87, 89	syl5ibrcom 230	. . . . 5 $/\$ $/\$
91	9	nnge1d 10674	. . . . . . . . . . 11 $/\$ $/\$
92	91	biantrurd 516	. . . . . . . . . 10 $/\$ $/\$ $/\$
93	6	adantl 473	. . . . . . . . . . . . . 14 $/\$
94	93	nnred 10646	. . . . . . . . . . . . 13 $/\$
95		prmuz2 14721	. . . . . . . . . . . . . . 15
96	95	adantl 473	. . . . . . . . . . . . . 14 $/\$
97		eluz2b1 11253	. . . . . . . . . . . . . . 15 $/\$
98	97	simprbi 471	. . . . . . . . . . . . . 14
99	96, 98	syl 17	. . . . . . . . . . . . 13 $/\$
100	94, 99	jca 541	. . . . . . . . . . . 12 $/\$ $/\$
101	100	adantr 472	. . . . . . . . . . 11 $/\$ $/\$ $/\$
102		elfzelz 11826	. . . . . . . . . . . 12
103	102	adantl 473	. . . . . . . . . . 11 $/\$ $/\$
104	4	adantr 472	. . . . . . . . . . . . 13 $/\$
105	104	nnrpd 11362	. . . . . . . . . . . 12 $/\$
106	105	adantr 472	. . . . . . . . . . 11 $/\$ $/\$
107		efexple 24288	. . . . . . . . . . 11 $/\$ $/\$ $/\$
108	101, 103, 106, 107	syl3anc 1292	. . . . . . . . . 10 $/\$ $/\$
109	9	nnzd 11062	. . . . . . . . . . 11 $/\$ $/\$
110	84	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
111	104	nnred 10646	. . . . . . . . . . . . . . . 16 $/\$
112		1red 9676	. . . . . . . . . . . . . . . . 17 $/\$
113	37	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
114		1lt2 10799	. . . . . . . . . . . . . . . . . 18
115	114	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
116		nnre 10638	. . . . . . . . . . . . . . . . . . . 20
117	116	adantr 472	. . . . . . . . . . . . . . . . . . 19 $/\$
118		0le2 10722	. . . . . . . . . . . . . . . . . . . . 21
119	37, 118	pm3.2i 462	. . . . . . . . . . . . . . . . . . . 20 $/\$
120	119	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
121		nnge1 10657	. . . . . . . . . . . . . . . . . . . 20
122	121	adantr 472	. . . . . . . . . . . . . . . . . . 19 $/\$
123		lemul2a 10482	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
124	112, 117, 120, 122, 123	syl31anc 1295	. . . . . . . . . . . . . . . . . 18 $/\$
125	69, 124	syl5eqbrr 4430	. . . . . . . . . . . . . . . . 17 $/\$
126	112, 113, 111, 115, 125	ltletrd 9812	. . . . . . . . . . . . . . . 16 $/\$
127	111, 126	rplogcld 23657	. . . . . . . . . . . . . . 15 $/\$
128	94, 99	rplogcld 23657	. . . . . . . . . . . . . . 15 $/\$
129	127, 128	rpdivcld 11381	. . . . . . . . . . . . . 14 $/\$
130	129	rpred 11364	. . . . . . . . . . . . 13 $/\$
131	130	flcld 12067	. . . . . . . . . . . 12 $/\$
132	131	adantr 472	. . . . . . . . . . 11 $/\$ $/\$
133		elfz 11816	. . . . . . . . . . 11 $/\$ $/\$ $/\$
134	109, 110, 132, 133	syl3anc 1292	. . . . . . . . . 10 $/\$ $/\$ $/\$
135	92, 108, 134	3bitr4rd 294	. . . . . . . . 9 $/\$ $/\$
136	135	notbid 301	. . . . . . . 8 $/\$ $/\$
137	111	adantr 472	. . . . . . . . 9 $/\$ $/\$
138	11	nnred 10646	. . . . . . . . 9 $/\$ $/\$
139	137, 138	ltnled 9799	. . . . . . . 8 $/\$ $/\$
140	136, 139	bitr4d 264	. . . . . . 7 $/\$ $/\$
141	16	rpge0d 11368	. . . . . . . . . . . . 13 $/\$ $/\$
142	141	adantrr 731	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
143	11	nngt0d 10675	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
144		ltdivmul 10502	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
145	137, 49, 138, 143, 144	syl112anc 1296	. . . . . . . . . . . . . . . 16 $/\$ $/\$
146	63	mulid1d 9678	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
147	146	breq2d 4407	. . . . . . . . . . . . . . . 16 $/\$ $/\$
148	145, 147	bitrd 261	. . . . . . . . . . . . . . 15 $/\$ $/\$
149	148	biimprd 231	. . . . . . . . . . . . . 14 $/\$ $/\$
150	149	impr 631	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
151		0p1e1 10743	. . . . . . . . . . . . 13
152	150, 151	syl6breqr 4436	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
153	17	adantrr 731	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
154		0z 10972	. . . . . . . . . . . . 13
155		flbi 12084	. . . . . . . . . . . . 13 $/\$ $/\$
156	153, 154, 155	sylancl 675	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
157	142, 152, 156	mpbir2and 936	. . . . . . . . . . 11 $/\$ $/\$ $/\$
158	24	rpge0d 11368	. . . . . . . . . . . . . . 15 $/\$ $/\$
159	158	adantrr 731	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
160	116, 21	ltaddrp2d 11395	. . . . . . . . . . . . . . . . . . . 20
161	61	2timesd 10878	. . . . . . . . . . . . . . . . . . . 20
162	160, 161	breqtrrd 4422	. . . . . . . . . . . . . . . . . . 19
163	162	ad2antrr 740	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
164	116	ad2antrr 740	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
165		lttr 9728	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
166	164, 137, 138, 165	syl3anc 1292	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
167	163, 166	mpand 689	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
168		ltdivmul 10502	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
169	164, 49, 138, 143, 168	syl112anc 1296	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
170	146	breq2d 4407	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
171	169, 170	bitrd 261	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
172	167, 171	sylibrd 242	. . . . . . . . . . . . . . . 16 $/\$ $/\$
173	172	impr 631	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
174	173, 151	syl6breqr 4436	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
175	25	adantrr 731	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
176		flbi 12084	. . . . . . . . . . . . . . 15 $/\$ $/\$
177	175, 154, 176	sylancl 675	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
178	159, 174, 177	mpbir2and 936	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
179	178	oveq2d 6324	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
180		2t0e0 10788	. . . . . . . . . . . 12
181	179, 180	syl6eq 2521	. . . . . . . . . . 11 $/\$ $/\$ $/\$
182	157, 181	oveq12d 6326	. . . . . . . . . 10 $/\$ $/\$ $/\$
183		0m0e0 10741	. . . . . . . . . 10
184	182, 183	syl6eq 2521	. . . . . . . . 9 $/\$ $/\$ $/\$
185		0le0 10721	. . . . . . . . 9
186	184, 185	syl6eqbr 4433	. . . . . . . 8 $/\$ $/\$ $/\$
187	186	expr 626	. . . . . . 7 $/\$ $/\$
188	140, 187	sylbid 223	. . . . . 6 $/\$ $/\$
189		iffalse 3881	. . . . . . . 8
190	189	eqcomd 2477	. . . . . . 7
191	190	breq2d 4407	. . . . . 6
192	188, 191	mpbidi 224	. . . . 5 $/\$ $/\$
193	90, 192	pm2.61d 163	. . . 4 $/\$ $/\$
194	1, 30, 34, 193	fsumle 13936	. . 3 $/\$
195		pcbcctr 24283	. . 3 $/\$
196	131	zred 11063	. . . . . . . 8 $/\$
197		flle 12068	. . . . . . . . 9
198	130, 197	syl 17	. . . . . . . 8 $/\$
199	104	nnnn0d 10949	. . . . . . . . . . . . . 14 $/\$
200	93, 199	nnexpcld 12475	. . . . . . . . . . . . 13 $/\$
201	200	nnred 10646	. . . . . . . . . . . 12 $/\$
202		bernneq3 12438	. . . . . . . . . . . . 13 $/\$
203	96, 199, 202	syl2anc 673	. . . . . . . . . . . 12 $/\$
204	111, 201, 203	ltled 9800	. . . . . . . . . . 11 $/\$
205	105	reeflogd 23652	. . . . . . . . . . 11 $/\$
206	93	nnrpd 11362	. . . . . . . . . . . . 13 $/\$
207	104	nnzd 11062	. . . . . . . . . . . . 13 $/\$
208		reexplog 23623	. . . . . . . . . . . . 13 $/\$
209	206, 207, 208	syl2anc 673	. . . . . . . . . . . 12 $/\$
210	209	eqcomd 2477	. . . . . . . . . . 11 $/\$
211	204, 205, 210	3brtr4d 4426	. . . . . . . . . 10 $/\$
212	105	relogcld 23651	. . . . . . . . . . 11 $/\$
213	128	rpred 11364	. . . . . . . . . . . 12 $/\$
214	111, 213	remulcld 9689	. . . . . . . . . . 11 $/\$
215		efle 14249	. . . . . . . . . . 11 $/\$
216	212, 214, 215	syl2anc 673	. . . . . . . . . 10 $/\$
217	211, 216	mpbird 240	. . . . . . . . 9 $/\$
218	212, 111, 128	ledivmul2d 11415	. . . . . . . . 9 $/\$
219	217, 218	mpbird 240	. . . . . . . 8 $/\$
220	196, 130, 111, 198, 219	letrd 9809	. . . . . . 7 $/\$
221		eluz 11196	. . . . . . . 8 $/\$
222	131, 207, 221	syl2anc 673	. . . . . . 7 $/\$
223	220, 222	mpbird 240	. . . . . 6 $/\$
224		fzss2 11864	. . . . . 6
225	223, 224	syl 17	. . . . 5 $/\$
226		sumhash 14920	. . . . 5 $/\$
227	1, 225, 226	syl2anc 673	. . . 4 $/\$
228	129	rprege0d 11371	. . . . 5 $/\$ $/\$
229		flge0nn0 12087	. . . . 5 $/\$
230		hashfz1 12567	. . . . 5
231	228, 229, 230	3syl 18	. . . 4 $/\$
232	227, 231	eqtr2d 2506	. . 3 $/\$
233	194, 195, 232	3brtr4d 4426	. 2 $/\$
234		simpr 468	. . . . 5 $/\$
235		nnnn0 10900	. . . . . . 7
236		fzctr 11928	. . . . . . 7
237		bccl2 12546	. . . . . . 7
238	235, 236, 237	3syl 18	. . . . . 6
239	238	adantr 472	. . . . 5 $/\$
240	234, 239	pccld 14879	. . . 4 $/\$
241	240	nn0zd 11061	. . 3 $/\$
242		efexple 24288	. . 3 $/\$ $/\$ $/\$
243	94, 99, 241, 105, 242	syl211anc 1298	. 2 $/\$
244	233, 243	mpbird 240	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $/\$ wa 376

wceq 1452

wcel 1904

wss 3390

cif 3872 class class class wbr 4395

cfv 5589 (class class class)co 6308

cfn 7587

cc 9555

cr 9556

cc0 9557

c1 9558

caddc 9560

cmul 9562

clt 9693

cle 9694

cmin 9880

cdiv 10291

cn 10631

c2 10681

cn0 10893

cz 10961

cuz 11182

crp 11325

cfz 11810

cfl 12059

cexp 12310

cbc 12525

chash 12553

csu 13829

ce 14191

cprime 14701

cpc 14865

clog 23583

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635 ax-addf 9636 ax-mulf 9637

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-iin 4272 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-of 6550 df-om 6712 df-1st 6812 df-2nd 6813 df-supp 6934 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-er 7381 df-map 7492 df-pm 7493 df-ixp 7541 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-fsupp 7902 df-fi 7943 df-sup 7974 df-inf 7975 df-oi 8043 df-card 8391 df-cda 8616 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-4 10692 df-5 10693 df-6 10694 df-7 10695 df-8 10696 df-9 10697 df-10 10698 df-n0 10894 df-z 10962 df-dec 11075 df-uz 11183 df-q 11288 df-rp 11326 df-xneg 11432 df-xadd 11433 df-xmul 11434 df-ioo 11664 df-ioc 11665 df-ico 11666 df-icc 11667 df-fz 11811 df-fzo 11943 df-fl 12061 df-mod 12130 df-seq 12252 df-exp 12311 df-fac 12498 df-bc 12526 df-hash 12554 df-shft 13207 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-limsup 13603 df-clim 13629 df-rlim 13630 df-sum 13830 df-ef 14198 df-sin 14200 df-cos 14201 df-pi 14203 df-dvds 14383 df-gcd 14548 df-prm 14702 df-pc 14866 df-struct 15201 df-ndx 15202 df-slot 15203 df-base 15204 df-sets 15205 df-ress 15206 df-plusg 15281 df-mulr 15282 df-starv 15283 df-sca 15284 df-vsca 15285 df-ip 15286 df-tset 15287 df-ple 15288 df-ds 15290 df-unif 15291 df-hom 15292 df-cco 15293 df-rest 15399 df-topn 15400 df-0g 15418 df-gsum 15419 df-topgen 15420 df-pt 15421 df-prds 15424 df-xrs 15478 df-qtop 15484 df-imas 15485 df-xps 15488 df-mre 15570 df-mrc 15571 df-acs 15573 df-mgm 16566 df-sgrp 16605 df-mnd 16615 df-submnd 16661 df-mulg 16754 df-cntz 17049 df-cmn 17510 df-psmet 19039 df-xmet 19040 df-met 19041 df-bl 19042 df-mopn 19043 df-fbas 19044 df-fg 19045 df-cnfld 19048 df-top 19998 df-bases 19999 df-topon 20000 df-topsp 20001 df-cld 20111 df-ntr 20112 df-cls 20113 df-nei 20191 df-lp 20229 df-perf 20230 df-cn 20320 df-cnp 20321 df-haus 20408 df-tx 20654 df-hmeo 20847 df-fil 20939 df-fm 21031 df-flim 21032 df-flf 21033 df-xms 21413 df-ms 21414 df-tms 21415 df-cncf 21988 df-limc 22900 df-dv 22901 df-log 23585

This theorem is referenced by: bposlem5 24295 bposlem6 24296 chebbnd1lem1 24386

W3C validator