bposlem1 - Metamath Proof Explorer

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

Theorem bposlem1 22628

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 11800	. . . 4 $/\$
2		2nn 10484	. . . . . . . . . . 11
3		nnmulcl 10350	. . . . . . . . . . 11 $/\$
4	2, 3	mpan 670	. . . . . . . . . 10
5	4	ad2antrr 725	. . . . . . . . 9 $/\$ $/\$
6		prmnn 13771	. . . . . . . . . . 11
7	6	ad2antlr 726	. . . . . . . . . 10 $/\$ $/\$
8		elfznn 11483	. . . . . . . . . . . 12
9	8	adantl 466	. . . . . . . . . . 11 $/\$ $/\$
10	9	nnnn0d 10641	. . . . . . . . . 10 $/\$ $/\$
11	7, 10	nnexpcld 12034	. . . . . . . . 9 $/\$ $/\$
12		nnrp 11005	. . . . . . . . . 10
13		nnrp 11005	. . . . . . . . . 10
14		rpdivcl 11018	. . . . . . . . . 10 $/\$
15	12, 13, 14	syl2an 477	. . . . . . . . 9 $/\$
16	5, 11, 15	syl2anc 661	. . . . . . . 8 $/\$ $/\$
17	16	rpred 11032	. . . . . . 7 $/\$ $/\$
18	17	flcld 11653	. . . . . 6 $/\$ $/\$
19		2z 10683	. . . . . . 7
20		simpll 753	. . . . . . . . . 10 $/\$ $/\$
21		nnrp 11005	. . . . . . . . . . 11
22		rpdivcl 11018	. . . . . . . . . . 11 $/\$
23	21, 13, 22	syl2an 477	. . . . . . . . . 10 $/\$
24	20, 11, 23	syl2anc 661	. . . . . . . . 9 $/\$ $/\$
25	24	rpred 11032	. . . . . . . 8 $/\$ $/\$
26	25	flcld 11653	. . . . . . 7 $/\$ $/\$
27		zmulcl 10698	. . . . . . 7 $/\$
28	19, 26, 27	sylancr 663	. . . . . 6 $/\$ $/\$
29	18, 28	zsubcld 10757	. . . . 5 $/\$ $/\$
30	29	zred 10752	. . . 4 $/\$ $/\$
31		1re 9390	. . . . . 6
32		0re 9391	. . . . . 6
33	31, 32	keepel 3862	. . . . 5
34	33	a1i 11	. . . 4 $/\$ $/\$
35	28	zred 10752	. . . . . . . . . 10 $/\$ $/\$
36	17, 35	resubcld 9781	. . . . . . . . 9 $/\$ $/\$
37		2re 10396	. . . . . . . . . 10
38	37	a1i 11	. . . . . . . . 9 $/\$ $/\$
39	18	zred 10752	. . . . . . . . . 10 $/\$ $/\$
40		flle 11654	. . . . . . . . . . 11
41	17, 40	syl 16	. . . . . . . . . 10 $/\$ $/\$
42	39, 17, 35, 41	lesub1dd 9960	. . . . . . . . 9 $/\$ $/\$
43		resubcl 9678	. . . . . . . . . . . . 13 $/\$
44	25, 31, 43	sylancl 662	. . . . . . . . . . . 12 $/\$ $/\$
45		remulcl 9372	. . . . . . . . . . . 12 $/\$
46	37, 44, 45	sylancr 663	. . . . . . . . . . 11 $/\$ $/\$
47		flltp1 11655	. . . . . . . . . . . . . 14
48	25, 47	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$
49		1red 9406	. . . . . . . . . . . . . 14 $/\$ $/\$
50	26	zred 10752	. . . . . . . . . . . . . 14 $/\$ $/\$
51	25, 49, 50	ltsubaddd 9940	. . . . . . . . . . . . 13 $/\$ $/\$
52	48, 51	mpbird 232	. . . . . . . . . . . 12 $/\$ $/\$
53		2pos 10418	. . . . . . . . . . . . . . 15
54	37, 53	pm3.2i 455	. . . . . . . . . . . . . 14 $/\$
55		ltmul2 10185	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
56	54, 55	mp3an3 1303	. . . . . . . . . . . . 13 $/\$
57	44, 50, 56	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$
58	52, 57	mpbid 210	. . . . . . . . . . 11 $/\$ $/\$
59	46, 35, 17, 58	ltsub2dd 9957	. . . . . . . . . 10 $/\$ $/\$
60		2cnd 10399	. . . . . . . . . . . . 13 $/\$ $/\$
61		nncn 10335	. . . . . . . . . . . . . 14
62	61	ad2antrr 725	. . . . . . . . . . . . 13 $/\$ $/\$
63	11	nncnd 10343	. . . . . . . . . . . . 13 $/\$ $/\$
64	11	nnne0d 10371	. . . . . . . . . . . . 13 $/\$ $/\$
65	60, 62, 63, 64	divassd 10147	. . . . . . . . . . . 12 $/\$ $/\$
66	25	recnd 9417	. . . . . . . . . . . . . 14 $/\$ $/\$
67		1cnd 9407	. . . . . . . . . . . . . 14 $/\$ $/\$
68	60, 66, 67	subdid 9805	. . . . . . . . . . . . 13 $/\$ $/\$
69		2t1e2 10475	. . . . . . . . . . . . . 14
70	69	oveq2i 6107	. . . . . . . . . . . . 13
71	68, 70	syl6eq 2491	. . . . . . . . . . . 12 $/\$ $/\$
72	65, 71	oveq12d 6114	. . . . . . . . . . 11 $/\$ $/\$
73		remulcl 9372	. . . . . . . . . . . . . 14 $/\$
74	37, 25, 73	sylancr 663	. . . . . . . . . . . . 13 $/\$ $/\$
75	74	recnd 9417	. . . . . . . . . . . 12 $/\$ $/\$
76		2cn 10397	. . . . . . . . . . . 12
77		nncan 9643	. . . . . . . . . . . 12 $/\$
78	75, 76, 77	sylancl 662	. . . . . . . . . . 11 $/\$ $/\$
79	72, 78	eqtrd 2475	. . . . . . . . . 10 $/\$ $/\$
80	59, 79	breqtrd 4321	. . . . . . . . 9 $/\$ $/\$
81	30, 36, 38, 42, 80	lelttrd 9534	. . . . . . . 8 $/\$ $/\$
82		df-2 10385	. . . . . . . 8
83	81, 82	syl6breq 4336	. . . . . . 7 $/\$ $/\$
84		1z 10681	. . . . . . . 8
85		zleltp1 10700	. . . . . . . 8 $/\$
86	29, 84, 85	sylancl 662	. . . . . . 7 $/\$ $/\$
87	83, 86	mpbird 232	. . . . . 6 $/\$ $/\$
88		iftrue 3802	. . . . . . 7
89	88	breq2d 4309	. . . . . 6
90	87, 89	syl5ibrcom 222	. . . . 5 $/\$ $/\$
91	9	nnge1d 10369	. . . . . . . . . . 11 $/\$ $/\$
92	91	biantrurd 508	. . . . . . . . . 10 $/\$ $/\$ $/\$
93	6	adantl 466	. . . . . . . . . . . . . 14 $/\$
94	93	nnred 10342	. . . . . . . . . . . . 13 $/\$
95		prmuz2 13786	. . . . . . . . . . . . . . 15
96	95	adantl 466	. . . . . . . . . . . . . 14 $/\$
97		eluz2b1 10931	. . . . . . . . . . . . . . 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 11458	. . . . . . . . . . . 12
103	102	adantl 466	. . . . . . . . . . 11 $/\$ $/\$
104	4	adantr 465	. . . . . . . . . . . . 13 $/\$
105	104	nnrpd 11031	. . . . . . . . . . . 12 $/\$
106	105	adantr 465	. . . . . . . . . . 11 $/\$ $/\$
107		efexple 22625	. . . . . . . . . . 11 $/\$ $/\$ $/\$
108	101, 103, 106, 107	syl3anc 1218	. . . . . . . . . 10 $/\$ $/\$
109	9	nnzd 10751	. . . . . . . . . . 11 $/\$ $/\$
110	84	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
111	104	nnred 10342	. . . . . . . . . . . . . . . 16 $/\$
112		1red 9406	. . . . . . . . . . . . . . . . 17 $/\$
113	37	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
114		1lt2 10493	. . . . . . . . . . . . . . . . . 18
115	114	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
116		nnre 10334	. . . . . . . . . . . . . . . . . . . 20
117	116	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
118		0le2 10417	. . . . . . . . . . . . . . . . . . . . 21
119	37, 118	pm3.2i 455	. . . . . . . . . . . . . . . . . . . 20 $/\$
120	119	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
121		nnge1 10353	. . . . . . . . . . . . . . . . . . . 20
122	121	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
123		lemul2a 10189	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
124	112, 117, 120, 122, 123	syl31anc 1221	. . . . . . . . . . . . . . . . . 18 $/\$
125	69, 124	syl5eqbrr 4331	. . . . . . . . . . . . . . . . 17 $/\$
126	112, 113, 111, 115, 125	ltletrd 9536	. . . . . . . . . . . . . . . 16 $/\$
127	111, 126	rplogcld 22083	. . . . . . . . . . . . . . 15 $/\$
128	94, 99	rplogcld 22083	. . . . . . . . . . . . . . 15 $/\$
129	127, 128	rpdivcld 11049	. . . . . . . . . . . . . 14 $/\$
130	129	rpred 11032	. . . . . . . . . . . . 13 $/\$
131	130	flcld 11653	. . . . . . . . . . . 12 $/\$
132	131	adantr 465	. . . . . . . . . . 11 $/\$ $/\$
133		elfz 11448	. . . . . . . . . . 11 $/\$ $/\$ $/\$
134	109, 110, 132, 133	syl3anc 1218	. . . . . . . . . 10 $/\$ $/\$ $/\$
135	92, 108, 134	3bitr4rd 286	. . . . . . . . 9 $/\$ $/\$
136	135	notbid 294	. . . . . . . 8 $/\$ $/\$
137	111	adantr 465	. . . . . . . . 9 $/\$ $/\$
138	11	nnred 10342	. . . . . . . . 9 $/\$ $/\$
139	137, 138	ltnled 9526	. . . . . . . 8 $/\$ $/\$
140	136, 139	bitr4d 256	. . . . . . 7 $/\$ $/\$
141	16	rpge0d 11036	. . . . . . . . . . . . 13 $/\$ $/\$
142	141	adantrr 716	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
143	11	nngt0d 10370	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
144		ltdivmul 10209	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
145	137, 49, 138, 143, 144	syl112anc 1222	. . . . . . . . . . . . . . . 16 $/\$ $/\$
146	63	mulid1d 9408	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
147	146	breq2d 4309	. . . . . . . . . . . . . . . 16 $/\$ $/\$
148	145, 147	bitrd 253	. . . . . . . . . . . . . . 15 $/\$ $/\$
149	148	biimprd 223	. . . . . . . . . . . . . 14 $/\$ $/\$
150	149	impr 619	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
151		0p1e1 10438	. . . . . . . . . . . . 13
152	150, 151	syl6breqr 4337	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
153	17	adantrr 716	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
154		0z 10662	. . . . . . . . . . . . 13
155		flbi 11669	. . . . . . . . . . . . 13 $/\$ $/\$
156	153, 154, 155	sylancl 662	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
157	142, 152, 156	mpbir2and 913	. . . . . . . . . . 11 $/\$ $/\$ $/\$
158	24	rpge0d 11036	. . . . . . . . . . . . . . 15 $/\$ $/\$
159	158	adantrr 716	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
160	116, 21	ltaddrp2d 11062	. . . . . . . . . . . . . . . . . . . 20
161	61	2timesd 10572	. . . . . . . . . . . . . . . . . . . 20
162	160, 161	breqtrrd 4323	. . . . . . . . . . . . . . . . . . 19
163	162	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
164	116	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
165		lttr 9456	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
166	164, 137, 138, 165	syl3anc 1218	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
167	163, 166	mpand 675	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
168		ltdivmul 10209	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
169	164, 49, 138, 143, 168	syl112anc 1222	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
170	146	breq2d 4309	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
171	169, 170	bitrd 253	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
172	167, 171	sylibrd 234	. . . . . . . . . . . . . . . 16 $/\$ $/\$
173	172	impr 619	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
174	173, 151	syl6breqr 4337	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
175	25	adantrr 716	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
176		flbi 11669	. . . . . . . . . . . . . . 15 $/\$ $/\$
177	175, 154, 176	sylancl 662	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
178	159, 174, 177	mpbir2and 913	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
179	178	oveq2d 6112	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
180		2t0e0 10482	. . . . . . . . . . . 12
181	179, 180	syl6eq 2491	. . . . . . . . . . 11 $/\$ $/\$ $/\$
182	157, 181	oveq12d 6114	. . . . . . . . . 10 $/\$ $/\$ $/\$
183		0m0e0 10436	. . . . . . . . . 10
184	182, 183	syl6eq 2491	. . . . . . . . 9 $/\$ $/\$ $/\$
185		0le0 10416	. . . . . . . . 9
186	184, 185	syl6eqbr 4334	. . . . . . . 8 $/\$ $/\$ $/\$
187	186	expr 615	. . . . . . 7 $/\$ $/\$
188	140, 187	sylbid 215	. . . . . 6 $/\$ $/\$
189		iffalse 3804	. . . . . . . 8
190	189	eqcomd 2448	. . . . . . 7
191	190	breq2d 4309	. . . . . 6
192	188, 191	mpbidi 216	. . . . 5 $/\$ $/\$
193	90, 192	pm2.61d 158	. . . 4 $/\$ $/\$
194	1, 30, 34, 193	fsumle 13267	. . 3 $/\$
195		pcbcctr 22620	. . 3 $/\$
196	131	zred 10752	. . . . . . . 8 $/\$
197		flle 11654	. . . . . . . . 9
198	130, 197	syl 16	. . . . . . . 8 $/\$
199	104	nnnn0d 10641	. . . . . . . . . . . . . 14 $/\$
200	93, 199	nnexpcld 12034	. . . . . . . . . . . . 13 $/\$
201	200	nnred 10342	. . . . . . . . . . . 12 $/\$
202		bernneq3 11997	. . . . . . . . . . . . 13 $/\$
203	96, 199, 202	syl2anc 661	. . . . . . . . . . . 12 $/\$
204	111, 201, 203	ltled 9527	. . . . . . . . . . 11 $/\$
205	105	reeflogd 22078	. . . . . . . . . . 11 $/\$
206	93	nnrpd 11031	. . . . . . . . . . . . 13 $/\$
207	104	nnzd 10751	. . . . . . . . . . . . 13 $/\$
208		reexplog 22048	. . . . . . . . . . . . 13 $/\$
209	206, 207, 208	syl2anc 661	. . . . . . . . . . . 12 $/\$
210	209	eqcomd 2448	. . . . . . . . . . 11 $/\$
211	204, 205, 210	3brtr4d 4327	. . . . . . . . . 10 $/\$
212	105	relogcld 22077	. . . . . . . . . . 11 $/\$
213	128	rpred 11032	. . . . . . . . . . . 12 $/\$
214	111, 213	remulcld 9419	. . . . . . . . . . 11 $/\$
215		efle 13407	. . . . . . . . . . 11 $/\$
216	212, 214, 215	syl2anc 661	. . . . . . . . . 10 $/\$
217	211, 216	mpbird 232	. . . . . . . . 9 $/\$
218	212, 111, 128	ledivmul2d 11082	. . . . . . . . 9 $/\$
219	217, 218	mpbird 232	. . . . . . . 8 $/\$
220	196, 130, 111, 198, 219	letrd 9533	. . . . . . 7 $/\$
221		eluz 10879	. . . . . . . 8 $/\$
222	131, 207, 221	syl2anc 661	. . . . . . 7 $/\$
223	220, 222	mpbird 232	. . . . . 6 $/\$
224		fzss2 11503	. . . . . 6
225	223, 224	syl 16	. . . . 5 $/\$
226		sumhash 13963	. . . . 5 $/\$
227	1, 225, 226	syl2anc 661	. . . 4 $/\$
228	129	rprege0d 11039	. . . . 5 $/\$ $/\$
229		flge0nn0 11671	. . . . 5 $/\$
230		hashfz1 12122	. . . . 5
231	228, 229, 230	3syl 20	. . . 4 $/\$
232	227, 231	eqtr2d 2476	. . 3 $/\$
233	194, 195, 232	3brtr4d 4327	. 2 $/\$
234		simpr 461	. . . . 5 $/\$
235		nnnn0 10591	. . . . . . 7
236		fzctr 11534	. . . . . . 7
237		bccl2 12104	. . . . . . 7
238	235, 236, 237	3syl 20	. . . . . 6
239	238	adantr 465	. . . . 5 $/\$
240	234, 239	pccld 13922	. . . 4 $/\$
241	240	nn0zd 10750	. . 3 $/\$
242		efexple 22625	. . 3 $/\$ $/\$ $/\$
243	94, 99, 241, 105, 242	syl211anc 1224	. 2 $/\$
244	233, 243	mpbird 232	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369

