bposlem1 - Metamath Proof Explorer

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

Theorem bposlem1 23287

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 12047	. . . 4 $/\$
2		2nn 10689	. . . . . . . . . . 11
3		nnmulcl 10555	. . . . . . . . . . 11 $/\$
4	2, 3	mpan 670	. . . . . . . . . 10
5	4	ad2antrr 725	. . . . . . . . 9 $/\$ $/\$
6		prmnn 14075	. . . . . . . . . . 11
7	6	ad2antlr 726	. . . . . . . . . 10 $/\$ $/\$
8		elfznn 11710	. . . . . . . . . . . 12
9	8	adantl 466	. . . . . . . . . . 11 $/\$ $/\$
10	9	nnnn0d 10848	. . . . . . . . . 10 $/\$ $/\$
11	7, 10	nnexpcld 12295	. . . . . . . . 9 $/\$ $/\$
12		nnrp 11225	. . . . . . . . . 10
13		nnrp 11225	. . . . . . . . . 10
14		rpdivcl 11238	. . . . . . . . . 10 $/\$
15	12, 13, 14	syl2an 477	. . . . . . . . 9 $/\$
16	5, 11, 15	syl2anc 661	. . . . . . . 8 $/\$ $/\$
17	16	rpred 11252	. . . . . . 7 $/\$ $/\$
18	17	flcld 11899	. . . . . 6 $/\$ $/\$
19		2z 10892	. . . . . . 7
20		simpll 753	. . . . . . . . . 10 $/\$ $/\$
21		nnrp 11225	. . . . . . . . . . 11
22		rpdivcl 11238	. . . . . . . . . . 11 $/\$
23	21, 13, 22	syl2an 477	. . . . . . . . . 10 $/\$
24	20, 11, 23	syl2anc 661	. . . . . . . . 9 $/\$ $/\$
25	24	rpred 11252	. . . . . . . 8 $/\$ $/\$
26	25	flcld 11899	. . . . . . 7 $/\$ $/\$
27		zmulcl 10907	. . . . . . 7 $/\$
28	19, 26, 27	sylancr 663	. . . . . 6 $/\$ $/\$
29	18, 28	zsubcld 10967	. . . . 5 $/\$ $/\$
30	29	zred 10962	. . . 4 $/\$ $/\$
31		1re 9591	. . . . . 6
32		0re 9592	. . . . . 6
33	31, 32	keepel 4007	. . . . 5
34	33	a1i 11	. . . 4 $/\$ $/\$
35	28	zred 10962	. . . . . . . . . 10 $/\$ $/\$
36	17, 35	resubcld 9983	. . . . . . . . 9 $/\$ $/\$
37		2re 10601	. . . . . . . . . 10
38	37	a1i 11	. . . . . . . . 9 $/\$ $/\$
39	18	zred 10962	. . . . . . . . . 10 $/\$ $/\$
40		flle 11900	. . . . . . . . . . 11
41	17, 40	syl 16	. . . . . . . . . 10 $/\$ $/\$
42	39, 17, 35, 41	lesub1dd 10164	. . . . . . . . 9 $/\$ $/\$
43		resubcl 9879	. . . . . . . . . . . . 13 $/\$
44	25, 31, 43	sylancl 662	. . . . . . . . . . . 12 $/\$ $/\$
45		remulcl 9573	. . . . . . . . . . . 12 $/\$
46	37, 44, 45	sylancr 663	. . . . . . . . . . 11 $/\$ $/\$
47		flltp1 11901	. . . . . . . . . . . . . 14
48	25, 47	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$
49		1red 9607	. . . . . . . . . . . . . 14 $/\$ $/\$
50	26	zred 10962	. . . . . . . . . . . . . 14 $/\$ $/\$
51	25, 49, 50	ltsubaddd 10144	. . . . . . . . . . . . 13 $/\$ $/\$
52	48, 51	mpbird 232	. . . . . . . . . . . 12 $/\$ $/\$
53		2pos 10623	. . . . . . . . . . . . . . 15
54	37, 53	pm3.2i 455	. . . . . . . . . . . . . 14 $/\$
55		ltmul2 10389	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
56	54, 55	mp3an3 1313	. . . . . . . . . . . . 13 $/\$
57	44, 50, 56	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$
58	52, 57	mpbid 210	. . . . . . . . . . 11 $/\$ $/\$
59	46, 35, 17, 58	ltsub2dd 10161	. . . . . . . . . 10 $/\$ $/\$
60		2cnd 10604	. . . . . . . . . . . . 13 $/\$ $/\$
61		nncn 10540	. . . . . . . . . . . . . 14
62	61	ad2antrr 725	. . . . . . . . . . . . 13 $/\$ $/\$
63	11	nncnd 10548	. . . . . . . . . . . . 13 $/\$ $/\$
64	11	nnne0d 10576	. . . . . . . . . . . . 13 $/\$ $/\$
65	60, 62, 63, 64	divassd 10351	. . . . . . . . . . . 12 $/\$ $/\$
66	25	recnd 9618	. . . . . . . . . . . . . 14 $/\$ $/\$
67		1cnd 9608	. . . . . . . . . . . . . 14 $/\$ $/\$
68	60, 66, 67	subdid 10008	. . . . . . . . . . . . 13 $/\$ $/\$
69		2t1e2 10680	. . . . . . . . . . . . . 14
70	69	oveq2i 6293	. . . . . . . . . . . . 13
71	68, 70	syl6eq 2524	. . . . . . . . . . . 12 $/\$ $/\$
72	65, 71	oveq12d 6300	. . . . . . . . . . 11 $/\$ $/\$
73		remulcl 9573	. . . . . . . . . . . . . 14 $/\$
74	37, 25, 73	sylancr 663	. . . . . . . . . . . . 13 $/\$ $/\$
75	74	recnd 9618	. . . . . . . . . . . 12 $/\$ $/\$
76		2cn 10602	. . . . . . . . . . . 12
77		nncan 9844	. . . . . . . . . . . 12 $/\$
78	75, 76, 77	sylancl 662	. . . . . . . . . . 11 $/\$ $/\$
79	72, 78	eqtrd 2508	. . . . . . . . . 10 $/\$ $/\$
80	59, 79	breqtrd 4471	. . . . . . . . 9 $/\$ $/\$
81	30, 36, 38, 42, 80	lelttrd 9735	. . . . . . . 8 $/\$ $/\$
82		df-2 10590	. . . . . . . 8
83	81, 82	syl6breq 4486	. . . . . . 7 $/\$ $/\$
84		1z 10890	. . . . . . . 8
85		zleltp1 10909	. . . . . . . 8 $/\$
86	29, 84, 85	sylancl 662	. . . . . . 7 $/\$ $/\$
87	83, 86	mpbird 232	. . . . . 6 $/\$ $/\$
88		iftrue 3945	. . . . . . 7
89	88	breq2d 4459	. . . . . 6
90	87, 89	syl5ibrcom 222	. . . . 5 $/\$ $/\$
91	9	nnge1d 10574	. . . . . . . . . . 11 $/\$ $/\$
92	91	biantrurd 508	. . . . . . . . . 10 $/\$ $/\$ $/\$
93	6	adantl 466	. . . . . . . . . . . . . 14 $/\$
94	93	nnred 10547	. . . . . . . . . . . . 13 $/\$
95		prmuz2 14090	. . . . . . . . . . . . . . 15
96	95	adantl 466	. . . . . . . . . . . . . 14 $/\$
97		eluz2b1 11149	. . . . . . . . . . . . . . 15 $/\$
98	97	simprbi 464	. . . . . . . . . . . . . 14
99	96, 98	syl 16	. . . . . . . . . . . . 13 $/\$
100	94, 99	jca 532	. . . . . . . . . . . 12 $/\$ $/\$
101	100	adantr 465	. . . . . . . . . . 11 $/\$ $/\$ $/\$
102		elfzelz 11684	. . . . . . . . . . . 12
103	102	adantl 466	. . . . . . . . . . 11 $/\$ $/\$
104	4	adantr 465	. . . . . . . . . . . . 13 $/\$
105	104	nnrpd 11251	. . . . . . . . . . . 12 $/\$
106	105	adantr 465	. . . . . . . . . . 11 $/\$ $/\$
107		efexple 23284	. . . . . . . . . . 11 $/\$ $/\$ $/\$
108	101, 103, 106, 107	syl3anc 1228	. . . . . . . . . 10 $/\$ $/\$
109	9	nnzd 10961	. . . . . . . . . . 11 $/\$ $/\$
110	84	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
111	104	nnred 10547	. . . . . . . . . . . . . . . 16 $/\$
112		1red 9607	. . . . . . . . . . . . . . . . 17 $/\$
113	37	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
114		1lt2 10698	. . . . . . . . . . . . . . . . . 18
115	114	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
116		nnre 10539	. . . . . . . . . . . . . . . . . . . 20
117	116	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
118		0le2 10622	. . . . . . . . . . . . . . . . . . . . 21
119	37, 118	pm3.2i 455	. . . . . . . . . . . . . . . . . . . 20 $/\$
120	119	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
121		nnge1 10558	. . . . . . . . . . . . . . . . . . . 20
122	121	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
123		lemul2a 10393	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
124	112, 117, 120, 122, 123	syl31anc 1231	. . . . . . . . . . . . . . . . . 18 $/\$
125	69, 124	syl5eqbrr 4481	. . . . . . . . . . . . . . . . 17 $/\$
126	112, 113, 111, 115, 125	ltletrd 9737	. . . . . . . . . . . . . . . 16 $/\$
127	111, 126	rplogcld 22742	. . . . . . . . . . . . . . 15 $/\$
128	94, 99	rplogcld 22742	. . . . . . . . . . . . . . 15 $/\$
129	127, 128	rpdivcld 11269	. . . . . . . . . . . . . 14 $/\$
130	129	rpred 11252	. . . . . . . . . . . . 13 $/\$
131	130	flcld 11899	. . . . . . . . . . . 12 $/\$
132	131	adantr 465	. . . . . . . . . . 11 $/\$ $/\$
133		elfz 11674	. . . . . . . . . . 11 $/\$ $/\$ $/\$
134	109, 110, 132, 133	syl3anc 1228	. . . . . . . . . 10 $/\$ $/\$ $/\$
135	92, 108, 134	3bitr4rd 286	. . . . . . . . 9 $/\$ $/\$
136	135	notbid 294	. . . . . . . 8 $/\$ $/\$
137	111	adantr 465	. . . . . . . . 9 $/\$ $/\$
138	11	nnred 10547	. . . . . . . . 9 $/\$ $/\$
139	137, 138	ltnled 9727	. . . . . . . 8 $/\$ $/\$
140	136, 139	bitr4d 256	. . . . . . 7 $/\$ $/\$
141	16	rpge0d 11256	. . . . . . . . . . . . 13 $/\$ $/\$
142	141	adantrr 716	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
143	11	nngt0d 10575	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
144		ltdivmul 10413	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
145	137, 49, 138, 143, 144	syl112anc 1232	. . . . . . . . . . . . . . . 16 $/\$ $/\$
146	63	mulid1d 9609	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
147	146	breq2d 4459	. . . . . . . . . . . . . . . 16 $/\$ $/\$
148	145, 147	bitrd 253	. . . . . . . . . . . . . . 15 $/\$ $/\$
149	148	biimprd 223	. . . . . . . . . . . . . 14 $/\$ $/\$
150	149	impr 619	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
151		0p1e1 10643	. . . . . . . . . . . . 13
152	150, 151	syl6breqr 4487	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
153	17	adantrr 716	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
154		0z 10871	. . . . . . . . . . . . 13
155		flbi 11916	. . . . . . . . . . . . 13 $/\$ $/\$
156	153, 154, 155	sylancl 662	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
157	142, 152, 156	mpbir2and 920	. . . . . . . . . . 11 $/\$ $/\$ $/\$
158	24	rpge0d 11256	. . . . . . . . . . . . . . 15 $/\$ $/\$
159	158	adantrr 716	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
160	116, 21	ltaddrp2d 11282	. . . . . . . . . . . . . . . . . . . 20
161	61	2timesd 10777	. . . . . . . . . . . . . . . . . . . 20
162	160, 161	breqtrrd 4473	. . . . . . . . . . . . . . . . . . 19
163	162	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
164	116	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
165		lttr 9657	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
166	164, 137, 138, 165	syl3anc 1228	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
167	163, 166	mpand 675	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
168		ltdivmul 10413	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
169	164, 49, 138, 143, 168	syl112anc 1232	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
170	146	breq2d 4459	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
171	169, 170	bitrd 253	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
172	167, 171	sylibrd 234	. . . . . . . . . . . . . . . 16 $/\$ $/\$
173	172	impr 619	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
174	173, 151	syl6breqr 4487	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
175	25	adantrr 716	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
176		flbi 11916	. . . . . . . . . . . . . . 15 $/\$ $/\$
177	175, 154, 176	sylancl 662	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
178	159, 174, 177	mpbir2and 920	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
179	178	oveq2d 6298	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
180		2t0e0 10687	. . . . . . . . . . . 12
181	179, 180	syl6eq 2524	. . . . . . . . . . 11 $/\$ $/\$ $/\$
182	157, 181	oveq12d 6300	. . . . . . . . . 10 $/\$ $/\$ $/\$
183		0m0e0 10641	. . . . . . . . . 10
184	182, 183	syl6eq 2524	. . . . . . . . 9 $/\$ $/\$ $/\$
185		0le0 10621	. . . . . . . . 9
186	184, 185	syl6eqbr 4484	. . . . . . . 8 $/\$ $/\$ $/\$
187	186	expr 615	. . . . . . 7 $/\$ $/\$
188	140, 187	sylbid 215	. . . . . 6 $/\$ $/\$
189		iffalse 3948	. . . . . . . 8
190	189	eqcomd 2475	. . . . . . 7
191	190	breq2d 4459	. . . . . 6
192	188, 191	mpbidi 216	. . . . 5 $/\$ $/\$
193	90, 192	pm2.61d 158	. . . 4 $/\$ $/\$
194	1, 30, 34, 193	fsumle 13572	. . 3 $/\$
195		pcbcctr 23279	. . 3 $/\$
196	131	zred 10962	. . . . . . . 8 $/\$
197		flle 11900	. . . . . . . . 9
198	130, 197	syl 16	. . . . . . . 8 $/\$
199	104	nnnn0d 10848	. . . . . . . . . . . . . 14 $/\$
200	93, 199	nnexpcld 12295	. . . . . . . . . . . . 13 $/\$
201	200	nnred 10547	. . . . . . . . . . . 12 $/\$
202		bernneq3 12258	. . . . . . . . . . . . 13 $/\$
203	96, 199, 202	syl2anc 661	. . . . . . . . . . . 12 $/\$
204	111, 201, 203	ltled 9728	. . . . . . . . . . 11 $/\$
205	105	reeflogd 22737	. . . . . . . . . . 11 $/\$
206	93	nnrpd 11251	. . . . . . . . . . . . 13 $/\$
207	104	nnzd 10961	. . . . . . . . . . . . 13 $/\$
208		reexplog 22707	. . . . . . . . . . . . 13 $/\$
209	206, 207, 208	syl2anc 661	. . . . . . . . . . . 12 $/\$
210	209	eqcomd 2475	. . . . . . . . . . 11 $/\$
211	204, 205, 210	3brtr4d 4477	. . . . . . . . . 10 $/\$
212	105	relogcld 22736	. . . . . . . . . . 11 $/\$
213	128	rpred 11252	. . . . . . . . . . . 12 $/\$
214	111, 213	remulcld 9620	. . . . . . . . . . 11 $/\$
215		efle 13710	. . . . . . . . . . 11 $/\$
216	212, 214, 215	syl2anc 661	. . . . . . . . . 10 $/\$
217	211, 216	mpbird 232	. . . . . . . . 9 $/\$
218	212, 111, 128	ledivmul2d 11302	. . . . . . . . 9 $/\$
219	217, 218	mpbird 232	. . . . . . . 8 $/\$
220	196, 130, 111, 198, 219	letrd 9734	. . . . . . 7 $/\$
221		eluz 11091	. . . . . . . 8 $/\$
222	131, 207, 221	syl2anc 661	. . . . . . 7 $/\$
223	220, 222	mpbird 232	. . . . . 6 $/\$
224		fzss2 11719	. . . . . 6
225	223, 224	syl 16	. . . . 5 $/\$
226		sumhash 14270	. . . . 5 $/\$
227	1, 225, 226	syl2anc 661	. . . 4 $/\$
228	129	rprege0d 11259	. . . . 5 $/\$ $/\$
229		flge0nn0 11918	. . . . 5 $/\$
230		hashfz1 12383	. . . . 5
231	228, 229, 230	3syl 20	. . . 4 $/\$
232	227, 231	eqtr2d 2509	. . 3 $/\$
233	194, 195, 232	3brtr4d 4477	. 2 $/\$
234		simpr 461	. . . . 5 $/\$
235		nnnn0 10798	. . . . . . 7
236		fzctr 11780	. . . . . . 7
237		bccl2 12365	. . . . . . 7
238	235, 236, 237	3syl 20	. . . . . 6
239	238	adantr 465	. . . . 5 $/\$
240	234, 239	pccld 14229	. . . 4 $/\$
241	240	nn0zd 10960	. . 3 $/\$
242		efexple 23284	. . 3 $/\$ $/\$ $/\$
243	94, 99, 241, 105, 242	syl211anc 1234	. 2 $/\$
244	233, 243	mpbird 232	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369

