bposlem1 - Metamath Proof Explorer

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

Theorem bposlem1 24204

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 12187	. . . 4 $/\$
2		2nn 10769	. . . . . . . . . . 11
3		nnmulcl 10634	. . . . . . . . . . 11 $/\$
4	2, 3	mpan 675	. . . . . . . . . 10
5	4	ad2antrr 731	. . . . . . . . 9 $/\$ $/\$
6		prmnn 14618	. . . . . . . . . . 11
7	6	ad2antlr 732	. . . . . . . . . 10 $/\$ $/\$
8		elfznn 11830	. . . . . . . . . . . 12
9	8	adantl 468	. . . . . . . . . . 11 $/\$ $/\$
10	9	nnnn0d 10927	. . . . . . . . . 10 $/\$ $/\$
11	7, 10	nnexpcld 12438	. . . . . . . . 9 $/\$ $/\$
12		nnrp 11313	. . . . . . . . . 10
13		nnrp 11313	. . . . . . . . . 10
14		rpdivcl 11327	. . . . . . . . . 10 $/\$
15	12, 13, 14	syl2an 480	. . . . . . . . 9 $/\$
16	5, 11, 15	syl2anc 666	. . . . . . . 8 $/\$ $/\$
17	16	rpred 11343	. . . . . . 7 $/\$ $/\$
18	17	flcld 12035	. . . . . 6 $/\$ $/\$
19		2z 10971	. . . . . . 7
20		simpll 759	. . . . . . . . . 10 $/\$ $/\$
21		nnrp 11313	. . . . . . . . . . 11
22		rpdivcl 11327	. . . . . . . . . . 11 $/\$
23	21, 13, 22	syl2an 480	. . . . . . . . . 10 $/\$
24	20, 11, 23	syl2anc 666	. . . . . . . . 9 $/\$ $/\$
25	24	rpred 11343	. . . . . . . 8 $/\$ $/\$
26	25	flcld 12035	. . . . . . 7 $/\$ $/\$
27		zmulcl 10987	. . . . . . 7 $/\$
28	19, 26, 27	sylancr 668	. . . . . 6 $/\$ $/\$
29	18, 28	zsubcld 11047	. . . . 5 $/\$ $/\$
30	29	zred 11042	. . . 4 $/\$ $/\$
31		1re 9644	. . . . . 6
32		0re 9645	. . . . . 6
33	31, 32	keepel 3977	. . . . 5
34	33	a1i 11	. . . 4 $/\$ $/\$
35	28	zred 11042	. . . . . . . . . 10 $/\$ $/\$
36	17, 35	resubcld 10049	. . . . . . . . 9 $/\$ $/\$
37		2re 10681	. . . . . . . . . 10
38	37	a1i 11	. . . . . . . . 9 $/\$ $/\$
39	18	zred 11042	. . . . . . . . . 10 $/\$ $/\$
40		flle 12036	. . . . . . . . . . 11
41	17, 40	syl 17	. . . . . . . . . 10 $/\$ $/\$
42	39, 17, 35, 41	lesub1dd 10231	. . . . . . . . 9 $/\$ $/\$
43		resubcl 9940	. . . . . . . . . . . . 13 $/\$
44	25, 31, 43	sylancl 667	. . . . . . . . . . . 12 $/\$ $/\$
45		remulcl 9626	. . . . . . . . . . . 12 $/\$
46	37, 44, 45	sylancr 668	. . . . . . . . . . 11 $/\$ $/\$
47		flltp1 12037	. . . . . . . . . . . . . 14
48	25, 47	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
49		1red 9660	. . . . . . . . . . . . . 14 $/\$ $/\$
50	26	zred 11042	. . . . . . . . . . . . . 14 $/\$ $/\$
51	25, 49, 50	ltsubaddd 10211	. . . . . . . . . . . . 13 $/\$ $/\$
52	48, 51	mpbird 236	. . . . . . . . . . . 12 $/\$ $/\$
53		2pos 10703	. . . . . . . . . . . . . . 15
54	37, 53	pm3.2i 457	. . . . . . . . . . . . . 14 $/\$
55		ltmul2 10458	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
56	54, 55	mp3an3 1350	. . . . . . . . . . . . 13 $/\$
57	44, 50, 56	syl2anc 666	. . . . . . . . . . . 12 $/\$ $/\$
58	52, 57	mpbid 214	. . . . . . . . . . 11 $/\$ $/\$
59	46, 35, 17, 58	ltsub2dd 10228	. . . . . . . . . 10 $/\$ $/\$
60		2cnd 10684	. . . . . . . . . . . . 13 $/\$ $/\$
61		nncn 10619	. . . . . . . . . . . . . 14
62	61	ad2antrr 731	. . . . . . . . . . . . 13 $/\$ $/\$
63	11	nncnd 10627	. . . . . . . . . . . . 13 $/\$ $/\$
64	11	nnne0d 10656	. . . . . . . . . . . . 13 $/\$ $/\$
65	60, 62, 63, 64	divassd 10420	. . . . . . . . . . . 12 $/\$ $/\$
66	25	recnd 9671	. . . . . . . . . . . . . 14 $/\$ $/\$
67		1cnd 9661	. . . . . . . . . . . . . 14 $/\$ $/\$
68	60, 66, 67	subdid 10076	. . . . . . . . . . . . 13 $/\$ $/\$
69		2t1e2 10760	. . . . . . . . . . . . . 14
70	69	oveq2i 6314	. . . . . . . . . . . . 13
71	68, 70	syl6eq 2480	. . . . . . . . . . . 12 $/\$ $/\$
72	65, 71	oveq12d 6321	. . . . . . . . . . 11 $/\$ $/\$
73		remulcl 9626	. . . . . . . . . . . . . 14 $/\$
74	37, 25, 73	sylancr 668	. . . . . . . . . . . . 13 $/\$ $/\$
75	74	recnd 9671	. . . . . . . . . . . 12 $/\$ $/\$
76		2cn 10682	. . . . . . . . . . . 12
77		nncan 9905	. . . . . . . . . . . 12 $/\$
78	75, 76, 77	sylancl 667	. . . . . . . . . . 11 $/\$ $/\$
79	72, 78	eqtrd 2464	. . . . . . . . . 10 $/\$ $/\$
80	59, 79	breqtrd 4446	. . . . . . . . 9 $/\$ $/\$
81	30, 36, 38, 42, 80	lelttrd 9795	. . . . . . . 8 $/\$ $/\$
82		df-2 10670	. . . . . . . 8
83	81, 82	syl6breq 4461	. . . . . . 7 $/\$ $/\$
84		1z 10969	. . . . . . . 8
85		zleltp1 10989	. . . . . . . 8 $/\$
86	29, 84, 85	sylancl 667	. . . . . . 7 $/\$ $/\$
87	83, 86	mpbird 236	. . . . . 6 $/\$ $/\$
88		iftrue 3916	. . . . . . 7
89	88	breq2d 4433	. . . . . 6
90	87, 89	syl5ibrcom 226	. . . . 5 $/\$ $/\$
91	9	nnge1d 10654	. . . . . . . . . . 11 $/\$ $/\$
92	91	biantrurd 511	. . . . . . . . . 10 $/\$ $/\$ $/\$
93	6	adantl 468	. . . . . . . . . . . . . 14 $/\$
94	93	nnred 10626	. . . . . . . . . . . . 13 $/\$
95		prmuz2 14635	. . . . . . . . . . . . . . 15
96	95	adantl 468	. . . . . . . . . . . . . 14 $/\$
97		eluz2b1 11232	. . . . . . . . . . . . . . 15 $/\$
98	97	simprbi 466	. . . . . . . . . . . . . 14
99	96, 98	syl 17	. . . . . . . . . . . . 13 $/\$
100	94, 99	jca 535	. . . . . . . . . . . 12 $/\$ $/\$
101	100	adantr 467	. . . . . . . . . . 11 $/\$ $/\$ $/\$
102		elfzelz 11802	. . . . . . . . . . . 12
103	102	adantl 468	. . . . . . . . . . 11 $/\$ $/\$
104	4	adantr 467	. . . . . . . . . . . . 13 $/\$
105	104	nnrpd 11341	. . . . . . . . . . . 12 $/\$
106	105	adantr 467	. . . . . . . . . . 11 $/\$ $/\$
107		efexple 24201	. . . . . . . . . . 11 $/\$ $/\$ $/\$
108	101, 103, 106, 107	syl3anc 1265	. . . . . . . . . 10 $/\$ $/\$
109	9	nnzd 11041	. . . . . . . . . . 11 $/\$ $/\$
110	84	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
111	104	nnred 10626	. . . . . . . . . . . . . . . 16 $/\$
112		1red 9660	. . . . . . . . . . . . . . . . 17 $/\$
113	37	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
114		1lt2 10778	. . . . . . . . . . . . . . . . . 18
115	114	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
116		nnre 10618	. . . . . . . . . . . . . . . . . . . 20
117	116	adantr 467	. . . . . . . . . . . . . . . . . . 19 $/\$
118		0le2 10702	. . . . . . . . . . . . . . . . . . . . 21
119	37, 118	pm3.2i 457	. . . . . . . . . . . . . . . . . . . 20 $/\$
120	119	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
121		nnge1 10637	. . . . . . . . . . . . . . . . . . . 20
122	121	adantr 467	. . . . . . . . . . . . . . . . . . 19 $/\$
123		lemul2a 10462	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
124	112, 117, 120, 122, 123	syl31anc 1268	. . . . . . . . . . . . . . . . . 18 $/\$
125	69, 124	syl5eqbrr 4456	. . . . . . . . . . . . . . . . 17 $/\$
126	112, 113, 111, 115, 125	ltletrd 9797	. . . . . . . . . . . . . . . 16 $/\$
127	111, 126	rplogcld 23570	. . . . . . . . . . . . . . 15 $/\$
128	94, 99	rplogcld 23570	. . . . . . . . . . . . . . 15 $/\$
129	127, 128	rpdivcld 11360	. . . . . . . . . . . . . 14 $/\$
130	129	rpred 11343	. . . . . . . . . . . . 13 $/\$
131	130	flcld 12035	. . . . . . . . . . . 12 $/\$
132	131	adantr 467	. . . . . . . . . . 11 $/\$ $/\$
133		elfz 11792	. . . . . . . . . . 11 $/\$ $/\$ $/\$
134	109, 110, 132, 133	syl3anc 1265	. . . . . . . . . 10 $/\$ $/\$ $/\$
135	92, 108, 134	3bitr4rd 290	. . . . . . . . 9 $/\$ $/\$
136	135	notbid 296	. . . . . . . 8 $/\$ $/\$
137	111	adantr 467	. . . . . . . . 9 $/\$ $/\$
138	11	nnred 10626	. . . . . . . . 9 $/\$ $/\$
139	137, 138	ltnled 9784	. . . . . . . 8 $/\$ $/\$
140	136, 139	bitr4d 260	. . . . . . 7 $/\$ $/\$
141	16	rpge0d 11347	. . . . . . . . . . . . 13 $/\$ $/\$
142	141	adantrr 722	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
143	11	nngt0d 10655	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
144		ltdivmul 10482	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
145	137, 49, 138, 143, 144	syl112anc 1269	. . . . . . . . . . . . . . . 16 $/\$ $/\$
146	63	mulid1d 9662	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
147	146	breq2d 4433	. . . . . . . . . . . . . . . 16 $/\$ $/\$
148	145, 147	bitrd 257	. . . . . . . . . . . . . . 15 $/\$ $/\$
149	148	biimprd 227	. . . . . . . . . . . . . 14 $/\$ $/\$
150	149	impr 624	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
151		0p1e1 10723	. . . . . . . . . . . . 13
152	150, 151	syl6breqr 4462	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
153	17	adantrr 722	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
154		0z 10950	. . . . . . . . . . . . 13
155		flbi 12052	. . . . . . . . . . . . 13 $/\$ $/\$
156	153, 154, 155	sylancl 667	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
157	142, 152, 156	mpbir2and 931	. . . . . . . . . . 11 $/\$ $/\$ $/\$
158	24	rpge0d 11347	. . . . . . . . . . . . . . 15 $/\$ $/\$
159	158	adantrr 722	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
160	116, 21	ltaddrp2d 11374	. . . . . . . . . . . . . . . . . . . 20
161	61	2timesd 10857	. . . . . . . . . . . . . . . . . . . 20
162	160, 161	breqtrrd 4448	. . . . . . . . . . . . . . . . . . 19
163	162	ad2antrr 731	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
164	116	ad2antrr 731	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
165		lttr 9712	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
166	164, 137, 138, 165	syl3anc 1265	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
167	163, 166	mpand 680	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
168		ltdivmul 10482	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
169	164, 49, 138, 143, 168	syl112anc 1269	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
170	146	breq2d 4433	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
171	169, 170	bitrd 257	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
172	167, 171	sylibrd 238	. . . . . . . . . . . . . . . 16 $/\$ $/\$
173	172	impr 624	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
174	173, 151	syl6breqr 4462	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
175	25	adantrr 722	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
176		flbi 12052	. . . . . . . . . . . . . . 15 $/\$ $/\$
177	175, 154, 176	sylancl 667	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
178	159, 174, 177	mpbir2and 931	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
179	178	oveq2d 6319	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
180		2t0e0 10767	. . . . . . . . . . . 12
181	179, 180	syl6eq 2480	. . . . . . . . . . 11 $/\$ $/\$ $/\$
182	157, 181	oveq12d 6321	. . . . . . . . . 10 $/\$ $/\$ $/\$
183		0m0e0 10721	. . . . . . . . . 10
184	182, 183	syl6eq 2480	. . . . . . . . 9 $/\$ $/\$ $/\$
185		0le0 10701	. . . . . . . . 9
186	184, 185	syl6eqbr 4459	. . . . . . . 8 $/\$ $/\$ $/\$
187	186	expr 619	. . . . . . 7 $/\$ $/\$
188	140, 187	sylbid 219	. . . . . 6 $/\$ $/\$
189		iffalse 3919	. . . . . . . 8
190	189	eqcomd 2431	. . . . . . 7
191	190	breq2d 4433	. . . . . 6
192	188, 191	mpbidi 220	. . . . 5 $/\$ $/\$
193	90, 192	pm2.61d 162	. . . 4 $/\$ $/\$
194	1, 30, 34, 193	fsumle 13852	. . 3 $/\$
195		pcbcctr 24196	. . 3 $/\$
196	131	zred 11042	. . . . . . . 8 $/\$
197		flle 12036	. . . . . . . . 9
198	130, 197	syl 17	. . . . . . . 8 $/\$
199	104	nnnn0d 10927	. . . . . . . . . . . . . 14 $/\$
200	93, 199	nnexpcld 12438	. . . . . . . . . . . . 13 $/\$
201	200	nnred 10626	. . . . . . . . . . . 12 $/\$
202		bernneq3 12401	. . . . . . . . . . . . 13 $/\$
203	96, 199, 202	syl2anc 666	. . . . . . . . . . . 12 $/\$
204	111, 201, 203	ltled 9785	. . . . . . . . . . 11 $/\$
205	105	reeflogd 23565	. . . . . . . . . . 11 $/\$
206	93	nnrpd 11341	. . . . . . . . . . . . 13 $/\$
207	104	nnzd 11041	. . . . . . . . . . . . 13 $/\$
208		reexplog 23536	. . . . . . . . . . . . 13 $/\$
209	206, 207, 208	syl2anc 666	. . . . . . . . . . . 12 $/\$
210	209	eqcomd 2431	. . . . . . . . . . 11 $/\$
211	204, 205, 210	3brtr4d 4452	. . . . . . . . . 10 $/\$
212	105	relogcld 23564	. . . . . . . . . . 11 $/\$
213	128	rpred 11343	. . . . . . . . . . . 12 $/\$
214	111, 213	remulcld 9673	. . . . . . . . . . 11 $/\$
215		efle 14165	. . . . . . . . . . 11 $/\$
216	212, 214, 215	syl2anc 666	. . . . . . . . . 10 $/\$
217	211, 216	mpbird 236	. . . . . . . . 9 $/\$
218	212, 111, 128	ledivmul2d 11394	. . . . . . . . 9 $/\$
219	217, 218	mpbird 236	. . . . . . . 8 $/\$
220	196, 130, 111, 198, 219	letrd 9794	. . . . . . 7 $/\$
221		eluz 11174	. . . . . . . 8 $/\$
222	131, 207, 221	syl2anc 666	. . . . . . 7 $/\$
223	220, 222	mpbird 236	. . . . . 6 $/\$
224		fzss2 11840	. . . . . 6
225	223, 224	syl 17	. . . . 5 $/\$
226		sumhash 14834	. . . . 5 $/\$
227	1, 225, 226	syl2anc 666	. . . 4 $/\$
228	129	rprege0d 11350	. . . . 5 $/\$ $/\$
229		flge0nn0 12055	. . . . 5 $/\$
230		hashfz1 12530	. . . . 5
231	228, 229, 230	3syl 18	. . . 4 $/\$
232	227, 231	eqtr2d 2465	. . 3 $/\$
233	194, 195, 232	3brtr4d 4452	. 2 $/\$
234		simpr 463	. . . . 5 $/\$
235		nnnn0 10878	. . . . . . 7
236		fzctr 11905	. . . . . . 7
237		bccl2 12509	. . . . . . 7
238	235, 236, 237	3syl 18	. . . . . 6
239	238	adantr 467	. . . . 5 $/\$
240	234, 239	pccld 14793	. . . 4 $/\$
241	240	nn0zd 11040	. . 3 $/\$
242		efexple 24201	. . 3 $/\$ $/\$ $/\$
243	94, 99, 241, 105, 242	syl211anc 1271	. 2 $/\$
244	233, 243	mpbird 236	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $/\$ wa 371