wceq 1369

wcel 1756

wss 3333

cif 3796 class class class wbr 4297

cfv 5423 (class class class)co 6096

cfn 7315

cc 9285

cr 9286

cc0 9287

c1 9288

caddc 9290

cmul 9292

clt 9423

cle 9424

cmin 9600

cdiv 9998

cn 10327

c2 10376

cn0 10584

cz 10651

cuz 10866

crp 10996

cfz 11442

cfl 11645

cexp 11870

cbc 12083

chash 12108

csu 13168

ce 13352

cprime 13768

cpc 13908

clog 22011

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4408 ax-sep 4418 ax-nul 4426 ax-pow 4475 ax-pr 4536 ax-un 6377 ax-inf2 7852 ax-cnex 9343 ax-resscn 9344 ax-1cn 9345 ax-icn 9346 ax-addcl 9347 ax-addrcl 9348 ax-mulcl 9349 ax-mulrcl 9350 ax-mulcom 9351 ax-addass 9352 ax-mulass 9353 ax-distr 9354 ax-i2m1 9355 ax-1ne0 9356 ax-1rid 9357 ax-rnegex 9358 ax-rrecex 9359 ax-cnre 9360 ax-pre-lttri 9361 ax-pre-lttrn 9362 ax-pre-ltadd 9363 ax-pre-mulgt0 9364 ax-pre-sup 9365 ax-addf 9366 ax-mulf 9367

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-fal 1375 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2573 df-ne 2613 df-nel 2614 df-ral 2725 df-rex 2726 df-reu 2727 df-rmo 2728 df-rab 2729 df-v 2979 df-sbc 3192 df-csb 3294 df-dif 3336 df-un 3338 df-in 3340 df-ss 3347 df-pss 3349 df-nul 3643 df-if 3797 df-pw 3867 df-sn 3883 df-pr 3885 df-tp 3887 df-op 3889 df-uni 4097 df-int 4134 df-iun 4178 df-iin 4179 df-br 4298 df-opab 4356 df-mpt 4357 df-tr 4391 df-eprel 4637 df-id 4641 df-po 4646 df-so 4647 df-fr 4684 df-se 4685 df-we 4686 df-ord 4727 df-on 4728 df-lim 4729 df-suc 4730 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-iota 5386 df-fun 5425 df-fn 5426 df-f 5427 df-f1 5428 df-fo 5429 df-f1o 5430 df-fv 5431 df-isom 5432 df-riota 6057 df-ov 6099 df-oprab 6100 df-mpt2 6101 df-of 6325 df-om 6482 df-1st 6582 df-2nd 6583 df-supp 6696 df-recs 6837 df-rdg 6871 df-1o 6925 df-2o 6926 df-oadd 6929 df-er 7106 df-map 7221 df-pm 7222 df-ixp 7269 df-en 7316 df-dom 7317 df-sdom 7318 df-fin 7319 df-fsupp 7626 df-fi 7666 df-sup 7696 df-oi 7729 df-card 8114 df-cda 8342 df-pnf 9425 df-mnf 9426 df-xr 9427 df-ltxr 9428 df-le 9429 df-sub 9602 df-neg 9603 df-div 9999 df-nn 10328 df-2 10385 df-3 10386 df-4 10387 df-5 10388 df-6 10389 df-7 10390 df-8 10391 df-9 10392 df-10 10393 df-n0 10585 df-z 10652 df-dec 10761 df-uz 10867 df-q 10959 df-rp 10997 df-xneg 11094 df-xadd 11095 df-xmul 11096 df-ioo 11309 df-ioc 11310 df-ico 11311 df-icc 11312 df-fz 11443 df-fzo 11554 df-fl 11647 df-mod 11714 df-seq 11812 df-exp 11871 df-fac 12057 df-bc 12084 df-hash 12109 df-shft 12561 df-cj 12593 df-re 12594 df-im 12595 df-sqr 12729 df-abs 12730 df-limsup 12954 df-clim 12971 df-rlim 12972 df-sum 13169 df-ef 13358 df-sin 13360 df-cos 13361 df-pi 13363 df-dvds 13541 df-gcd 13696 df-prm 13769 df-pc 13909 df-struct 14181 df-ndx 14182 df-slot 14183 df-base 14184 df-sets 14185 df-ress 14186 df-plusg 14256 df-mulr 14257 df-starv 14258 df-sca 14259 df-vsca 14260 df-ip 14261 df-tset 14262 df-ple 14263 df-ds 14265 df-unif 14266 df-hom 14267 df-cco 14268 df-rest 14366 df-topn 14367 df-0g 14385 df-gsum 14386 df-topgen 14387 df-pt 14388 df-prds 14391 df-xrs 14445 df-qtop 14450 df-imas 14451 df-xps 14453 df-mre 14529 df-mrc 14530 df-acs 14532 df-mnd 15420 df-submnd 15470 df-mulg 15553 df-cntz 15840 df-cmn 16284 df-psmet 17814 df-xmet 17815 df-met 17816 df-bl 17817 df-mopn 17818 df-fbas 17819 df-fg 17820 df-cnfld 17824 df-top 18508 df-bases 18510 df-topon 18511 df-topsp 18512 df-cld 18628 df-ntr 18629 df-cls 18630 df-nei 18707 df-lp 18745 df-perf 18746 df-cn 18836 df-cnp 18837 df-haus 18924 df-tx 19140 df-hmeo 19333 df-fil 19424 df-fm 19516 df-flim 19517 df-flf 19518 df-xms 19900 df-ms 19901 df-tms 19902 df-cncf 20459 df-limc 21346 df-dv 21347 df-log 22013

This theorem is referenced by: bposlem5 22632 bposlem6 22633 chebbnd1lem1 22723

W3C validator