bposlem1 - Metamath Proof Explorer

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

Theorem bposlem1 24212

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 12186	. . . 4 $/\$
2		2nn 10767	. . . . . . . . . . 11
3		nnmulcl 10632	. . . . . . . . . . 11 $/\$
4	2, 3	mpan 676	. . . . . . . . . 10
5	4	ad2antrr 732	. . . . . . . . 9 $/\$ $/\$
6		prmnn 14625	. . . . . . . . . . 11
7	6	ad2antlr 733	. . . . . . . . . 10 $/\$ $/\$
8		elfznn 11828	. . . . . . . . . . . 12
9	8	adantl 468	. . . . . . . . . . 11 $/\$ $/\$
10	9	nnnn0d 10925	. . . . . . . . . 10 $/\$ $/\$
11	7, 10	nnexpcld 12437	. . . . . . . . 9 $/\$ $/\$
12		nnrp 11311	. . . . . . . . . 10
13		nnrp 11311	. . . . . . . . . 10
14		rpdivcl 11325	. . . . . . . . . 10 $/\$
15	12, 13, 14	syl2an 480	. . . . . . . . 9 $/\$
16	5, 11, 15	syl2anc 667	. . . . . . . 8 $/\$ $/\$
17	16	rpred 11341	. . . . . . 7 $/\$ $/\$
18	17	flcld 12034	. . . . . 6 $/\$ $/\$
19		2z 10969	. . . . . . 7
20		simpll 760	. . . . . . . . . 10 $/\$ $/\$
21		nnrp 11311	. . . . . . . . . . 11
22		rpdivcl 11325	. . . . . . . . . . 11 $/\$
23	21, 13, 22	syl2an 480	. . . . . . . . . 10 $/\$
24	20, 11, 23	syl2anc 667	. . . . . . . . 9 $/\$ $/\$
25	24	rpred 11341	. . . . . . . 8 $/\$ $/\$
26	25	flcld 12034	. . . . . . 7 $/\$ $/\$
27		zmulcl 10985	. . . . . . 7 $/\$
28	19, 26, 27	sylancr 669	. . . . . 6 $/\$ $/\$
29	18, 28	zsubcld 11045	. . . . 5 $/\$ $/\$
30	29	zred 11040	. . . 4 $/\$ $/\$
31		1re 9642	. . . . . 6
32		0re 9643	. . . . . 6
33	31, 32	keepel 3948	. . . . 5
34	33	a1i 11	. . . 4 $/\$ $/\$
35	28	zred 11040	. . . . . . . . . 10 $/\$ $/\$
36	17, 35	resubcld 10047	. . . . . . . . 9 $/\$ $/\$
37		2re 10679	. . . . . . . . . 10
38	37	a1i 11	. . . . . . . . 9 $/\$ $/\$
39	18	zred 11040	. . . . . . . . . 10 $/\$ $/\$
40		flle 12035	. . . . . . . . . . 11
41	17, 40	syl 17	. . . . . . . . . 10 $/\$ $/\$
42	39, 17, 35, 41	lesub1dd 10229	. . . . . . . . 9 $/\$ $/\$
43		resubcl 9938	. . . . . . . . . . . . 13 $/\$
44	25, 31, 43	sylancl 668	. . . . . . . . . . . 12 $/\$ $/\$
45		remulcl 9624	. . . . . . . . . . . 12 $/\$
46	37, 44, 45	sylancr 669	. . . . . . . . . . 11 $/\$ $/\$
47		flltp1 12036	. . . . . . . . . . . . . 14
48	25, 47	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
49		1red 9658	. . . . . . . . . . . . . 14 $/\$ $/\$
50	26	zred 11040	. . . . . . . . . . . . . 14 $/\$ $/\$
51	25, 49, 50	ltsubaddd 10209	. . . . . . . . . . . . 13 $/\$ $/\$
52	48, 51	mpbird 236	. . . . . . . . . . . 12 $/\$ $/\$
53		2pos 10701	. . . . . . . . . . . . . . 15
54	37, 53	pm3.2i 457	. . . . . . . . . . . . . 14 $/\$
55		ltmul2 10456	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
56	54, 55	mp3an3 1353	. . . . . . . . . . . . 13 $/\$
57	44, 50, 56	syl2anc 667	. . . . . . . . . . . 12 $/\$ $/\$
58	52, 57	mpbid 214	. . . . . . . . . . 11 $/\$ $/\$
59	46, 35, 17, 58	ltsub2dd 10226	. . . . . . . . . 10 $/\$ $/\$
60		2cnd 10682	. . . . . . . . . . . . 13 $/\$ $/\$
61		nncn 10617	. . . . . . . . . . . . . 14
62	61	ad2antrr 732	. . . . . . . . . . . . 13 $/\$ $/\$
63	11	nncnd 10625	. . . . . . . . . . . . 13 $/\$ $/\$
64	11	nnne0d 10654	. . . . . . . . . . . . 13 $/\$ $/\$
65	60, 62, 63, 64	divassd 10418	. . . . . . . . . . . 12 $/\$ $/\$
66	25	recnd 9669	. . . . . . . . . . . . . 14 $/\$ $/\$
67		1cnd 9659	. . . . . . . . . . . . . 14 $/\$ $/\$
68	60, 66, 67	subdid 10074	. . . . . . . . . . . . 13 $/\$ $/\$
69		2t1e2 10758	. . . . . . . . . . . . . 14
70	69	oveq2i 6301	. . . . . . . . . . . . 13
71	68, 70	syl6eq 2501	. . . . . . . . . . . 12 $/\$ $/\$
72	65, 71	oveq12d 6308	. . . . . . . . . . 11 $/\$ $/\$
73		remulcl 9624	. . . . . . . . . . . . . 14 $/\$
74	37, 25, 73	sylancr 669	. . . . . . . . . . . . 13 $/\$ $/\$
75	74	recnd 9669	. . . . . . . . . . . 12 $/\$ $/\$
76		2cn 10680	. . . . . . . . . . . 12
77		nncan 9903	. . . . . . . . . . . 12 $/\$
78	75, 76, 77	sylancl 668	. . . . . . . . . . 11 $/\$ $/\$
79	72, 78	eqtrd 2485	. . . . . . . . . 10 $/\$ $/\$
80	59, 79	breqtrd 4427	. . . . . . . . 9 $/\$ $/\$
81	30, 36, 38, 42, 80	lelttrd 9793	. . . . . . . 8 $/\$ $/\$
82		df-2 10668	. . . . . . . 8
83	81, 82	syl6breq 4442	. . . . . . 7 $/\$ $/\$
84		1z 10967	. . . . . . . 8
85		zleltp1 10987	. . . . . . . 8 $/\$
86	29, 84, 85	sylancl 668	. . . . . . 7 $/\$ $/\$
87	83, 86	mpbird 236	. . . . . 6 $/\$ $/\$
88		iftrue 3887	. . . . . . 7
89	88	breq2d 4414	. . . . . 6
90	87, 89	syl5ibrcom 226	. . . . 5 $/\$ $/\$
91	9	nnge1d 10652	. . . . . . . . . . 11 $/\$ $/\$
92	91	biantrurd 511	. . . . . . . . . 10 $/\$ $/\$ $/\$
93	6	adantl 468	. . . . . . . . . . . . . 14 $/\$
94	93	nnred 10624	. . . . . . . . . . . . 13 $/\$
95		prmuz2 14642	. . . . . . . . . . . . . . 15
96	95	adantl 468	. . . . . . . . . . . . . 14 $/\$
97		eluz2b1 11230	. . . . . . . . . . . . . . 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 11800	. . . . . . . . . . . 12
103	102	adantl 468	. . . . . . . . . . 11 $/\$ $/\$
104	4	adantr 467	. . . . . . . . . . . . 13 $/\$
105	104	nnrpd 11339	. . . . . . . . . . . 12 $/\$
106	105	adantr 467	. . . . . . . . . . 11 $/\$ $/\$
107		efexple 24209	. . . . . . . . . . 11 $/\$ $/\$ $/\$
108	101, 103, 106, 107	syl3anc 1268	. . . . . . . . . 10 $/\$ $/\$
109	9	nnzd 11039	. . . . . . . . . . 11 $/\$ $/\$
110	84	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
111	104	nnred 10624	. . . . . . . . . . . . . . . 16 $/\$
112		1red 9658	. . . . . . . . . . . . . . . . 17 $/\$
113	37	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
114		1lt2 10776	. . . . . . . . . . . . . . . . . 18
115	114	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
116		nnre 10616	. . . . . . . . . . . . . . . . . . . 20
117	116	adantr 467	. . . . . . . . . . . . . . . . . . 19 $/\$
118		0le2 10700	. . . . . . . . . . . . . . . . . . . . 21
119	37, 118	pm3.2i 457	. . . . . . . . . . . . . . . . . . . 20 $/\$
120	119	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
121		nnge1 10635	. . . . . . . . . . . . . . . . . . . 20
122	121	adantr 467	. . . . . . . . . . . . . . . . . . 19 $/\$
123		lemul2a 10460	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
124	112, 117, 120, 122, 123	syl31anc 1271	. . . . . . . . . . . . . . . . . 18 $/\$
125	69, 124	syl5eqbrr 4437	. . . . . . . . . . . . . . . . 17 $/\$
126	112, 113, 111, 115, 125	ltletrd 9795	. . . . . . . . . . . . . . . 16 $/\$
127	111, 126	rplogcld 23578	. . . . . . . . . . . . . . 15 $/\$
128	94, 99	rplogcld 23578	. . . . . . . . . . . . . . 15 $/\$
129	127, 128	rpdivcld 11358	. . . . . . . . . . . . . 14 $/\$
130	129	rpred 11341	. . . . . . . . . . . . 13 $/\$
131	130	flcld 12034	. . . . . . . . . . . 12 $/\$
132	131	adantr 467	. . . . . . . . . . 11 $/\$ $/\$
133		elfz 11790	. . . . . . . . . . 11 $/\$ $/\$ $/\$
134	109, 110, 132, 133	syl3anc 1268	. . . . . . . . . 10 $/\$ $/\$ $/\$
135	92, 108, 134	3bitr4rd 290	. . . . . . . . 9 $/\$ $/\$
136	135	notbid 296	. . . . . . . 8 $/\$ $/\$
137	111	adantr 467	. . . . . . . . 9 $/\$ $/\$
138	11	nnred 10624	. . . . . . . . 9 $/\$ $/\$
139	137, 138	ltnled 9782	. . . . . . . 8 $/\$ $/\$
140	136, 139	bitr4d 260	. . . . . . 7 $/\$ $/\$
141	16	rpge0d 11345	. . . . . . . . . . . . 13 $/\$ $/\$
142	141	adantrr 723	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
143	11	nngt0d 10653	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
144		ltdivmul 10480	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
145	137, 49, 138, 143, 144	syl112anc 1272	. . . . . . . . . . . . . . . 16 $/\$ $/\$
146	63	mulid1d 9660	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
147	146	breq2d 4414	. . . . . . . . . . . . . . . 16 $/\$ $/\$
148	145, 147	bitrd 257	. . . . . . . . . . . . . . 15 $/\$ $/\$
149	148	biimprd 227	. . . . . . . . . . . . . 14 $/\$ $/\$
150	149	impr 625	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
151		0p1e1 10721	. . . . . . . . . . . . 13
152	150, 151	syl6breqr 4443	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
153	17	adantrr 723	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
154		0z 10948	. . . . . . . . . . . . 13
155		flbi 12051	. . . . . . . . . . . . 13 $/\$ $/\$
156	153, 154, 155	sylancl 668	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
157	142, 152, 156	mpbir2and 933	. . . . . . . . . . 11 $/\$ $/\$ $/\$
158	24	rpge0d 11345	. . . . . . . . . . . . . . 15 $/\$ $/\$
159	158	adantrr 723	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
160	116, 21	ltaddrp2d 11372	. . . . . . . . . . . . . . . . . . . 20
161	61	2timesd 10855	. . . . . . . . . . . . . . . . . . . 20
162	160, 161	breqtrrd 4429	. . . . . . . . . . . . . . . . . . 19
163	162	ad2antrr 732	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
164	116	ad2antrr 732	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
165		lttr 9710	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
166	164, 137, 138, 165	syl3anc 1268	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
167	163, 166	mpand 681	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
168		ltdivmul 10480	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
169	164, 49, 138, 143, 168	syl112anc 1272	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
170	146	breq2d 4414	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
171	169, 170	bitrd 257	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
172	167, 171	sylibrd 238	. . . . . . . . . . . . . . . 16 $/\$ $/\$
173	172	impr 625	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
174	173, 151	syl6breqr 4443	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
175	25	adantrr 723	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
176		flbi 12051	. . . . . . . . . . . . . . 15 $/\$ $/\$
177	175, 154, 176	sylancl 668	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
178	159, 174, 177	mpbir2and 933	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
179	178	oveq2d 6306	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
180		2t0e0 10765	. . . . . . . . . . . 12
181	179, 180	syl6eq 2501	. . . . . . . . . . 11 $/\$ $/\$ $/\$
182	157, 181	oveq12d 6308	. . . . . . . . . 10 $/\$ $/\$ $/\$
183		0m0e0 10719	. . . . . . . . . 10
184	182, 183	syl6eq 2501	. . . . . . . . 9 $/\$ $/\$ $/\$
185		0le0 10699	. . . . . . . . 9
186	184, 185	syl6eqbr 4440	. . . . . . . 8 $/\$ $/\$ $/\$
187	186	expr 620	. . . . . . 7 $/\$ $/\$
188	140, 187	sylbid 219	. . . . . 6 $/\$ $/\$
189		iffalse 3890	. . . . . . . 8
190	189	eqcomd 2457	. . . . . . 7
191	190	breq2d 4414	. . . . . 6
192	188, 191	mpbidi 220	. . . . 5 $/\$ $/\$
193	90, 192	pm2.61d 162	. . . 4 $/\$ $/\$
194	1, 30, 34, 193	fsumle 13859	. . 3 $/\$
195		pcbcctr 24204	. . 3 $/\$
196	131	zred 11040	. . . . . . . 8 $/\$
197		flle 12035	. . . . . . . . 9
198	130, 197	syl 17	. . . . . . . 8 $/\$
199	104	nnnn0d 10925	. . . . . . . . . . . . . 14 $/\$
200	93, 199	nnexpcld 12437	. . . . . . . . . . . . 13 $/\$
201	200	nnred 10624	. . . . . . . . . . . 12 $/\$
202		bernneq3 12400	. . . . . . . . . . . . 13 $/\$
203	96, 199, 202	syl2anc 667	. . . . . . . . . . . 12 $/\$
204	111, 201, 203	ltled 9783	. . . . . . . . . . 11 $/\$
205	105	reeflogd 23573	. . . . . . . . . . 11 $/\$
206	93	nnrpd 11339	. . . . . . . . . . . . 13 $/\$
207	104	nnzd 11039	. . . . . . . . . . . . 13 $/\$
208		reexplog 23544	. . . . . . . . . . . . 13 $/\$
209	206, 207, 208	syl2anc 667	. . . . . . . . . . . 12 $/\$
210	209	eqcomd 2457	. . . . . . . . . . 11 $/\$
211	204, 205, 210	3brtr4d 4433	. . . . . . . . . 10 $/\$
212	105	relogcld 23572	. . . . . . . . . . 11 $/\$
213	128	rpred 11341	. . . . . . . . . . . 12 $/\$
214	111, 213	remulcld 9671	. . . . . . . . . . 11 $/\$
215		efle 14172	. . . . . . . . . . 11 $/\$
216	212, 214, 215	syl2anc 667	. . . . . . . . . 10 $/\$
217	211, 216	mpbird 236	. . . . . . . . 9 $/\$
218	212, 111, 128	ledivmul2d 11392	. . . . . . . . 9 $/\$
219	217, 218	mpbird 236	. . . . . . . 8 $/\$
220	196, 130, 111, 198, 219	letrd 9792	. . . . . . 7 $/\$
221		eluz 11172	. . . . . . . 8 $/\$
222	131, 207, 221	syl2anc 667	. . . . . . 7 $/\$
223	220, 222	mpbird 236	. . . . . 6 $/\$
224		fzss2 11838	. . . . . 6
225	223, 224	syl 17	. . . . 5 $/\$
226		sumhash 14841	. . . . 5 $/\$
227	1, 225, 226	syl2anc 667	. . . 4 $/\$
228	129	rprege0d 11348	. . . . 5 $/\$ $/\$
229		flge0nn0 12054	. . . . 5 $/\$
230		hashfz1 12529	. . . . 5
231	228, 229, 230	3syl 18	. . . 4 $/\$
232	227, 231	eqtr2d 2486	. . 3 $/\$
233	194, 195, 232	3brtr4d 4433	. 2 $/\$
234		simpr 463	. . . . 5 $/\$
235		nnnn0 10876	. . . . . . 7
236		fzctr 11903	. . . . . . 7
237		bccl2 12508	. . . . . . 7
238	235, 236, 237	3syl 18	. . . . . 6
239	238	adantr 467	. . . . 5 $/\$
240	234, 239	pccld 14800	. . . 4 $/\$
241	240	nn0zd 11038	. . 3 $/\$
242		efexple 24209	. . 3 $/\$ $/\$ $/\$
243	94, 99, 241, 105, 242	syl211anc 1274	. 2 $/\$
244	233, 243	mpbird 236	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $/\$ wa 371

