bposlem1 - Metamath Proof Explorer

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

Theorem bposlem1 22582

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 11791	. . . 4 $/\$
2		2nn 10475	. . . . . . . . . . 11
3		nnmulcl 10341	. . . . . . . . . . 11 $/\$
4	2, 3	mpan 665	. . . . . . . . . 10
5	4	ad2antrr 720	. . . . . . . . 9 $/\$ $/\$
6		prmnn 13762	. . . . . . . . . . 11
7	6	ad2antlr 721	. . . . . . . . . 10 $/\$ $/\$
8		elfznn 11474	. . . . . . . . . . . 12
9	8	adantl 463	. . . . . . . . . . 11 $/\$ $/\$
10	9	nnnn0d 10632	. . . . . . . . . 10 $/\$ $/\$
11	7, 10	nnexpcld 12025	. . . . . . . . 9 $/\$ $/\$
12		nnrp 10996	. . . . . . . . . 10
13		nnrp 10996	. . . . . . . . . 10
14		rpdivcl 11009	. . . . . . . . . 10 $/\$
15	12, 13, 14	syl2an 474	. . . . . . . . 9 $/\$
16	5, 11, 15	syl2anc 656	. . . . . . . 8 $/\$ $/\$
17	16	rpred 11023	. . . . . . 7 $/\$ $/\$
18	17	flcld 11644	. . . . . 6 $/\$ $/\$
19		2z 10674	. . . . . . 7
20		simpll 748	. . . . . . . . . 10 $/\$ $/\$
21		nnrp 10996	. . . . . . . . . . 11
22		rpdivcl 11009	. . . . . . . . . . 11 $/\$
23	21, 13, 22	syl2an 474	. . . . . . . . . 10 $/\$
24	20, 11, 23	syl2anc 656	. . . . . . . . 9 $/\$ $/\$
25	24	rpred 11023	. . . . . . . 8 $/\$ $/\$
26	25	flcld 11644	. . . . . . 7 $/\$ $/\$
27		zmulcl 10689	. . . . . . 7 $/\$
28	19, 26, 27	sylancr 658	. . . . . 6 $/\$ $/\$
29	18, 28	zsubcld 10748	. . . . 5 $/\$ $/\$
30	29	zred 10743	. . . 4 $/\$ $/\$
31		1re 9381	. . . . . 6
32		0re 9382	. . . . . 6
33	31, 32	keepel 3854	. . . . 5
34	33	a1i 11	. . . 4 $/\$ $/\$
35	28	zred 10743	. . . . . . . . . 10 $/\$ $/\$
36	17, 35	resubcld 9772	. . . . . . . . 9 $/\$ $/\$
37		2re 10387	. . . . . . . . . 10
38	37	a1i 11	. . . . . . . . 9 $/\$ $/\$
39	18	zred 10743	. . . . . . . . . 10 $/\$ $/\$
40		flle 11645	. . . . . . . . . . 11
41	17, 40	syl 16	. . . . . . . . . 10 $/\$ $/\$
42	39, 17, 35, 41	lesub1dd 9951	. . . . . . . . 9 $/\$ $/\$
43		resubcl 9669	. . . . . . . . . . . . 13 $/\$
44	25, 31, 43	sylancl 657	. . . . . . . . . . . 12 $/\$ $/\$
45		remulcl 9363	. . . . . . . . . . . 12 $/\$
46	37, 44, 45	sylancr 658	. . . . . . . . . . 11 $/\$ $/\$
47		flltp1 11646	. . . . . . . . . . . . . 14
48	25, 47	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$
49		1red 9397	. . . . . . . . . . . . . 14 $/\$ $/\$
50	26	zred 10743	. . . . . . . . . . . . . 14 $/\$ $/\$
51	25, 49, 50	ltsubaddd 9931	. . . . . . . . . . . . 13 $/\$ $/\$
52	48, 51	mpbird 232	. . . . . . . . . . . 12 $/\$ $/\$
53		2pos 10409	. . . . . . . . . . . . . . 15
54	37, 53	pm3.2i 452	. . . . . . . . . . . . . 14 $/\$
55		ltmul2 10176	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
56	54, 55	mp3an3 1298	. . . . . . . . . . . . 13 $/\$
57	44, 50, 56	syl2anc 656	. . . . . . . . . . . 12 $/\$ $/\$
58	52, 57	mpbid 210	. . . . . . . . . . 11 $/\$ $/\$
59	46, 35, 17, 58	ltsub2dd 9948	. . . . . . . . . 10 $/\$ $/\$
60		2cnd 10390	. . . . . . . . . . . . 13 $/\$ $/\$
61		nncn 10326	. . . . . . . . . . . . . 14
62	61	ad2antrr 720	. . . . . . . . . . . . 13 $/\$ $/\$
63	11	nncnd 10334	. . . . . . . . . . . . 13 $/\$ $/\$
64	11	nnne0d 10362	. . . . . . . . . . . . 13 $/\$ $/\$
65	60, 62, 63, 64	divassd 10138	. . . . . . . . . . . 12 $/\$ $/\$
66	25	recnd 9408	. . . . . . . . . . . . . 14 $/\$ $/\$
67		1cnd 9398	. . . . . . . . . . . . . 14 $/\$ $/\$
68	60, 66, 67	subdid 9796	. . . . . . . . . . . . 13 $/\$ $/\$
69		2t1e2 10466	. . . . . . . . . . . . . 14
70	69	oveq2i 6101	. . . . . . . . . . . . 13
71	68, 70	syl6eq 2489	. . . . . . . . . . . 12 $/\$ $/\$
72	65, 71	oveq12d 6108	. . . . . . . . . . 11 $/\$ $/\$
73		remulcl 9363	. . . . . . . . . . . . . 14 $/\$
74	37, 25, 73	sylancr 658	. . . . . . . . . . . . 13 $/\$ $/\$
75	74	recnd 9408	. . . . . . . . . . . 12 $/\$ $/\$
76		2cn 10388	. . . . . . . . . . . 12
77		nncan 9634	. . . . . . . . . . . 12 $/\$
78	75, 76, 77	sylancl 657	. . . . . . . . . . 11 $/\$ $/\$
79	72, 78	eqtrd 2473	. . . . . . . . . 10 $/\$ $/\$
80	59, 79	breqtrd 4313	. . . . . . . . 9 $/\$ $/\$
81	30, 36, 38, 42, 80	lelttrd 9525	. . . . . . . 8 $/\$ $/\$
82		df-2 10376	. . . . . . . 8
83	81, 82	syl6breq 4328	. . . . . . 7 $/\$ $/\$
84		1z 10672	. . . . . . . 8
85		zleltp1 10691	. . . . . . . 8 $/\$
86	29, 84, 85	sylancl 657	. . . . . . 7 $/\$ $/\$
87	83, 86	mpbird 232	. . . . . 6 $/\$ $/\$
88		iftrue 3794	. . . . . . 7
89	88	breq2d 4301	. . . . . 6
90	87, 89	syl5ibrcom 222	. . . . 5 $/\$ $/\$
91	9	nnge1d 10360	. . . . . . . . . . 11 $/\$ $/\$
92	91	biantrurd 505	. . . . . . . . . 10 $/\$ $/\$ $/\$
93	6	adantl 463	. . . . . . . . . . . . . 14 $/\$
94	93	nnred 10333	. . . . . . . . . . . . 13 $/\$
95		prmuz2 13777	. . . . . . . . . . . . . . 15
96	95	adantl 463	. . . . . . . . . . . . . 14 $/\$
97		eluz2b1 10922	. . . . . . . . . . . . . . 15 $/\$
98	97	simprbi 461	. . . . . . . . . . . . . 14
99	96, 98	syl 16	. . . . . . . . . . . . 13 $/\$
100	94, 99	jca 529	. . . . . . . . . . . 12 $/\$ $/\$
101	100	adantr 462	. . . . . . . . . . 11 $/\$ $/\$ $/\$
102		elfzelz 11449	. . . . . . . . . . . 12
103	102	adantl 463	. . . . . . . . . . 11 $/\$ $/\$
104	4	adantr 462	. . . . . . . . . . . . 13 $/\$
105	104	nnrpd 11022	. . . . . . . . . . . 12 $/\$
106	105	adantr 462	. . . . . . . . . . 11 $/\$ $/\$
107		efexple 22579	. . . . . . . . . . 11 $/\$ $/\$ $/\$
108	101, 103, 106, 107	syl3anc 1213	. . . . . . . . . 10 $/\$ $/\$
109	9	nnzd 10742	. . . . . . . . . . 11 $/\$ $/\$
110	84	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
111	104	nnred 10333	. . . . . . . . . . . . . . . 16 $/\$
112		1red 9397	. . . . . . . . . . . . . . . . 17 $/\$
113	37	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
114		1lt2 10484	. . . . . . . . . . . . . . . . . 18
115	114	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
116		nnre 10325	. . . . . . . . . . . . . . . . . . . 20
117	116	adantr 462	. . . . . . . . . . . . . . . . . . 19 $/\$
118		0le2 10408	. . . . . . . . . . . . . . . . . . . . 21
119	37, 118	pm3.2i 452	. . . . . . . . . . . . . . . . . . . 20 $/\$
120	119	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
121		nnge1 10344	. . . . . . . . . . . . . . . . . . . 20
122	121	adantr 462	. . . . . . . . . . . . . . . . . . 19 $/\$
123		lemul2a 10180	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
124	112, 117, 120, 122, 123	syl31anc 1216	. . . . . . . . . . . . . . . . . 18 $/\$
125	69, 124	syl5eqbrr 4323	. . . . . . . . . . . . . . . . 17 $/\$
126	112, 113, 111, 115, 125	ltletrd 9527	. . . . . . . . . . . . . . . 16 $/\$
127	111, 126	rplogcld 22037	. . . . . . . . . . . . . . 15 $/\$
128	94, 99	rplogcld 22037	. . . . . . . . . . . . . . 15 $/\$
129	127, 128	rpdivcld 11040	. . . . . . . . . . . . . 14 $/\$
130	129	rpred 11023	. . . . . . . . . . . . 13 $/\$
131	130	flcld 11644	. . . . . . . . . . . 12 $/\$
132	131	adantr 462	. . . . . . . . . . 11 $/\$ $/\$
133		elfz 11439	. . . . . . . . . . 11 $/\$ $/\$ $/\$
134	109, 110, 132, 133	syl3anc 1213	. . . . . . . . . 10 $/\$ $/\$ $/\$
135	92, 108, 134	3bitr4rd 286	. . . . . . . . 9 $/\$ $/\$
136	135	notbid 294	. . . . . . . 8 $/\$ $/\$
137	111	adantr 462	. . . . . . . . 9 $/\$ $/\$
138	11	nnred 10333	. . . . . . . . 9 $/\$ $/\$
139	137, 138	ltnled 9517	. . . . . . . 8 $/\$ $/\$
140	136, 139	bitr4d 256	. . . . . . 7 $/\$ $/\$
141	16	rpge0d 11027	. . . . . . . . . . . . 13 $/\$ $/\$
142	141	adantrr 711	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
143	11	nngt0d 10361	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
144		ltdivmul 10200	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
145	137, 49, 138, 143, 144	syl112anc 1217	. . . . . . . . . . . . . . . 16 $/\$ $/\$
146	63	mulid1d 9399	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
147	146	breq2d 4301	. . . . . . . . . . . . . . . 16 $/\$ $/\$
148	145, 147	bitrd 253	. . . . . . . . . . . . . . 15 $/\$ $/\$
149	148	biimprd 223	. . . . . . . . . . . . . 14 $/\$ $/\$
150	149	impr 616	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
151		0p1e1 10429	. . . . . . . . . . . . 13
152	150, 151	syl6breqr 4329	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
153	17	adantrr 711	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
154		0z 10653	. . . . . . . . . . . . 13
155		flbi 11660	. . . . . . . . . . . . 13 $/\$ $/\$
156	153, 154, 155	sylancl 657	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
157	142, 152, 156	mpbir2and 908	. . . . . . . . . . 11 $/\$ $/\$ $/\$
158	24	rpge0d 11027	. . . . . . . . . . . . . . 15 $/\$ $/\$
159	158	adantrr 711	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
160	116, 21	ltaddrp2d 11053	. . . . . . . . . . . . . . . . . . . 20
161	61	2timesd 10563	. . . . . . . . . . . . . . . . . . . 20
162	160, 161	breqtrrd 4315	. . . . . . . . . . . . . . . . . . 19
163	162	ad2antrr 720	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
164	116	ad2antrr 720	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
165		lttr 9447	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
166	164, 137, 138, 165	syl3anc 1213	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
167	163, 166	mpand 670	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
168		ltdivmul 10200	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
169	164, 49, 138, 143, 168	syl112anc 1217	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
170	146	breq2d 4301	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
171	169, 170	bitrd 253	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
172	167, 171	sylibrd 234	. . . . . . . . . . . . . . . 16 $/\$ $/\$
173	172	impr 616	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
174	173, 151	syl6breqr 4329	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
175	25	adantrr 711	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
176		flbi 11660	. . . . . . . . . . . . . . 15 $/\$ $/\$
177	175, 154, 176	sylancl 657	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
178	159, 174, 177	mpbir2and 908	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
179	178	oveq2d 6106	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
180		2t0e0 10473	. . . . . . . . . . . 12
181	179, 180	syl6eq 2489	. . . . . . . . . . 11 $/\$ $/\$ $/\$
182	157, 181	oveq12d 6108	. . . . . . . . . 10 $/\$ $/\$ $/\$
183		0m0e0 10427	. . . . . . . . . 10
184	182, 183	syl6eq 2489	. . . . . . . . 9 $/\$ $/\$ $/\$
185		0le0 10407	. . . . . . . . 9
186	184, 185	syl6eqbr 4326	. . . . . . . 8 $/\$ $/\$ $/\$
187	186	expr 612	. . . . . . 7 $/\$ $/\$
188	140, 187	sylbid 215	. . . . . 6 $/\$ $/\$
189		iffalse 3796	. . . . . . . 8
190	189	eqcomd 2446	. . . . . . 7
191	190	breq2d 4301	. . . . . 6
192	188, 191	mpbidi 216	. . . . 5 $/\$ $/\$
193	90, 192	pm2.61d 158	. . . 4 $/\$ $/\$
194	1, 30, 34, 193	fsumle 13258	. . 3 $/\$
195		pcbcctr 22574	. . 3 $/\$
196	131	zred 10743	. . . . . . . 8 $/\$
197		flle 11645	. . . . . . . . 9
198	130, 197	syl 16	. . . . . . . 8 $/\$
199	104	nnnn0d 10632	. . . . . . . . . . . . . 14 $/\$
200	93, 199	nnexpcld 12025	. . . . . . . . . . . . 13 $/\$
201	200	nnred 10333	. . . . . . . . . . . 12 $/\$
202		bernneq3 11988	. . . . . . . . . . . . 13 $/\$
203	96, 199, 202	syl2anc 656	. . . . . . . . . . . 12 $/\$
204	111, 201, 203	ltled 9518	. . . . . . . . . . 11 $/\$
205	105	reeflogd 22032	. . . . . . . . . . 11 $/\$
206	93	nnrpd 11022	. . . . . . . . . . . . 13 $/\$
207	104	nnzd 10742	. . . . . . . . . . . . 13 $/\$
208		reexplog 22002	. . . . . . . . . . . . 13 $/\$
209	206, 207, 208	syl2anc 656	. . . . . . . . . . . 12 $/\$
210	209	eqcomd 2446	. . . . . . . . . . 11 $/\$
211	204, 205, 210	3brtr4d 4319	. . . . . . . . . 10 $/\$
212	105	relogcld 22031	. . . . . . . . . . 11 $/\$
213	128	rpred 11023	. . . . . . . . . . . 12 $/\$
214	111, 213	remulcld 9410	. . . . . . . . . . 11 $/\$
215		efle 13398	. . . . . . . . . . 11 $/\$
216	212, 214, 215	syl2anc 656	. . . . . . . . . 10 $/\$
217	211, 216	mpbird 232	. . . . . . . . 9 $/\$
218	212, 111, 128	ledivmul2d 11073	. . . . . . . . 9 $/\$
219	217, 218	mpbird 232	. . . . . . . 8 $/\$
220	196, 130, 111, 198, 219	letrd 9524	. . . . . . 7 $/\$
221		eluz 10870	. . . . . . . 8 $/\$
222	131, 207, 221	syl2anc 656	. . . . . . 7 $/\$
223	220, 222	mpbird 232	. . . . . 6 $/\$
224		fzss2 11494	. . . . . 6
225	223, 224	syl 16	. . . . 5 $/\$
226		sumhash 13954	. . . . 5 $/\$
227	1, 225, 226	syl2anc 656	. . . 4 $/\$
228	129	rprege0d 11030	. . . . 5 $/\$ $/\$
229		flge0nn0 11662	. . . . 5 $/\$
230		hashfz1 12113	. . . . 5
231	228, 229, 230	3syl 20	. . . 4 $/\$
232	227, 231	eqtr2d 2474	. . 3 $/\$
233	194, 195, 232	3brtr4d 4319	. 2 $/\$
234		simpr 458	. . . . 5 $/\$
235		nnnn0 10582	. . . . . . 7
236		fzctr 11525	. . . . . . 7
237		bccl2 12095	. . . . . . 7
238	235, 236, 237	3syl 20	. . . . . 6
239	238	adantr 462	. . . . 5 $/\$
240	234, 239	pccld 13913	. . . 4 $/\$
241	240	nn0zd 10741	. . 3 $/\$
242		efexple 22579	. . 3 $/\$ $/\$ $/\$
243	94, 99, 241, 105, 242	syl211anc 1219	. 2 $/\$
244	233, 243	mpbird 232	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369