wceq 1438

wcel 1869

wss 3437

cif 3910 class class class wbr 4421

cfv 5599 (class class class)co 6303

cfn 7575

cc 9539

cr 9540

cc0 9541

c1 9542

caddc 9544

cmul 9546

clt 9677

cle 9678

cmin 9862

cdiv 10271

cn 10611

c2 10661

cn0 10871

cz 10939

cuz 11161

crp 11304

cfz 11786

cfl 12027

cexp 12273

cbc 12488

chash 12516

csu 13745

ce 14107

cprime 14615

cpc 14779

clog 23496

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1666 ax-4 1679 ax-5 1749 ax-6 1795 ax-7 1840 ax-8 1871 ax-9 1873 ax-10 1888 ax-11 1893 ax-12 1906 ax-13 2054 ax-ext 2401 ax-rep 4534 ax-sep 4544 ax-nul 4553 ax-pow 4600 ax-pr 4658 ax-un 6595 ax-inf2 8150 ax-cnex 9597 ax-resscn 9598 ax-1cn 9599 ax-icn 9600 ax-addcl 9601 ax-addrcl 9602 ax-mulcl 9603 ax-mulrcl 9604 ax-mulcom 9605 ax-addass 9606 ax-mulass 9607 ax-distr 9608 ax-i2m1 9609 ax-1ne0 9610 ax-1rid 9611 ax-rnegex 9612 ax-rrecex 9613 ax-cnre 9614 ax-pre-lttri 9615 ax-pre-lttrn 9616 ax-pre-ltadd 9617 ax-pre-mulgt0 9618 ax-pre-sup 9619 ax-addf 9620 ax-mulf 9621

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 984 df-3an 985 df-tru 1441 df-fal 1444 df-ex 1661 df-nf 1665 df-sb 1788 df-eu 2270 df-mo 2271 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2573 df-ne 2621 df-nel 2622 df-ral 2781 df-rex 2782 df-reu 2783 df-rmo 2784 df-rab 2785 df-v 3084 df-sbc 3301 df-csb 3397 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-pss 3453 df-nul 3763 df-if 3911 df-pw 3982 df-sn 3998 df-pr 4000 df-tp 4002 df-op 4004 df-uni 4218 df-int 4254 df-iun 4299 df-iin 4300 df-br 4422 df-opab 4481 df-mpt 4482 df-tr 4517 df-eprel 4762 df-id 4766 df-po 4772 df-so 4773 df-fr 4810 df-se 4811 df-we 4812 df-xp 4857 df-rel 4858 df-cnv 4859 df-co 4860 df-dm 4861 df-rn 4862 df-res 4863 df-ima 4864 df-pred 5397 df-ord 5443 df-on 5444 df-lim 5445 df-suc 5446 df-iota 5563 df-fun 5601 df-fn 5602 df-f 5603 df-f1 5604 df-fo 5605 df-f1o 5606 df-fv 5607 df-isom 5608 df-riota 6265 df-ov 6306 df-oprab 6307 df-mpt2 6308 df-of 6543 df-om 6705 df-1st 6805 df-2nd 6806 df-supp 6924 df-wrecs 7034 df-recs 7096 df-rdg 7134 df-1o 7188 df-2o 7189 df-oadd 7192 df-er 7369 df-map 7480 df-pm 7481 df-ixp 7529 df-en 7576 df-dom 7577 df-sdom 7578 df-fin 7579 df-fsupp 7888 df-fi 7929 df-sup 7960 df-inf 7961 df-oi 8029 df-card 8376 df-cda 8600 df-pnf 9679 df-mnf 9680 df-xr 9681 df-ltxr 9682 df-le 9683 df-sub 9864 df-neg 9865 df-div 10272 df-nn 10612 df-2 10670 df-3 10671 df-4 10672 df-5 10673 df-6 10674 df-7 10675 df-8 10676 df-9 10677 df-10 10678 df-n0 10872 df-z 10940 df-dec 11054 df-uz 11162 df-q 11267 df-rp 11305 df-xneg 11411 df-xadd 11412 df-xmul 11413 df-ioo 11641 df-ioc 11642 df-ico 11643 df-icc 11644 df-fz 11787 df-fzo 11918 df-fl 12029 df-mod 12098 df-seq 12215 df-exp 12274 df-fac 12461 df-bc 12489 df-hash 12517 df-shft 13124 df-cj 13156 df-re 13157 df-im 13158 df-sqrt 13292 df-abs 13293 df-limsup 13519 df-clim 13545 df-rlim 13546 df-sum 13746 df-ef 14114 df-sin 14116 df-cos 14117 df-pi 14119 df-dvds 14299 df-gcd 14462 df-prm 14616 df-pc 14780 df-struct 15116 df-ndx 15117 df-slot 15118 df-base 15119 df-sets 15120 df-ress 15121 df-plusg 15196 df-mulr 15197 df-starv 15198 df-sca 15199 df-vsca 15200 df-ip 15201 df-tset 15202 df-ple 15203 df-ds 15205 df-unif 15206 df-hom 15207 df-cco 15208 df-rest 15314 df-topn 15315 df-0g 15333 df-gsum 15334 df-topgen 15335 df-pt 15336 df-prds 15339 df-xrs 15393 df-qtop 15399 df-imas 15400 df-xps 15403 df-mre 15485 df-mrc 15486 df-acs 15488 df-mgm 16481 df-sgrp 16520 df-mnd 16530 df-submnd 16576 df-mulg 16669 df-cntz 16964 df-cmn 17425 df-psmet 18955 df-xmet 18956 df-met 18957 df-bl 18958 df-mopn 18959 df-fbas 18960 df-fg 18961 df-cnfld 18964 df-top 19913 df-bases 19914 df-topon 19915 df-topsp 19916 df-cld 20026 df-ntr 20027 df-cls 20028 df-nei 20106 df-lp 20144 df-perf 20145 df-cn 20235 df-cnp 20236 df-haus 20323 df-tx 20569 df-hmeo 20762 df-fil 20853 df-fm 20945 df-flim 20946 df-flf 20947 df-xms 21327 df-ms 21328 df-tms 21329 df-cncf 21902 df-limc 22813 df-dv 22814 df-log 23498

This theorem is referenced by: bposlem5 24208 bposlem6 24209 chebbnd1lem1 24299

W3C validator