bposlem1 - Metamath Proof Explorer

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

Theorem bposlem1 23830

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 12035	. . . 4 $/\$
2		2nn 10652	. . . . . . . . . . 11
3		nnmulcl 10517	. . . . . . . . . . 11 $/\$
4	2, 3	mpan 668	. . . . . . . . . 10
5	4	ad2antrr 724	. . . . . . . . 9 $/\$ $/\$
6		prmnn 14319	. . . . . . . . . . 11
7	6	ad2antlr 725	. . . . . . . . . 10 $/\$ $/\$
8		elfznn 11683	. . . . . . . . . . . 12
9	8	adantl 464	. . . . . . . . . . 11 $/\$ $/\$
10	9	nnnn0d 10811	. . . . . . . . . 10 $/\$ $/\$
11	7, 10	nnexpcld 12283	. . . . . . . . 9 $/\$ $/\$
12		nnrp 11190	. . . . . . . . . 10
13		nnrp 11190	. . . . . . . . . 10
14		rpdivcl 11204	. . . . . . . . . 10 $/\$
15	12, 13, 14	syl2an 475	. . . . . . . . 9 $/\$
16	5, 11, 15	syl2anc 659	. . . . . . . 8 $/\$ $/\$
17	16	rpred 11220	. . . . . . 7 $/\$ $/\$
18	17	flcld 11883	. . . . . 6 $/\$ $/\$
19		2z 10855	. . . . . . 7
20		simpll 752	. . . . . . . . . 10 $/\$ $/\$
21		nnrp 11190	. . . . . . . . . . 11
22		rpdivcl 11204	. . . . . . . . . . 11 $/\$
23	21, 13, 22	syl2an 475	. . . . . . . . . 10 $/\$
24	20, 11, 23	syl2anc 659	. . . . . . . . 9 $/\$ $/\$
25	24	rpred 11220	. . . . . . . 8 $/\$ $/\$
26	25	flcld 11883	. . . . . . 7 $/\$ $/\$
27		zmulcl 10871	. . . . . . 7 $/\$
28	19, 26, 27	sylancr 661	. . . . . 6 $/\$ $/\$
29	18, 28	zsubcld 10931	. . . . 5 $/\$ $/\$
30	29	zred 10926	. . . 4 $/\$ $/\$
31		1re 9543	. . . . . 6
32		0re 9544	. . . . . 6
33	31, 32	keepel 3949	. . . . 5
34	33	a1i 11	. . . 4 $/\$ $/\$
35	28	zred 10926	. . . . . . . . . 10 $/\$ $/\$
36	17, 35	resubcld 9946	. . . . . . . . 9 $/\$ $/\$
37		2re 10564	. . . . . . . . . 10
38	37	a1i 11	. . . . . . . . 9 $/\$ $/\$
39	18	zred 10926	. . . . . . . . . 10 $/\$ $/\$
40		flle 11884	. . . . . . . . . . 11
41	17, 40	syl 17	. . . . . . . . . 10 $/\$ $/\$
42	39, 17, 35, 41	lesub1dd 10126	. . . . . . . . 9 $/\$ $/\$
43		resubcl 9837	. . . . . . . . . . . . 13 $/\$
44	25, 31, 43	sylancl 660	. . . . . . . . . . . 12 $/\$ $/\$
45		remulcl 9525	. . . . . . . . . . . 12 $/\$
46	37, 44, 45	sylancr 661	. . . . . . . . . . 11 $/\$ $/\$
47		flltp1 11885	. . . . . . . . . . . . . 14
48	25, 47	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
49		1red 9559	. . . . . . . . . . . . . 14 $/\$ $/\$
50	26	zred 10926	. . . . . . . . . . . . . 14 $/\$ $/\$
51	25, 49, 50	ltsubaddd 10106	. . . . . . . . . . . . 13 $/\$ $/\$
52	48, 51	mpbird 232	. . . . . . . . . . . 12 $/\$ $/\$
53		2pos 10586	. . . . . . . . . . . . . . 15
54	37, 53	pm3.2i 453	. . . . . . . . . . . . . 14 $/\$
55		ltmul2 10352	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
56	54, 55	mp3an3 1313	. . . . . . . . . . . . 13 $/\$
57	44, 50, 56	syl2anc 659	. . . . . . . . . . . 12 $/\$ $/\$
58	52, 57	mpbid 210	. . . . . . . . . . 11 $/\$ $/\$
59	46, 35, 17, 58	ltsub2dd 10123	. . . . . . . . . 10 $/\$ $/\$
60		2cnd 10567	. . . . . . . . . . . . 13 $/\$ $/\$
61		nncn 10502	. . . . . . . . . . . . . 14
62	61	ad2antrr 724	. . . . . . . . . . . . 13 $/\$ $/\$
63	11	nncnd 10510	. . . . . . . . . . . . 13 $/\$ $/\$
64	11	nnne0d 10539	. . . . . . . . . . . . 13 $/\$ $/\$
65	60, 62, 63, 64	divassd 10314	. . . . . . . . . . . 12 $/\$ $/\$
66	25	recnd 9570	. . . . . . . . . . . . . 14 $/\$ $/\$
67		1cnd 9560	. . . . . . . . . . . . . 14 $/\$ $/\$
68	60, 66, 67	subdid 9971	. . . . . . . . . . . . 13 $/\$ $/\$
69		2t1e2 10643	. . . . . . . . . . . . . 14
70	69	oveq2i 6243	. . . . . . . . . . . . 13
71	68, 70	syl6eq 2457	. . . . . . . . . . . 12 $/\$ $/\$
72	65, 71	oveq12d 6250	. . . . . . . . . . 11 $/\$ $/\$
73		remulcl 9525	. . . . . . . . . . . . . 14 $/\$
74	37, 25, 73	sylancr 661	. . . . . . . . . . . . 13 $/\$ $/\$
75	74	recnd 9570	. . . . . . . . . . . 12 $/\$ $/\$
76		2cn 10565	. . . . . . . . . . . 12
77		nncan 9802	. . . . . . . . . . . 12 $/\$
78	75, 76, 77	sylancl 660	. . . . . . . . . . 11 $/\$ $/\$
79	72, 78	eqtrd 2441	. . . . . . . . . 10 $/\$ $/\$
80	59, 79	breqtrd 4416	. . . . . . . . 9 $/\$ $/\$
81	30, 36, 38, 42, 80	lelttrd 9692	. . . . . . . 8 $/\$ $/\$
82		df-2 10553	. . . . . . . 8
83	81, 82	syl6breq 4431	. . . . . . 7 $/\$ $/\$
84		1z 10853	. . . . . . . 8
85		zleltp1 10873	. . . . . . . 8 $/\$
86	29, 84, 85	sylancl 660	. . . . . . 7 $/\$ $/\$
87	83, 86	mpbird 232	. . . . . 6 $/\$ $/\$
88		iftrue 3888	. . . . . . 7
89	88	breq2d 4404	. . . . . 6
90	87, 89	syl5ibrcom 222	. . . . 5 $/\$ $/\$
91	9	nnge1d 10537	. . . . . . . . . . 11 $/\$ $/\$
92	91	biantrurd 506	. . . . . . . . . 10 $/\$ $/\$ $/\$
93	6	adantl 464	. . . . . . . . . . . . . 14 $/\$
94	93	nnred 10509	. . . . . . . . . . . . 13 $/\$
95		prmuz2 14334	. . . . . . . . . . . . . . 15
96	95	adantl 464	. . . . . . . . . . . . . 14 $/\$
97		eluz2b1 11114	. . . . . . . . . . . . . . 15 $/\$
98	97	simprbi 462	. . . . . . . . . . . . . 14
99	96, 98	syl 17	. . . . . . . . . . . . 13 $/\$
100	94, 99	jca 530	. . . . . . . . . . . 12 $/\$ $/\$
101	100	adantr 463	. . . . . . . . . . 11 $/\$ $/\$ $/\$
102		elfzelz 11657	. . . . . . . . . . . 12
103	102	adantl 464	. . . . . . . . . . 11 $/\$ $/\$
104	4	adantr 463	. . . . . . . . . . . . 13 $/\$
105	104	nnrpd 11218	. . . . . . . . . . . 12 $/\$
106	105	adantr 463	. . . . . . . . . . 11 $/\$ $/\$
107		efexple 23827	. . . . . . . . . . 11 $/\$ $/\$ $/\$
108	101, 103, 106, 107	syl3anc 1228	. . . . . . . . . 10 $/\$ $/\$
109	9	nnzd 10925	. . . . . . . . . . 11 $/\$ $/\$
110	84	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
111	104	nnred 10509	. . . . . . . . . . . . . . . 16 $/\$
112		1red 9559	. . . . . . . . . . . . . . . . 17 $/\$
113	37	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
114		1lt2 10661	. . . . . . . . . . . . . . . . . 18
115	114	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
116		nnre 10501	. . . . . . . . . . . . . . . . . . . 20
117	116	adantr 463	. . . . . . . . . . . . . . . . . . 19 $/\$
118		0le2 10585	. . . . . . . . . . . . . . . . . . . . 21
119	37, 118	pm3.2i 453	. . . . . . . . . . . . . . . . . . . 20 $/\$
120	119	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
121		nnge1 10520	. . . . . . . . . . . . . . . . . . . 20
122	121	adantr 463	. . . . . . . . . . . . . . . . . . 19 $/\$
123		lemul2a 10356	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
124	112, 117, 120, 122, 123	syl31anc 1231	. . . . . . . . . . . . . . . . . 18 $/\$
125	69, 124	syl5eqbrr 4426	. . . . . . . . . . . . . . . . 17 $/\$
126	112, 113, 111, 115, 125	ltletrd 9694	. . . . . . . . . . . . . . . 16 $/\$
127	111, 126	rplogcld 23198	. . . . . . . . . . . . . . 15 $/\$
128	94, 99	rplogcld 23198	. . . . . . . . . . . . . . 15 $/\$
129	127, 128	rpdivcld 11237	. . . . . . . . . . . . . 14 $/\$
130	129	rpred 11220	. . . . . . . . . . . . 13 $/\$
131	130	flcld 11883	. . . . . . . . . . . 12 $/\$
132	131	adantr 463	. . . . . . . . . . 11 $/\$ $/\$
133		elfz 11647	. . . . . . . . . . 11 $/\$ $/\$ $/\$
134	109, 110, 132, 133	syl3anc 1228	. . . . . . . . . 10 $/\$ $/\$ $/\$
135	92, 108, 134	3bitr4rd 286	. . . . . . . . 9 $/\$ $/\$
136	135	notbid 292	. . . . . . . 8 $/\$ $/\$
137	111	adantr 463	. . . . . . . . 9 $/\$ $/\$
138	11	nnred 10509	. . . . . . . . 9 $/\$ $/\$
139	137, 138	ltnled 9682	. . . . . . . 8 $/\$ $/\$
140	136, 139	bitr4d 256	. . . . . . 7 $/\$ $/\$
141	16	rpge0d 11224	. . . . . . . . . . . . 13 $/\$ $/\$
142	141	adantrr 715	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
143	11	nngt0d 10538	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
144		ltdivmul 10376	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
145	137, 49, 138, 143, 144	syl112anc 1232	. . . . . . . . . . . . . . . 16 $/\$ $/\$
146	63	mulid1d 9561	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
147	146	breq2d 4404	. . . . . . . . . . . . . . . 16 $/\$ $/\$
148	145, 147	bitrd 253	. . . . . . . . . . . . . . 15 $/\$ $/\$
149	148	biimprd 223	. . . . . . . . . . . . . 14 $/\$ $/\$
150	149	impr 617	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
151		0p1e1 10606	. . . . . . . . . . . . 13
152	150, 151	syl6breqr 4432	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
153	17	adantrr 715	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
154		0z 10834	. . . . . . . . . . . . 13
155		flbi 11900	. . . . . . . . . . . . 13 $/\$ $/\$
156	153, 154, 155	sylancl 660	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
157	142, 152, 156	mpbir2and 921	. . . . . . . . . . 11 $/\$ $/\$ $/\$
158	24	rpge0d 11224	. . . . . . . . . . . . . . 15 $/\$ $/\$
159	158	adantrr 715	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
160	116, 21	ltaddrp2d 11250	. . . . . . . . . . . . . . . . . . . 20
161	61	2timesd 10740	. . . . . . . . . . . . . . . . . . . 20
162	160, 161	breqtrrd 4418	. . . . . . . . . . . . . . . . . . 19
163	162	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
164	116	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
165		lttr 9610	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
166	164, 137, 138, 165	syl3anc 1228	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
167	163, 166	mpand 673	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
168		ltdivmul 10376	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
169	164, 49, 138, 143, 168	syl112anc 1232	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
170	146	breq2d 4404	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
171	169, 170	bitrd 253	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
172	167, 171	sylibrd 234	. . . . . . . . . . . . . . . 16 $/\$ $/\$
173	172	impr 617	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
174	173, 151	syl6breqr 4432	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
175	25	adantrr 715	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
176		flbi 11900	. . . . . . . . . . . . . . 15 $/\$ $/\$
177	175, 154, 176	sylancl 660	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
178	159, 174, 177	mpbir2and 921	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
179	178	oveq2d 6248	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
180		2t0e0 10650	. . . . . . . . . . . 12
181	179, 180	syl6eq 2457	. . . . . . . . . . 11 $/\$ $/\$ $/\$
182	157, 181	oveq12d 6250	. . . . . . . . . 10 $/\$ $/\$ $/\$
183		0m0e0 10604	. . . . . . . . . 10
184	182, 183	syl6eq 2457	. . . . . . . . 9 $/\$ $/\$ $/\$
185		0le0 10584	. . . . . . . . 9
186	184, 185	syl6eqbr 4429	. . . . . . . 8 $/\$ $/\$ $/\$
187	186	expr 613	. . . . . . 7 $/\$ $/\$
188	140, 187	sylbid 215	. . . . . 6 $/\$ $/\$
189		iffalse 3891	. . . . . . . 8
190	189	eqcomd 2408	. . . . . . 7
191	190	breq2d 4404	. . . . . 6
192	188, 191	mpbidi 216	. . . . 5 $/\$ $/\$
193	90, 192	pm2.61d 158	. . . 4 $/\$ $/\$
194	1, 30, 34, 193	fsumle 13669	. . 3 $/\$
195		pcbcctr 23822	. . 3 $/\$
196	131	zred 10926	. . . . . . . 8 $/\$
197		flle 11884	. . . . . . . . 9
198	130, 197	syl 17	. . . . . . . 8 $/\$
199	104	nnnn0d 10811	. . . . . . . . . . . . . 14 $/\$
200	93, 199	nnexpcld 12283	. . . . . . . . . . . . 13 $/\$
201	200	nnred 10509	. . . . . . . . . . . 12 $/\$
202		bernneq3 12246	. . . . . . . . . . . . 13 $/\$
203	96, 199, 202	syl2anc 659	. . . . . . . . . . . 12 $/\$
204	111, 201, 203	ltled 9683	. . . . . . . . . . 11 $/\$
205	105	reeflogd 23193	. . . . . . . . . . 11 $/\$
206	93	nnrpd 11218	. . . . . . . . . . . . 13 $/\$
207	104	nnzd 10925	. . . . . . . . . . . . 13 $/\$
208		reexplog 23164	. . . . . . . . . . . . 13 $/\$
209	206, 207, 208	syl2anc 659	. . . . . . . . . . . 12 $/\$
210	209	eqcomd 2408	. . . . . . . . . . 11 $/\$
211	204, 205, 210	3brtr4d 4422	. . . . . . . . . 10 $/\$
212	105	relogcld 23192	. . . . . . . . . . 11 $/\$
213	128	rpred 11220	. . . . . . . . . . . 12 $/\$
214	111, 213	remulcld 9572	. . . . . . . . . . 11 $/\$
215		efle 13952	. . . . . . . . . . 11 $/\$
216	212, 214, 215	syl2anc 659	. . . . . . . . . 10 $/\$
217	211, 216	mpbird 232	. . . . . . . . 9 $/\$
218	212, 111, 128	ledivmul2d 11270	. . . . . . . . 9 $/\$
219	217, 218	mpbird 232	. . . . . . . 8 $/\$
220	196, 130, 111, 198, 219	letrd 9691	. . . . . . 7 $/\$
221		eluz 11056	. . . . . . . 8 $/\$
222	131, 207, 221	syl2anc 659	. . . . . . 7 $/\$
223	220, 222	mpbird 232	. . . . . 6 $/\$
224		fzss2 11693	. . . . . 6
225	223, 224	syl 17	. . . . 5 $/\$
226		sumhash 14514	. . . . 5 $/\$
227	1, 225, 226	syl2anc 659	. . . 4 $/\$
228	129	rprege0d 11227	. . . . 5 $/\$ $/\$
229		flge0nn0 11903	. . . . 5 $/\$
230		hashfz1 12371	. . . . 5
231	228, 229, 230	3syl 20	. . . 4 $/\$
232	227, 231	eqtr2d 2442	. . 3 $/\$
233	194, 195, 232	3brtr4d 4422	. 2 $/\$
234		simpr 459	. . . . 5 $/\$
235		nnnn0 10761	. . . . . . 7
236		fzctr 11757	. . . . . . 7
237		bccl2 12353	. . . . . . 7
238	235, 236, 237	3syl 20	. . . . . 6
239	238	adantr 463	. . . . 5 $/\$
240	234, 239	pccld 14473	. . . 4 $/\$
241	240	nn0zd 10924	. . 3 $/\$
242		efexple 23827	. . 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 367