wceq 1364

wcel 1761

wss 3325

cif 3788 class class class wbr 4289

cfv 5415 (class class class)co 6090

cfn 7306

cc 9276

cr 9277

cc0 9278

c1 9279

caddc 9281

cmul 9283

clt 9414

cle 9415

cmin 9591

cdiv 9989

cn 10318

c2 10367

cn0 10575

cz 10642

cuz 10857

crp 10987

cfz 11433

cfl 11636

cexp 11861

cbc 12074

chash 12099

csu 13159

ce 13343

cprime 13759

cpc 13899

clog 21965

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-8 1763 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-rep 4400 ax-sep 4410 ax-nul 4418 ax-pow 4467 ax-pr 4528 ax-un 6371 ax-inf2 7843 ax-cnex 9334 ax-resscn 9335 ax-1cn 9336 ax-icn 9337 ax-addcl 9338 ax-addrcl 9339 ax-mulcl 9340 ax-mulrcl 9341 ax-mulcom 9342 ax-addass 9343 ax-mulass 9344 ax-distr 9345 ax-i2m1 9346 ax-1ne0 9347 ax-1rid 9348 ax-rnegex 9349 ax-rrecex 9350 ax-cnre 9351 ax-pre-lttri 9352 ax-pre-lttrn 9353 ax-pre-ltadd 9354 ax-pre-mulgt0 9355 ax-pre-sup 9356 ax-addf 9357 ax-mulf 9358

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 961 df-3an 962 df-tru 1367 df-fal 1370 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2261 df-mo 2262 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-nel 2607 df-ral 2718 df-rex 2719 df-reu 2720 df-rmo 2721 df-rab 2722 df-v 2972 df-sbc 3184 df-csb 3286 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-pss 3341 df-nul 3635 df-if 3789 df-pw 3859 df-sn 3875 df-pr 3877 df-tp 3879 df-op 3881 df-uni 4089 df-int 4126 df-iun 4170 df-iin 4171 df-br 4290 df-opab 4348 df-mpt 4349 df-tr 4383 df-eprel 4628 df-id 4632 df-po 4637 df-so 4638 df-fr 4675 df-se 4676 df-we 4677 df-ord 4718 df-on 4719 df-lim 4720 df-suc 4721 df-xp 4842 df-rel 4843 df-cnv 4844 df-co 4845 df-dm 4846 df-rn 4847 df-res 4848 df-ima 4849 df-iota 5378 df-fun 5417 df-fn 5418 df-f 5419 df-f1 5420 df-fo 5421 df-f1o 5422 df-fv 5423 df-isom 5424 df-riota 6049 df-ov 6093 df-oprab 6094 df-mpt2 6095 df-of 6319 df-om 6476 df-1st 6576 df-2nd 6577 df-supp 6690 df-recs 6828 df-rdg 6862 df-1o 6916 df-2o 6917 df-oadd 6920 df-er 7097 df-map 7212 df-pm 7213 df-ixp 7260 df-en 7307 df-dom 7308 df-sdom 7309 df-fin 7310 df-fsupp 7617 df-fi 7657 df-sup 7687 df-oi 7720 df-card 8105 df-cda 8333 df-pnf 9416 df-mnf 9417 df-xr 9418 df-ltxr 9419 df-le 9420 df-sub 9593 df-neg 9594 df-div 9990 df-nn 10319 df-2 10376 df-3 10377 df-4 10378 df-5 10379 df-6 10380 df-7 10381 df-8 10382 df-9 10383 df-10 10384 df-n0 10576 df-z 10643 df-dec 10752 df-uz 10858 df-q 10950 df-rp 10988 df-xneg 11085 df-xadd 11086 df-xmul 11087 df-ioo 11300 df-ioc 11301 df-ico 11302 df-icc 11303 df-fz 11434 df-fzo 11545 df-fl 11638 df-mod 11705 df-seq 11803 df-exp 11862 df-fac 12048 df-bc 12075 df-hash 12100 df-shft 12552 df-cj 12584 df-re 12585 df-im 12586 df-sqr 12720 df-abs 12721 df-limsup 12945 df-clim 12962 df-rlim 12963 df-sum 13160 df-ef 13349 df-sin 13351 df-cos 13352 df-pi 13354 df-dvds 13532 df-gcd 13687 df-prm 13760 df-pc 13900 df-struct 14172 df-ndx 14173 df-slot 14174 df-base 14175 df-sets 14176 df-ress 14177 df-plusg 14247 df-mulr 14248 df-starv 14249 df-sca 14250 df-vsca 14251 df-ip 14252 df-tset 14253 df-ple 14254 df-ds 14256 df-unif 14257 df-hom 14258 df-cco 14259 df-rest 14357 df-topn 14358 df-0g 14376 df-gsum 14377 df-topgen 14378 df-pt 14379 df-prds 14382 df-xrs 14436 df-qtop 14441 df-imas 14442 df-xps 14444 df-mre 14520 df-mrc 14521 df-acs 14523 df-mnd 15411 df-submnd 15461 df-mulg 15541 df-cntz 15828 df-cmn 16272 df-psmet 17768 df-xmet 17769 df-met 17770 df-bl 17771 df-mopn 17772 df-fbas 17773 df-fg 17774 df-cnfld 17778 df-top 18462 df-bases 18464 df-topon 18465 df-topsp 18466 df-cld 18582 df-ntr 18583 df-cls 18584 df-nei 18661 df-lp 18699 df-perf 18700 df-cn 18790 df-cnp 18791 df-haus 18878 df-tx 19094 df-hmeo 19287 df-fil 19378 df-fm 19470 df-flim 19471 df-flf 19472 df-xms 19854 df-ms 19855 df-tms 19856 df-cncf 20413 df-limc 21300 df-dv 21301 df-log 21967

This theorem is referenced by: bposlem5 22586 bposlem6 22587 chebbnd1lem1 22677

W3C validator