wceq 1379

wcel 1767

wss 3476

cif 3939 class class class wbr 4447

cfv 5586 (class class class)co 6282

cfn 7513

cc 9486

cr 9487

cc0 9488

c1 9489

caddc 9491

cmul 9493

clt 9624

cle 9625

cmin 9801

cdiv 10202

cn 10532

c2 10581

cn0 10791

cz 10860

cuz 11078

crp 11216

cfz 11668

cfl 11891

cexp 12130

cbc 12344

chash 12369

csu 13467

ce 13655

cprime 14072

cpc 14215

clog 22670

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6574 ax-inf2 8054 ax-cnex 9544 ax-resscn 9545 ax-1cn 9546 ax-icn 9547 ax-addcl 9548 ax-addrcl 9549 ax-mulcl 9550 ax-mulrcl 9551 ax-mulcom 9552 ax-addass 9553 ax-mulass 9554 ax-distr 9555 ax-i2m1 9556 ax-1ne0 9557 ax-1rid 9558 ax-rnegex 9559 ax-rrecex 9560 ax-cnre 9561 ax-pre-lttri 9562 ax-pre-lttrn 9563 ax-pre-ltadd 9564 ax-pre-mulgt0 9565 ax-pre-sup 9566 ax-addf 9567 ax-mulf 9568

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-iin 4328 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5549 df-fun 5588 df-fn 5589 df-f 5590 df-f1 5591 df-fo 5592 df-f1o 5593 df-fv 5594 df-isom 5595 df-riota 6243 df-ov 6285 df-oprab 6286 df-mpt2 6287 df-of 6522 df-om 6679 df-1st 6781 df-2nd 6782 df-supp 6899 df-recs 7039 df-rdg 7073 df-1o 7127 df-2o 7128 df-oadd 7131 df-er 7308 df-map 7419 df-pm 7420 df-ixp 7467 df-en 7514 df-dom 7515 df-sdom 7516 df-fin 7517 df-fsupp 7826 df-fi 7867 df-sup 7897 df-oi 7931 df-card 8316 df-cda 8544 df-pnf 9626 df-mnf 9627 df-xr 9628 df-ltxr 9629 df-le 9630 df-sub 9803 df-neg 9804 df-div 10203 df-nn 10533 df-2 10590 df-3 10591 df-4 10592 df-5 10593 df-6 10594 df-7 10595 df-8 10596 df-9 10597 df-10 10598 df-n0 10792 df-z 10861 df-dec 10973 df-uz 11079 df-q 11179 df-rp 11217 df-xneg 11314 df-xadd 11315 df-xmul 11316 df-ioo 11529 df-ioc 11530 df-ico 11531 df-icc 11532 df-fz 11669 df-fzo 11789 df-fl 11893 df-mod 11961 df-seq 12072 df-exp 12131 df-fac 12318 df-bc 12345 df-hash 12370 df-shft 12859 df-cj 12891 df-re 12892 df-im 12893 df-sqrt 13027 df-abs 13028 df-limsup 13253 df-clim 13270 df-rlim 13271 df-sum 13468 df-ef 13661 df-sin 13663 df-cos 13664 df-pi 13666 df-dvds 13844 df-gcd 14000 df-prm 14073 df-pc 14216 df-struct 14488 df-ndx 14489 df-slot 14490 df-base 14491 df-sets 14492 df-ress 14493 df-plusg 14564 df-mulr 14565 df-starv 14566 df-sca 14567 df-vsca 14568 df-ip 14569 df-tset 14570 df-ple 14571 df-ds 14573 df-unif 14574 df-hom 14575 df-cco 14576 df-rest 14674 df-topn 14675 df-0g 14693 df-gsum 14694 df-topgen 14695 df-pt 14696 df-prds 14699 df-xrs 14753 df-qtop 14758 df-imas 14759 df-xps 14761 df-mre 14837 df-mrc 14838 df-acs 14840 df-mnd 15728 df-submnd 15778 df-mulg 15861 df-cntz 16150 df-cmn 16596 df-psmet 18182 df-xmet 18183 df-met 18184 df-bl 18185 df-mopn 18186 df-fbas 18187 df-fg 18188 df-cnfld 18192 df-top 19166 df-bases 19168 df-topon 19169 df-topsp 19170 df-cld 19286 df-ntr 19287 df-cls 19288 df-nei 19365 df-lp 19403 df-perf 19404 df-cn 19494 df-cnp 19495 df-haus 19582 df-tx 19798 df-hmeo 19991 df-fil 20082 df-fm 20174 df-flim 20175 df-flf 20176 df-xms 20558 df-ms 20559 df-tms 20560 df-cncf 21117 df-limc 22005 df-dv 22006 df-log 22672

This theorem is referenced by: bposlem5 23291 bposlem6 23292 chebbnd1lem1 23382

W3C validator