wceq 1444

wcel 1887

wss 3404

cif 3881 class class class wbr 4402

cfv 5582 (class class class)co 6290

cfn 7569

cc 9537

cr 9538

cc0 9539

c1 9540

caddc 9542

cmul 9544

clt 9675

cle 9676

cmin 9860

cdiv 10269

cn 10609

c2 10659

cn0 10869

cz 10937

cuz 11159

crp 11302

cfz 11784

cfl 12026

cexp 12272

cbc 12487

chash 12515

csu 13752

ce 14114

cprime 14622

cpc 14786

clog 23504

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-inf2 8146 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616 ax-pre-sup 9617 ax-addf 9618 ax-mulf 9619

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-fal 1450 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-iin 4281 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-se 4794 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-isom 5591 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-of 6531 df-om 6693 df-1st 6793 df-2nd 6794 df-supp 6915 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-2o 7183 df-oadd 7186 df-er 7363 df-map 7474 df-pm 7475 df-ixp 7523 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-fsupp 7884 df-fi 7925 df-sup 7956 df-inf 7957 df-oi 8025 df-card 8373 df-cda 8598 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-div 10270 df-nn 10610 df-2 10668 df-3 10669 df-4 10670 df-5 10671 df-6 10672 df-7 10673 df-8 10674 df-9 10675 df-10 10676 df-n0 10870 df-z 10938 df-dec 11052 df-uz 11160 df-q 11265 df-rp 11303 df-xneg 11409 df-xadd 11410 df-xmul 11411 df-ioo 11639 df-ioc 11640 df-ico 11641 df-icc 11642 df-fz 11785 df-fzo 11916 df-fl 12028 df-mod 12097 df-seq 12214 df-exp 12273 df-fac 12460 df-bc 12488 df-hash 12516 df-shft 13130 df-cj 13162 df-re 13163 df-im 13164 df-sqrt 13298 df-abs 13299 df-limsup 13526 df-clim 13552 df-rlim 13553 df-sum 13753 df-ef 14121 df-sin 14123 df-cos 14124 df-pi 14126 df-dvds 14306 df-gcd 14469 df-prm 14623 df-pc 14787 df-struct 15123 df-ndx 15124 df-slot 15125 df-base 15126 df-sets 15127 df-ress 15128 df-plusg 15203 df-mulr 15204 df-starv 15205 df-sca 15206 df-vsca 15207 df-ip 15208 df-tset 15209 df-ple 15210 df-ds 15212 df-unif 15213 df-hom 15214 df-cco 15215 df-rest 15321 df-topn 15322 df-0g 15340 df-gsum 15341 df-topgen 15342 df-pt 15343 df-prds 15346 df-xrs 15400 df-qtop 15406 df-imas 15407 df-xps 15410 df-mre 15492 df-mrc 15493 df-acs 15495 df-mgm 16488 df-sgrp 16527 df-mnd 16537 df-submnd 16583 df-mulg 16676 df-cntz 16971 df-cmn 17432 df-psmet 18962 df-xmet 18963 df-met 18964 df-bl 18965 df-mopn 18966 df-fbas 18967 df-fg 18968 df-cnfld 18971 df-top 19921 df-bases 19922 df-topon 19923 df-topsp 19924 df-cld 20034 df-ntr 20035 df-cls 20036 df-nei 20114 df-lp 20152 df-perf 20153 df-cn 20243 df-cnp 20244 df-haus 20331 df-tx 20577 df-hmeo 20770 df-fil 20861 df-fm 20953 df-flim 20954 df-flf 20955 df-xms 21335 df-ms 21336 df-tms 21337 df-cncf 21910 df-limc 22821 df-dv 22822 df-log 23506

This theorem is referenced by: bposlem5 24216 bposlem6 24217 chebbnd1lem1 24307

W3C validator