wceq 1403

wcel 1840

wss 3411

cif 3882 class class class wbr 4392

cfv 5523 (class class class)co 6232

cfn 7472

cc 9438

cr 9439

cc0 9440

c1 9441

caddc 9443

cmul 9445

clt 9576

cle 9577

cmin 9759

cdiv 10165

cn 10494

c2 10544

cn0 10754

cz 10823

cuz 11043

crp 11181

cfz 11641

cfl 11875

cexp 12118

cbc 12332

chash 12357

csu 13562

ce 13896

cprime 14316

cpc 14459

clog 23124

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1637 ax-4 1650 ax-5 1723 ax-6 1769 ax-7 1812 ax-8 1842 ax-9 1844 ax-10 1859 ax-11 1864 ax-12 1876 ax-13 2024 ax-ext 2378 ax-rep 4504 ax-sep 4514 ax-nul 4522 ax-pow 4569 ax-pr 4627 ax-un 6528 ax-inf2 8009 ax-cnex 9496 ax-resscn 9497 ax-1cn 9498 ax-icn 9499 ax-addcl 9500 ax-addrcl 9501 ax-mulcl 9502 ax-mulrcl 9503 ax-mulcom 9504 ax-addass 9505 ax-mulass 9506 ax-distr 9507 ax-i2m1 9508 ax-1ne0 9509 ax-1rid 9510 ax-rnegex 9511 ax-rrecex 9512 ax-cnre 9513 ax-pre-lttri 9514 ax-pre-lttrn 9515 ax-pre-ltadd 9516 ax-pre-mulgt0 9517 ax-pre-sup 9518 ax-addf 9519 ax-mulf 9520

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 973 df-3an 974 df-tru 1406 df-fal 1409 df-ex 1632 df-nf 1636 df-sb 1762 df-eu 2240 df-mo 2241 df-clab 2386 df-cleq 2392 df-clel 2395 df-nfc 2550 df-ne 2598 df-nel 2599 df-ral 2756 df-rex 2757 df-reu 2758 df-rmo 2759 df-rab 2760 df-v 3058 df-sbc 3275 df-csb 3371 df-dif 3414 df-un 3416 df-in 3418 df-ss 3425 df-pss 3427 df-nul 3736 df-if 3883 df-pw 3954 df-sn 3970 df-pr 3972 df-tp 3974 df-op 3976 df-uni 4189 df-int 4225 df-iun 4270 df-iin 4271 df-br 4393 df-opab 4451 df-mpt 4452 df-tr 4487 df-eprel 4731 df-id 4735 df-po 4741 df-so 4742 df-fr 4779 df-se 4780 df-we 4781 df-ord 4822 df-on 4823 df-lim 4824 df-suc 4825 df-xp 4946 df-rel 4947 df-cnv 4948 df-co 4949 df-dm 4950 df-rn 4951 df-res 4952 df-ima 4953 df-iota 5487 df-fun 5525 df-fn 5526 df-f 5527 df-f1 5528 df-fo 5529 df-f1o 5530 df-fv 5531 df-isom 5532 df-riota 6194 df-ov 6235 df-oprab 6236 df-mpt2 6237 df-of 6475 df-om 6637 df-1st 6736 df-2nd 6737 df-supp 6855 df-recs 6997 df-rdg 7031 df-1o 7085 df-2o 7086 df-oadd 7089 df-er 7266 df-map 7377 df-pm 7378 df-ixp 7426 df-en 7473 df-dom 7474 df-sdom 7475 df-fin 7476 df-fsupp 7782 df-fi 7823 df-sup 7853 df-oi 7887 df-card 8270 df-cda 8498 df-pnf 9578 df-mnf 9579 df-xr 9580 df-ltxr 9581 df-le 9582 df-sub 9761 df-neg 9762 df-div 10166 df-nn 10495 df-2 10553 df-3 10554 df-4 10555 df-5 10556 df-6 10557 df-7 10558 df-8 10559 df-9 10560 df-10 10561 df-n0 10755 df-z 10824 df-dec 10938 df-uz 11044 df-q 11144 df-rp 11182 df-xneg 11287 df-xadd 11288 df-xmul 11289 df-ioo 11502 df-ioc 11503 df-ico 11504 df-icc 11505 df-fz 11642 df-fzo 11766 df-fl 11877 df-mod 11946 df-seq 12060 df-exp 12119 df-fac 12306 df-bc 12333 df-hash 12358 df-shft 12954 df-cj 12986 df-re 12987 df-im 12988 df-sqrt 13122 df-abs 13123 df-limsup 13348 df-clim 13365 df-rlim 13366 df-sum 13563 df-ef 13902 df-sin 13904 df-cos 13905 df-pi 13907 df-dvds 14086 df-gcd 14244 df-prm 14317 df-pc 14460 df-struct 14733 df-ndx 14734 df-slot 14735 df-base 14736 df-sets 14737 df-ress 14738 df-plusg 14812 df-mulr 14813 df-starv 14814 df-sca 14815 df-vsca 14816 df-ip 14817 df-tset 14818 df-ple 14819 df-ds 14821 df-unif 14822 df-hom 14823 df-cco 14824 df-rest 14927 df-topn 14928 df-0g 14946 df-gsum 14947 df-topgen 14948 df-pt 14949 df-prds 14952 df-xrs 15006 df-qtop 15011 df-imas 15012 df-xps 15014 df-mre 15090 df-mrc 15091 df-acs 15093 df-mgm 16086 df-sgrp 16125 df-mnd 16135 df-submnd 16181 df-mulg 16274 df-cntz 16569 df-cmn 17014 df-psmet 18621 df-xmet 18622 df-met 18623 df-bl 18624 df-mopn 18625 df-fbas 18626 df-fg 18627 df-cnfld 18631 df-top 19581 df-bases 19583 df-topon 19584 df-topsp 19585 df-cld 19702 df-ntr 19703 df-cls 19704 df-nei 19782 df-lp 19820 df-perf 19821 df-cn 19911 df-cnp 19912 df-haus 19999 df-tx 20245 df-hmeo 20438 df-fil 20529 df-fm 20621 df-flim 20622 df-flf 20623 df-xms 21005 df-ms 21006 df-tms 21007 df-cncf 21564 df-limc 22452 df-dv 22453 df-log 23126

This theorem is referenced by: bposlem5 23834 bposlem6 23835 chebbnd1lem1 23925

W3C validator