bposlem1 - Metamath Proof Explorer

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

Theorem bposlem1 23684

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 12085	. . . 4 $/\$
2		2nn 10714	. . . . . . . . . . 11
3		nnmulcl 10579	. . . . . . . . . . 11 $/\$
4	2, 3	mpan 670	. . . . . . . . . 10
5	4	ad2antrr 725	. . . . . . . . 9 $/\$ $/\$
6		prmnn 14231	. . . . . . . . . . 11
7	6	ad2antlr 726	. . . . . . . . . 10 $/\$ $/\$
8		elfznn 11739	. . . . . . . . . . . 12
9	8	adantl 466	. . . . . . . . . . 11 $/\$ $/\$
10	9	nnnn0d 10873	. . . . . . . . . 10 $/\$ $/\$
11	7, 10	nnexpcld 12333	. . . . . . . . 9 $/\$ $/\$
12		nnrp 11254	. . . . . . . . . 10
13		nnrp 11254	. . . . . . . . . 10
14		rpdivcl 11267	. . . . . . . . . 10 $/\$
15	12, 13, 14	syl2an 477	. . . . . . . . 9 $/\$
16	5, 11, 15	syl2anc 661	. . . . . . . 8 $/\$ $/\$
17	16	rpred 11281	. . . . . . 7 $/\$ $/\$
18	17	flcld 11937	. . . . . 6 $/\$ $/\$
19		2z 10917	. . . . . . 7
20		simpll 753	. . . . . . . . . 10 $/\$ $/\$
21		nnrp 11254	. . . . . . . . . . 11
22		rpdivcl 11267	. . . . . . . . . . 11 $/\$
23	21, 13, 22	syl2an 477	. . . . . . . . . 10 $/\$
24	20, 11, 23	syl2anc 661	. . . . . . . . 9 $/\$ $/\$
25	24	rpred 11281	. . . . . . . 8 $/\$ $/\$
26	25	flcld 11937	. . . . . . 7 $/\$ $/\$
27		zmulcl 10933	. . . . . . 7 $/\$
28	19, 26, 27	sylancr 663	. . . . . 6 $/\$ $/\$
29	18, 28	zsubcld 10995	. . . . 5 $/\$ $/\$
30	29	zred 10990	. . . 4 $/\$ $/\$
31		1re 9612	. . . . . 6
32		0re 9613	. . . . . 6
33	31, 32	keepel 4012	. . . . 5
34	33	a1i 11	. . . 4 $/\$ $/\$
35	28	zred 10990	. . . . . . . . . 10 $/\$ $/\$
36	17, 35	resubcld 10008	. . . . . . . . 9 $/\$ $/\$
37		2re 10626	. . . . . . . . . 10
38	37	a1i 11	. . . . . . . . 9 $/\$ $/\$
39	18	zred 10990	. . . . . . . . . 10 $/\$ $/\$
40		flle 11938	. . . . . . . . . . 11
41	17, 40	syl 16	. . . . . . . . . 10 $/\$ $/\$
42	39, 17, 35, 41	lesub1dd 10189	. . . . . . . . 9 $/\$ $/\$
43		resubcl 9902	. . . . . . . . . . . . 13 $/\$
44	25, 31, 43	sylancl 662	. . . . . . . . . . . 12 $/\$ $/\$
45		remulcl 9594	. . . . . . . . . . . 12 $/\$
46	37, 44, 45	sylancr 663	. . . . . . . . . . 11 $/\$ $/\$
47		flltp1 11939	. . . . . . . . . . . . . 14
48	25, 47	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$
49		1red 9628	. . . . . . . . . . . . . 14 $/\$ $/\$
50	26	zred 10990	. . . . . . . . . . . . . 14 $/\$ $/\$
51	25, 49, 50	ltsubaddd 10169	. . . . . . . . . . . . 13 $/\$ $/\$
52	48, 51	mpbird 232	. . . . . . . . . . . 12 $/\$ $/\$
53		2pos 10648	. . . . . . . . . . . . . . 15
54	37, 53	pm3.2i 455	. . . . . . . . . . . . . 14 $/\$
55		ltmul2 10414	. . . . . . . . . . . . . 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 10186	. . . . . . . . . 10 $/\$ $/\$
60		2cnd 10629	. . . . . . . . . . . . 13 $/\$ $/\$
61		nncn 10564	. . . . . . . . . . . . . 14
62	61	ad2antrr 725	. . . . . . . . . . . . 13 $/\$ $/\$
63	11	nncnd 10572	. . . . . . . . . . . . 13 $/\$ $/\$
64	11	nnne0d 10601	. . . . . . . . . . . . 13 $/\$ $/\$
65	60, 62, 63, 64	divassd 10376	. . . . . . . . . . . 12 $/\$ $/\$
66	25	recnd 9639	. . . . . . . . . . . . . 14 $/\$ $/\$
67		1cnd 9629	. . . . . . . . . . . . . 14 $/\$ $/\$
68	60, 66, 67	subdid 10033	. . . . . . . . . . . . 13 $/\$ $/\$
69		2t1e2 10705	. . . . . . . . . . . . . 14
70	69	oveq2i 6307	. . . . . . . . . . . . 13
71	68, 70	syl6eq 2514	. . . . . . . . . . . 12 $/\$ $/\$
72	65, 71	oveq12d 6314	. . . . . . . . . . 11 $/\$ $/\$
73		remulcl 9594	. . . . . . . . . . . . . 14 $/\$
74	37, 25, 73	sylancr 663	. . . . . . . . . . . . 13 $/\$ $/\$
75	74	recnd 9639	. . . . . . . . . . . 12 $/\$ $/\$
76		2cn 10627	. . . . . . . . . . . 12
77		nncan 9867	. . . . . . . . . . . 12 $/\$
78	75, 76, 77	sylancl 662	. . . . . . . . . . 11 $/\$ $/\$
79	72, 78	eqtrd 2498	. . . . . . . . . 10 $/\$ $/\$
80	59, 79	breqtrd 4480	. . . . . . . . 9 $/\$ $/\$
81	30, 36, 38, 42, 80	lelttrd 9757	. . . . . . . 8 $/\$ $/\$
82		df-2 10615	. . . . . . . 8
83	81, 82	syl6breq 4495	. . . . . . 7 $/\$ $/\$
84		1z 10915	. . . . . . . 8
85		zleltp1 10935	. . . . . . . 8 $/\$
86	29, 84, 85	sylancl 662	. . . . . . 7 $/\$ $/\$
87	83, 86	mpbird 232	. . . . . 6 $/\$ $/\$
88		iftrue 3950	. . . . . . 7
89	88	breq2d 4468	. . . . . 6
90	87, 89	syl5ibrcom 222	. . . . 5 $/\$ $/\$
91	9	nnge1d 10599	. . . . . . . . . . 11 $/\$ $/\$
92	91	biantrurd 508	. . . . . . . . . 10 $/\$ $/\$ $/\$
93	6	adantl 466	. . . . . . . . . . . . . 14 $/\$
94	93	nnred 10571	. . . . . . . . . . . . 13 $/\$
95		prmuz2 14246	. . . . . . . . . . . . . . 15
96	95	adantl 466	. . . . . . . . . . . . . 14 $/\$
97		eluz2b1 11178	. . . . . . . . . . . . . . 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 11713	. . . . . . . . . . . 12
103	102	adantl 466	. . . . . . . . . . 11 $/\$ $/\$
104	4	adantr 465	. . . . . . . . . . . . 13 $/\$
105	104	nnrpd 11280	. . . . . . . . . . . 12 $/\$
106	105	adantr 465	. . . . . . . . . . 11 $/\$ $/\$
107		efexple 23681	. . . . . . . . . . 11 $/\$ $/\$ $/\$
108	101, 103, 106, 107	syl3anc 1228	. . . . . . . . . 10 $/\$ $/\$
109	9	nnzd 10989	. . . . . . . . . . 11 $/\$ $/\$
110	84	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
111	104	nnred 10571	. . . . . . . . . . . . . . . 16 $/\$
112		1red 9628	. . . . . . . . . . . . . . . . 17 $/\$
113	37	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
114		1lt2 10723	. . . . . . . . . . . . . . . . . 18
115	114	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
116		nnre 10563	. . . . . . . . . . . . . . . . . . . 20
117	116	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
118		0le2 10647	. . . . . . . . . . . . . . . . . . . . 21
119	37, 118	pm3.2i 455	. . . . . . . . . . . . . . . . . . . 20 $/\$
120	119	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
121		nnge1 10582	. . . . . . . . . . . . . . . . . . . 20
122	121	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
123		lemul2a 10418	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
124	112, 117, 120, 122, 123	syl31anc 1231	. . . . . . . . . . . . . . . . . 18 $/\$
125	69, 124	syl5eqbrr 4490	. . . . . . . . . . . . . . . . 17 $/\$
126	112, 113, 111, 115, 125	ltletrd 9759	. . . . . . . . . . . . . . . 16 $/\$
127	111, 126	rplogcld 23139	. . . . . . . . . . . . . . 15 $/\$
128	94, 99	rplogcld 23139	. . . . . . . . . . . . . . 15 $/\$
129	127, 128	rpdivcld 11298	. . . . . . . . . . . . . 14 $/\$
130	129	rpred 11281	. . . . . . . . . . . . 13 $/\$
131	130	flcld 11937	. . . . . . . . . . . 12 $/\$
132	131	adantr 465	. . . . . . . . . . 11 $/\$ $/\$
133		elfz 11703	. . . . . . . . . . 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 10571	. . . . . . . . 9 $/\$ $/\$
139	137, 138	ltnled 9749	. . . . . . . 8 $/\$ $/\$
140	136, 139	bitr4d 256	. . . . . . 7 $/\$ $/\$
141	16	rpge0d 11285	. . . . . . . . . . . . 13 $/\$ $/\$
142	141	adantrr 716	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
143	11	nngt0d 10600	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
144		ltdivmul 10438	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
145	137, 49, 138, 143, 144	syl112anc 1232	. . . . . . . . . . . . . . . 16 $/\$ $/\$
146	63	mulid1d 9630	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
147	146	breq2d 4468	. . . . . . . . . . . . . . . 16 $/\$ $/\$
148	145, 147	bitrd 253	. . . . . . . . . . . . . . 15 $/\$ $/\$
149	148	biimprd 223	. . . . . . . . . . . . . 14 $/\$ $/\$
150	149	impr 619	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
151		0p1e1 10668	. . . . . . . . . . . . 13
152	150, 151	syl6breqr 4496	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
153	17	adantrr 716	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
154		0z 10896	. . . . . . . . . . . . 13
155		flbi 11954	. . . . . . . . . . . . 13 $/\$ $/\$
156	153, 154, 155	sylancl 662	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
157	142, 152, 156	mpbir2and 922	. . . . . . . . . . 11 $/\$ $/\$ $/\$
158	24	rpge0d 11285	. . . . . . . . . . . . . . 15 $/\$ $/\$
159	158	adantrr 716	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
160	116, 21	ltaddrp2d 11311	. . . . . . . . . . . . . . . . . . . 20
161	61	2timesd 10802	. . . . . . . . . . . . . . . . . . . 20
162	160, 161	breqtrrd 4482	. . . . . . . . . . . . . . . . . . 19
163	162	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
164	116	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
165		lttr 9678	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
166	164, 137, 138, 165	syl3anc 1228	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
167	163, 166	mpand 675	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
168		ltdivmul 10438	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
169	164, 49, 138, 143, 168	syl112anc 1232	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
170	146	breq2d 4468	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
171	169, 170	bitrd 253	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
172	167, 171	sylibrd 234	. . . . . . . . . . . . . . . 16 $/\$ $/\$
173	172	impr 619	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
174	173, 151	syl6breqr 4496	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
175	25	adantrr 716	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
176		flbi 11954	. . . . . . . . . . . . . . 15 $/\$ $/\$
177	175, 154, 176	sylancl 662	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
178	159, 174, 177	mpbir2and 922	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
179	178	oveq2d 6312	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
180		2t0e0 10712	. . . . . . . . . . . 12
181	179, 180	syl6eq 2514	. . . . . . . . . . 11 $/\$ $/\$ $/\$
182	157, 181	oveq12d 6314	. . . . . . . . . 10 $/\$ $/\$ $/\$
183		0m0e0 10666	. . . . . . . . . 10
184	182, 183	syl6eq 2514	. . . . . . . . 9 $/\$ $/\$ $/\$
185		0le0 10646	. . . . . . . . 9
186	184, 185	syl6eqbr 4493	. . . . . . . 8 $/\$ $/\$ $/\$
187	186	expr 615	. . . . . . 7 $/\$ $/\$
188	140, 187	sylbid 215	. . . . . 6 $/\$ $/\$
189		iffalse 3953	. . . . . . . 8
190	189	eqcomd 2465	. . . . . . 7
191	190	breq2d 4468	. . . . . 6
192	188, 191	mpbidi 216	. . . . 5 $/\$ $/\$
193	90, 192	pm2.61d 158	. . . 4 $/\$ $/\$
194	1, 30, 34, 193	fsumle 13624	. . 3 $/\$
195		pcbcctr 23676	. . 3 $/\$
196	131	zred 10990	. . . . . . . 8 $/\$
197		flle 11938	. . . . . . . . 9
198	130, 197	syl 16	. . . . . . . 8 $/\$
199	104	nnnn0d 10873	. . . . . . . . . . . . . 14 $/\$
200	93, 199	nnexpcld 12333	. . . . . . . . . . . . 13 $/\$
201	200	nnred 10571	. . . . . . . . . . . 12 $/\$
202		bernneq3 12296	. . . . . . . . . . . . 13 $/\$
203	96, 199, 202	syl2anc 661	. . . . . . . . . . . 12 $/\$
204	111, 201, 203	ltled 9750	. . . . . . . . . . 11 $/\$
205	105	reeflogd 23134	. . . . . . . . . . 11 $/\$
206	93	nnrpd 11280	. . . . . . . . . . . . 13 $/\$
207	104	nnzd 10989	. . . . . . . . . . . . 13 $/\$
208		reexplog 23104	. . . . . . . . . . . . 13 $/\$
209	206, 207, 208	syl2anc 661	. . . . . . . . . . . 12 $/\$
210	209	eqcomd 2465	. . . . . . . . . . 11 $/\$
211	204, 205, 210	3brtr4d 4486	. . . . . . . . . 10 $/\$
212	105	relogcld 23133	. . . . . . . . . . 11 $/\$
213	128	rpred 11281	. . . . . . . . . . . 12 $/\$
214	111, 213	remulcld 9641	. . . . . . . . . . 11 $/\$
215		efle 13864	. . . . . . . . . . 11 $/\$
216	212, 214, 215	syl2anc 661	. . . . . . . . . 10 $/\$
217	211, 216	mpbird 232	. . . . . . . . 9 $/\$
218	212, 111, 128	ledivmul2d 11331	. . . . . . . . 9 $/\$
219	217, 218	mpbird 232	. . . . . . . 8 $/\$
220	196, 130, 111, 198, 219	letrd 9756	. . . . . . 7 $/\$
221		eluz 11119	. . . . . . . 8 $/\$
222	131, 207, 221	syl2anc 661	. . . . . . 7 $/\$
223	220, 222	mpbird 232	. . . . . 6 $/\$
224		fzss2 11748	. . . . . 6
225	223, 224	syl 16	. . . . 5 $/\$
226		sumhash 14426	. . . . 5 $/\$
227	1, 225, 226	syl2anc 661	. . . 4 $/\$
228	129	rprege0d 11288	. . . . 5 $/\$ $/\$
229		flge0nn0 11956	. . . . 5 $/\$
230		hashfz1 12421	. . . . 5
231	228, 229, 230	3syl 20	. . . 4 $/\$
232	227, 231	eqtr2d 2499	. . 3 $/\$
233	194, 195, 232	3brtr4d 4486	. 2 $/\$
234		simpr 461	. . . . 5 $/\$
235		nnnn0 10823	. . . . . . 7
236		fzctr 11812	. . . . . . 7
237		bccl2 12403	. . . . . . 7
238	235, 236, 237	3syl 20	. . . . . 6
239	238	adantr 465	. . . . 5 $/\$
240	234, 239	pccld 14385	. . . 4 $/\$
241	240	nn0zd 10988	. . 3 $/\$
242		efexple 23681	. . 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 1395

wcel 1819

wss 3471

cif 3944 class class class wbr 4456

cfv 5594 (class class class)co 6296

cfn 7535

cc 9507

cr 9508

cc0 9509

c1 9510

caddc 9512

cmul 9514

clt 9645

cle 9646

cmin 9824

cdiv 10227

cn 10556

c2 10606

cn0 10816

cz 10885

cuz 11106

crp 11245

cfz 11697

cfl 11929

cexp 12168

cbc 12382

chash 12407

csu 13519

ce 13808

cprime 14228

cpc 14371

clog 23067

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-inf2 8075 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587 ax-addf 9588 ax-mulf 9589

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-fal 1401 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-iin 4335 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-se 4848 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-isom 5603 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-of 6539 df-om 6700 df-1st 6799 df-2nd 6800 df-supp 6918 df-recs 7060 df-rdg 7094 df-1o 7148 df-2o 7149 df-oadd 7152 df-er 7329 df-map 7440 df-pm 7441 df-ixp 7489 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-fsupp 7848 df-fi 7889 df-sup 7919 df-oi 7953 df-card 8337 df-cda 8565 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-2 10615 df-3 10616 df-4 10617 df-5 10618 df-6 10619 df-7 10620 df-8 10621 df-9 10622 df-10 10623 df-n0 10817 df-z 10886 df-dec 11001 df-uz 11107 df-q 11208 df-rp 11246 df-xneg 11343 df-xadd 11344 df-xmul 11345 df-ioo 11558 df-ioc 11559 df-ico 11560 df-icc 11561 df-fz 11698 df-fzo 11821 df-fl 11931 df-mod 11999 df-seq 12110 df-exp 12169 df-fac 12356 df-bc 12383 df-hash 12408 df-shft 12911 df-cj 12943 df-re 12944 df-im 12945 df-sqrt 13079 df-abs 13080 df-limsup 13305 df-clim 13322 df-rlim 13323 df-sum 13520 df-ef 13814 df-sin 13816 df-cos 13817 df-pi 13819 df-dvds 13998 df-gcd 14156 df-prm 14229 df-pc 14372 df-struct 14645 df-ndx 14646 df-slot 14647 df-base 14648 df-sets 14649 df-ress 14650 df-plusg 14724 df-mulr 14725 df-starv 14726 df-sca 14727 df-vsca 14728 df-ip 14729 df-tset 14730 df-ple 14731 df-ds 14733 df-unif 14734 df-hom 14735 df-cco 14736 df-rest 14839 df-topn 14840 df-0g 14858 df-gsum 14859 df-topgen 14860 df-pt 14861 df-prds 14864 df-xrs 14918 df-qtop 14923 df-imas 14924 df-xps 14926 df-mre 15002 df-mrc 15003 df-acs 15005 df-mgm 15998 df-sgrp 16037 df-mnd 16047 df-submnd 16093 df-mulg 16186 df-cntz 16481 df-cmn 16926 df-psmet 18537 df-xmet 18538 df-met 18539 df-bl 18540 df-mopn 18541 df-fbas 18542 df-fg 18543 df-cnfld 18547 df-top 19525 df-bases 19527 df-topon 19528 df-topsp 19529 df-cld 19646 df-ntr 19647 df-cls 19648 df-nei 19725 df-lp 19763 df-perf 19764 df-cn 19854 df-cnp 19855 df-haus 19942 df-tx 20188 df-hmeo 20381 df-fil 20472 df-fm 20564 df-flim 20565 df-flf 20566 df-xms 20948 df-ms 20949 df-tms 20950 df-cncf 21507 df-limc 22395 df-dv 22396 df-log 23069

This theorem is referenced by: bposlem5 23688 bposlem6 23689 chebbnd1lem1 23779

W3C validator