log2tlbndlog2 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > log2tlbndlog2		Unicode version

Theorem log2tlbndlog2 16082

Description: Bound the error term in the series of the hypothesis. The presence of the hypothesis here is a temporary measure until it can be proved as log2cnv . (Contributed by Mario Carneiro, 7-Apr-2015.)

**Hypothesis**
Ref	Expression
log2tlbnd.log2cnv

**Assertion**
Ref	Expression
log2tlbndlog2

Distinct variable group:

**Proof of Theorem log2tlbndlog2**
Step	Hyp	Ref	Expression
1		0zd 9656	. . . . 5
2		nn0z 9664	. . . . . 6
3		peano2zm 9682	. . . . . 6
4	2, 3	syl 14	. . . . 5
5	1, 4	fzfigd 10868	. . . 4
6		elfznn0 10521	. . . . 5
7		2re 9374	. . . . . . 7
8		3nn 9467	. . . . . . . . 9
9		2nn0 9580	. . . . . . . . . . 11
10		simpr 110	. . . . . . . . . . 11 $/\$
11		nn0mulcl 9599	. . . . . . . . . . 11 $/\$
12	9, 10, 11	sylancr 418	. . . . . . . . . 10 $/\$
13		nn0p1nn 9602	. . . . . . . . . 10
14	12, 13	syl 14	. . . . . . . . 9 $/\$
15		nnmulcl 9325	. . . . . . . . 9 $/\$
16	8, 14, 15	sylancr 418	. . . . . . . 8 $/\$
17		9nn 9473	. . . . . . . . 9
18		nnexpcl 10989	. . . . . . . . 9 $/\$
19	17, 10, 18	sylancr 418	. . . . . . . 8 $/\$
20	16, 19	nnmulcld 9353	. . . . . . 7 $/\$
21		nndivre 9340	. . . . . . 7 $/\$
22	7, 20, 21	sylancr 418	. . . . . 6 $/\$
23	22	recnd 8354	. . . . 5 $/\$
24	6, 23	sylan2 286	. . . 4 $/\$
25	5, 24	fsumcl 12167	. . 3
26		eqid 2238	. . . . 5
27		eluznn0 9999	. . . . . 6 $/\$
28		eqid 2238	. . . . . . 7
29		oveq2 6093	. . . . . . . . . . 11
30	29	oveq1d 6100	. . . . . . . . . 10
31	30	oveq2d 6101	. . . . . . . . 9
32		oveq2 6093	. . . . . . . . 9
33	31, 32	oveq12d 6103	. . . . . . . 8
34	33	oveq2d 6101	. . . . . . 7
35		id 19	. . . . . . 7
36	7	a1i 9	. . . . . . . 8
37		3rp 10060	. . . . . . . . . . 11
38	37	a1i 9	. . . . . . . . . 10
39		nn0re 9572	. . . . . . . . . . . 12
40	36, 39	remulcld 8356	. . . . . . . . . . 11
41		0le2 9394	. . . . . . . . . . . . 13
42	41	a1i 9	. . . . . . . . . . . 12
43		nn0ge0 9588	. . . . . . . . . . . 12
44	36, 39, 42, 43	mulge0d 8949	. . . . . . . . . . 11
45	40, 44	ge0p1rpd 10128	. . . . . . . . . 10
46	38, 45	rpmulcld 10114	. . . . . . . . 9
47		9re 9391	. . . . . . . . . . 11
48		9pos 9408	. . . . . . . . . . 11
49	47, 48	elrpii 10057	. . . . . . . . . 10
50		nn0z 9664	. . . . . . . . . 10
51		rpexpcl 10995	. . . . . . . . . 10 $/\$
52	49, 50, 51	sylancr 418	. . . . . . . . 9
53	46, 52	rpmulcld 10114	. . . . . . . 8
54	36, 53	rerpdivcld 10129	. . . . . . 7
55	28, 34, 35, 54	fvmptd3 5799	. . . . . 6
56	27, 55	syl 14	. . . . 5 $/\$
57	27, 22	syldan 282	. . . . 5 $/\$
58		log2tlbnd.log2cnv	. . . . . . 7
59		seqex 10886	. . . . . . . 8
60		2rp 10059	. . . . . . . . . 10
61		relogcl 15963	. . . . . . . . . 10
62	60, 61	ax-mp 5	. . . . . . . . 9
63	62	elexi 2834	. . . . . . . 8
64	59, 63	breldm 4985	. . . . . . 7
65	58, 64	mp1i 10	. . . . . 6
66		nn0uz 9957	. . . . . . 7
67		id 19	. . . . . . 7
68	55	adantl 277	. . . . . . . 8 $/\$
69	68, 23	eqeltrd 2315	. . . . . . 7 $/\$
70	66, 67, 69	iserex 12105	. . . . . 6
71	65, 70	mpbid 147	. . . . 5
72	26, 2, 56, 57, 71	isumrecl 12196	. . . 4
73	72	recnd 8354	. . 3
74	58	a1i 9	. . . . 5
75	66, 1, 68, 23, 74	isumclim 12188	. . . 4
76	66, 26, 67, 68, 23, 65	isumsplit 12258	. . . 4
77	75, 76	eqtr3d 2273	. . 3
78	25, 73, 77	mvrladdd 8693	. 2
79	7	a1i 9	. . . . . 6 $/\$
80	41	a1i 9	. . . . . 6 $/\$
81	20	nnred 9317	. . . . . 6 $/\$
82	20	nngt0d 9348	. . . . . 6 $/\$
83		divge0 9203	. . . . . 6 $/\$ $/\$ $/\$
84	79, 80, 81, 82, 83	syl22anc 1279	. . . . 5 $/\$
85	27, 84	syldan 282	. . . 4 $/\$
86	26, 2, 56, 57, 71, 85	isumge0 12197	. . 3
87		eqid 2238	. . . . . . . 8
88		oveq2 6093	. . . . . . . . 9
89	88	oveq2d 6101	. . . . . . . 8
90	60	a1i 9	. . . . . . . . . . 11 $/\$
91	37	a1i 9	. . . . . . . . . . . 12 $/\$
92	9	a1i 9	. . . . . . . . . . . . . . . 16
93	92, 67	nn0mulcld 9625	. . . . . . . . . . . . . . 15
94		nn0p1nn 9602	. . . . . . . . . . . . . . 15
95	93, 94	syl 14	. . . . . . . . . . . . . 14
96	95	nnrpd 10095	. . . . . . . . . . . . 13
97	96	adantr 276	. . . . . . . . . . . 12 $/\$
98	91, 97	rpmulcld 10114	. . . . . . . . . . 11 $/\$
99	90, 98	rpdivcld 10115	. . . . . . . . . 10 $/\$
100	99	rpred 10097	. . . . . . . . 9 $/\$
101		1z 9670	. . . . . . . . . . . . . 14
102		znq 10024	. . . . . . . . . . . . . 14 $/\$
103	101, 17, 102	mp2an 430	. . . . . . . . . . . . 13
104		qre 10025	. . . . . . . . . . . . 13
105	103, 104	ax-mp 5	. . . . . . . . . . . 12
106	105	a1i 9	. . . . . . . . . . 11
107	106, 35	reexpcld 11128	. . . . . . . . . 10
108	107	adantl 277	. . . . . . . . 9 $/\$
109	100, 108	remulcld 8356	. . . . . . . 8 $/\$
110	87, 89, 10, 109	fvmptd3 5799	. . . . . . 7 $/\$
111		9cn 9392	. . . . . . . . . . 11
112	111	a1i 9	. . . . . . . . . 10 $/\$
113	47, 48	gt0ap0ii 8956	. . . . . . . . . . 11 #
114	113	a1i 9	. . . . . . . . . 10 $/\$ #
115	50	adantl 277	. . . . . . . . . 10 $/\$
116	112, 114, 115	exprecapd 11119	. . . . . . . . 9 $/\$
117	116	oveq2d 6101	. . . . . . . 8 $/\$
118		nn0mulcl 9599	. . . . . . . . . . . . . . 15 $/\$
119	9, 118	mpan 428	. . . . . . . . . . . . . 14
120	119, 94	syl 14	. . . . . . . . . . . . 13
121		nnmulcl 9325	. . . . . . . . . . . . 13 $/\$
122	8, 120, 121	sylancr 418	. . . . . . . . . . . 12
123		nndivre 9340	. . . . . . . . . . . 12 $/\$
124	7, 122, 123	sylancr 418	. . . . . . . . . . 11
125	124	recnd 8354	. . . . . . . . . 10
126	125	adantr 276	. . . . . . . . 9 $/\$
127	19	nncnd 9318	. . . . . . . . 9 $/\$
128	19	nnap0d 9350	. . . . . . . . 9 $/\$ #
129	126, 127, 128	divrecapd 9123	. . . . . . . 8 $/\$
130		2cnd 9377	. . . . . . . . 9 $/\$
131	122	adantr 276	. . . . . . . . . 10 $/\$
132	131	nncnd 9318	. . . . . . . . 9 $/\$
133	131	nnap0d 9350	. . . . . . . . 9 $/\$ #
134	130, 132, 127, 133, 128	divdivap1d 9152	. . . . . . . 8 $/\$
135	117, 129, 134	3eqtr2d 2277	. . . . . . 7 $/\$
136	110, 135	eqtrd 2271	. . . . . 6 $/\$
137	27, 136	syldan 282	. . . . 5 $/\$
138	131, 19	nnmulcld 9353	. . . . . . 7 $/\$
139		nndivre 9340	. . . . . . 7 $/\$
140	7, 138, 139	sylancr 418	. . . . . 6 $/\$
141	27, 140	syldan 282	. . . . 5 $/\$
142	119	adantr 276	. . . . . . . . . 10 $/\$
143	142	nn0red 9621	. . . . . . . . 9 $/\$
144	9, 27, 11	sylancr 418	. . . . . . . . . 10 $/\$
145	144	nn0red 9621	. . . . . . . . 9 $/\$
146		1red 8341	. . . . . . . . 9 $/\$
147		eluzle 9934	. . . . . . . . . . 11
148	147	adantl 277	. . . . . . . . . 10 $/\$
149		nn0re 9572	. . . . . . . . . . . 12
150	149	adantr 276	. . . . . . . . . . 11 $/\$
151	27	nn0red 9621	. . . . . . . . . . 11 $/\$
152	7	a1i 9	. . . . . . . . . . 11 $/\$
153		2pos 9395	. . . . . . . . . . . 12
154	153	a1i 9	. . . . . . . . . . 11 $/\$
155		lemul2 9187	. . . . . . . . . . 11 $/\$ $/\$ $/\$
156	150, 151, 152, 154, 155	syl112anc 1282	. . . . . . . . . 10 $/\$
157	148, 156	mpbid 147	. . . . . . . . 9 $/\$
158	143, 145, 146, 157	leadd1dd 8887	. . . . . . . 8 $/\$
159	120	adantr 276	. . . . . . . . . 10 $/\$
160	159	nnred 9317	. . . . . . . . 9 $/\$
161	27, 14	syldan 282	. . . . . . . . . 10 $/\$
162	161	nnred 9317	. . . . . . . . 9 $/\$
163		3re 9378	. . . . . . . . . 10
164	163	a1i 9	. . . . . . . . 9 $/\$
165		3pos 9398	. . . . . . . . . 10
166	165	a1i 9	. . . . . . . . 9 $/\$
167		lemul2 9187	. . . . . . . . 9 $/\$ $/\$ $/\$
168	160, 162, 164, 166, 167	syl112anc 1282	. . . . . . . 8 $/\$
169	158, 168	mpbid 147	. . . . . . 7 $/\$
170	122	adantr 276	. . . . . . . . 9 $/\$
171	170	nnred 9317	. . . . . . . 8 $/\$
172	27, 16	syldan 282	. . . . . . . . 9 $/\$
173	172	nnred 9317	. . . . . . . 8 $/\$
174	17, 27, 18	sylancr 418	. . . . . . . . 9 $/\$
175	174	nnred 9317	. . . . . . . 8 $/\$
176	174	nngt0d 9348	. . . . . . . 8 $/\$
177		lemul1 8921	. . . . . . . 8 $/\$ $/\$ $/\$
178	171, 173, 175, 176, 177	syl112anc 1282	. . . . . . 7 $/\$
179	169, 178	mpbid 147	. . . . . 6 $/\$
180	27, 138	syldan 282	. . . . . . . 8 $/\$
181	180	nnred 9317	. . . . . . 7 $/\$
182	180	nngt0d 9348	. . . . . . 7 $/\$
183	27, 81	syldan 282	. . . . . . 7 $/\$
184	27, 82	syldan 282	. . . . . . 7 $/\$
185		lediv2 9221	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
186	181, 182, 183, 184, 152, 154, 185	syl222anc 1294	. . . . . 6 $/\$
187	179, 186	mpbid 147	. . . . 5 $/\$
188		seqex 10886	. . . . . 6
189	49	a1i 9	. . . . . . . . 9
190		8nn 9472	. . . . . . . . . . . 12
191	190	a1i 9	. . . . . . . . . . 11
192	191	nnrpd 10095	. . . . . . . . . 10
193		nnexpcl 10989	. . . . . . . . . . . 12 $/\$
194	17, 193	mpan 428	. . . . . . . . . . 11
195	194	nnrpd 10095	. . . . . . . . . 10
196	192, 195	rpmulcld 10114	. . . . . . . . 9
197	189, 196	rpdivcld 10115	. . . . . . . 8
198	197	rpred 10097	. . . . . . 7
199	124, 198	remulcld 8356	. . . . . 6
200	105	recni 8338	. . . . . . . . . 10
201	200	a1i 9	. . . . . . . . 9
202		0re 8326	. . . . . . . . . . . . 13
203	47, 48	recgt0ii 9237	. . . . . . . . . . . . 13
204	202, 105, 203	ltleii 8428	. . . . . . . . . . . 12
205		absid 11837	. . . . . . . . . . . 12 $/\$
206	105, 204, 205	mp2an 430	. . . . . . . . . . 11
207		1lt9 9509	. . . . . . . . . . . . 13
208		recgt1i 9228	. . . . . . . . . . . . 13 $/\$ $/\$
209	47, 207, 208	mp2an 430	. . . . . . . . . . . 12 $/\$
210	209	simpri 113	. . . . . . . . . . 11
211	206, 210	eqbrtri 4151	. . . . . . . . . 10
212	211	a1i 9	. . . . . . . . 9
213		eqid 2238	. . . . . . . . . . 11
214	213, 88, 35, 107	fvmptd3 5799	. . . . . . . . . 10
215	27, 214	syl 14	. . . . . . . . 9 $/\$
216	201, 212, 67, 215	geolim2 12279	. . . . . . . 8
217	111	a1i 9	. . . . . . . . . . 11
218	113	a1i 9	. . . . . . . . . . 11 #
219	217, 218, 2	exprecapd 11119	. . . . . . . . . 10
220	111, 113	dividapi 9075	. . . . . . . . . . . . 13
221	220	oveq1i 6095	. . . . . . . . . . . 12
222		ax-1cn 8272	. . . . . . . . . . . . . 14
223	111, 113	pm3.2i 272	. . . . . . . . . . . . . 14 $/\$ #
224		divsubdirap 9038	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ #
225	111, 222, 223, 224	mp3an 1378	. . . . . . . . . . . . 13
226		9m1e8 9430	. . . . . . . . . . . . . 14
227	226	oveq1i 6095	. . . . . . . . . . . . 13
228	225, 227	eqtr3i 2261	. . . . . . . . . . . 12
229	221, 228	eqtr3i 2261	. . . . . . . . . . 11
230	229	a1i 9	. . . . . . . . . 10
231	219, 230	oveq12d 6103	. . . . . . . . 9
232	222	a1i 9	. . . . . . . . . 10
233	194	nncnd 9318	. . . . . . . . . 10
234		8cn 9390	. . . . . . . . . . . 12
235	234, 111, 113	divclapi 9084	. . . . . . . . . . 11
236	235	a1i 9	. . . . . . . . . 10
237	194	nnap0d 9350	. . . . . . . . . 10 #
238	190	nnap0i 9335	. . . . . . . . . . . 12 #
239	234, 111, 238, 113	divap0i 9090	. . . . . . . . . . 11 #
240	239	a1i 9	. . . . . . . . . 10 #
241	232, 233, 236, 237, 240	divdiv32apd 9146	. . . . . . . . 9
242		recdivap 9048	. . . . . . . . . . . 12 $/\$ # $/\$ $/\$ #
243	234, 238, 111, 113, 242	mp4an 431	. . . . . . . . . . 11
244	243	oveq1i 6095	. . . . . . . . . 10
245	234	a1i 9	. . . . . . . . . . 11
246	238	a1i 9	. . . . . . . . . . 11 #
247	217, 245, 233, 246, 237	divdivap1d 9152	. . . . . . . . . 10
248	244, 247	eqtrid 2283	. . . . . . . . 9
249	231, 241, 248	3eqtrd 2275	. . . . . . . 8
250	216, 249	breqtrd 4156	. . . . . . 7
251		expcl 10994	. . . . . . . . 9 $/\$
252	200, 27, 251	sylancr 418	. . . . . . . 8 $/\$
253	215, 252	eqeltrd 2315	. . . . . . 7 $/\$
254	27, 110	syldan 282	. . . . . . . 8 $/\$
255	215	oveq2d 6101	. . . . . . . 8 $/\$
256	254, 255	eqtr4d 2274	. . . . . . 7 $/\$
257	26, 2, 125, 250, 253, 256	isermulc2 12106	. . . . . 6
258		breldmg 4987	. . . . . 6 $/\$ $/\$
259	188, 199, 257, 258	mp3an2i 1383	. . . . 5
260	26, 2, 56, 57, 137, 141, 187, 71, 259	isumle 12262	. . . 4
261	141	recnd 8354	. . . . 5 $/\$
262		3cn 9379	. . . . . . . . . . . 12
263		4cn 9382	. . . . . . . . . . . 12
264		2cn 9375	. . . . . . . . . . . 12
265		4ap0 9403	. . . . . . . . . . . 12 #
266		3ap0 9400	. . . . . . . . . . . 12 #
267		2ap0 9397	. . . . . . . . . . . 12 #
268	262, 263, 264, 262, 265, 266, 267	divdivdivapi 9105	. . . . . . . . . . 11
269		3t3e9 9462	. . . . . . . . . . . 12
270		4t2e8 9463	. . . . . . . . . . . 12
271	269, 270	oveq12i 6097	. . . . . . . . . . 11
272	268, 271	eqtri 2259	. . . . . . . . . 10
273	272	oveq2i 6096	. . . . . . . . 9
274	262, 263, 265	divclapi 9084	. . . . . . . . . 10
275	264, 262, 266	divclapi 9084	. . . . . . . . . 10
276	264, 262, 267, 266	divap0i 9090	. . . . . . . . . 10 #
277	274, 275, 276	divcanap2i 9085	. . . . . . . . 9
278	273, 277	eqtr3i 2261	. . . . . . . 8
279	278	oveq1i 6095	. . . . . . 7
280		2cnd 9377	. . . . . . . . . 10
281	262	a1i 9	. . . . . . . . . 10
282	120	nncnd 9318	. . . . . . . . . 10
283	266	a1i 9	. . . . . . . . . 10 #
284	120	nnap0d 9350	. . . . . . . . . 10 #
285	280, 281, 282, 283, 284	divdivap1d 9152	. . . . . . . . 9
286	285, 247	oveq12d 6103	. . . . . . . 8
287	275	a1i 9	. . . . . . . . 9
288	111, 234, 238	divclapi 9084	. . . . . . . . . 10
289	288	a1i 9	. . . . . . . . 9
290	287, 282, 289, 233, 284, 237	divmuldivapd 9162	. . . . . . . 8
291	286, 290	eqtr3d 2273	. . . . . . 7
292	263	a1i 9	. . . . . . . . . 10
293	292, 282, 233	mulassd 8349	. . . . . . . . 9
294	293	oveq2d 6101	. . . . . . . 8
295	120, 194	nnmulcld 9353	. . . . . . . . . 10
296	295	nncnd 9318	. . . . . . . . 9
297	265	a1i 9	. . . . . . . . 9 #
298	282, 233, 284, 237	mulap0d 8986	. . . . . . . . 9 #
299	281, 292, 296, 297, 298	divdivap1d 9152	. . . . . . . 8
300	294, 299	eqtr4d 2274	. . . . . . 7
301	279, 291, 300	3eqtr4a 2297	. . . . . 6
302	257, 301	breqtrd 4156	. . . . 5
303	26, 2, 137, 261, 302	isumclim 12188	. . . 4
304	260, 303	breqtrd 4156	. . 3
305		4nn 9468	. . . . . . 7
306		nnmulcl 9325	. . . . . . 7 $/\$
307	305, 120, 306	sylancr 418	. . . . . 6
308	307, 194	nnmulcld 9353	. . . . 5
309		nndivre 9340	. . . . 5 $/\$
310	163, 308, 309	sylancr 418	. . . 4
311		elicc2 10340	. . . 4 $/\$ $/\$ $/\$
312	202, 310, 311	sylancr 418	. . 3 $/\$ $/\$
313	72, 86, 304, 312	mpbir3and 1211	. 2
314	78, 313	eqeltrd 2315	1

Colors of variables: wff set class

This proof depends on syntax axioms:

wi 4 $/\$ wa 104

wb 105 $/\$ w3a 1009

wceq 1402

wcel 2209

cvv 2821 class class class wbr 4130

cmpt 4192

cdm 4774

cfv 5377 (class class class)co 6085

cc 8177

cr 8178

cc0 8179

c1 8180

caddc 8182

cmul 8184

clt 8360

cle 8361

cmin 8497 # cap 8909

cdiv 9002

cn 9304

c2 9355

c3 9356

c4 9357

c8 9361

c9 9362

cn0 9563

cz 9644

cuz 9921

cq 10019

crp 10054

cicc 10293

cfz 10411

cseq 10884

cexp 10975

cabs 11763

cli 12044

csu 12119

clog 15957

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4246 ax-sep 4249 ax-nul 4259 ax-pow 4311 ax-pr 4346 ax-un 4578 ax-setind 4684 ax-iinf 4735 ax-cnex 8270 ax-resscn 8271 ax-1cn 8272 ax-1re 8273 ax-icn 8274 ax-addcl 8275 ax-addrcl 8276 ax-mulcl 8277 ax-mulrcl 8278 ax-addcom 8279 ax-mulcom 8280 ax-addass 8281 ax-mulass 8282 ax-distr 8283 ax-i2m1 8284 ax-0lt1 8285 ax-1rid 8286 ax-0id 8287 ax-rnegex 8288 ax-precex 8289 ax-cnre 8290 ax-pre-ltirr 8291 ax-pre-ltwlin 8292 ax-pre-lttrn 8293 ax-pre-apti 8294 ax-pre-ltadd 8295 ax-pre-mulgt0 8296 ax-pre-mulext 8297 ax-arch 8298 ax-caucvg 8299 ax-pre-suploc 8300 ax-addf 8301 ax-mulf 8302

This proof depends on definitions: df-bi 117 df-stab 843 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-disj 4107 df-br 4131 df-opab 4193 df-mpt 4194 df-tr 4230 df-id 4438 df-po 4441 df-iso 4442 df-iord 4511 df-on 4513 df-ilim 4514 df-suc 4516 df-iom 4738 df-xp 4780 df-rel 4781 df-cnv 4782 df-co 4783 df-dm 4784 df-rn 4785 df-res 4786 df-ima 4787 df-iota 5337 df-fun 5379 df-fn 5380 df-f 5381 df-f1 5382 df-fo 5383 df-f1o 5384 df-fv 5385 df-isom 5386 df-riota 6038 df-ov 6088 df-oprab 6089 df-mpo 6090 df-of 6302 df-1st 6374 df-2nd 6375 df-recs 6576 df-irdg 6641 df-frec 6662 df-1o 6687 df-oadd 6691 df-er 6807 df-map 6924 df-pm 6925 df-en 7023 df-dom 7024 df-fin 7025 df-sup 7324 df-inf 7325 df-pnf 8362 df-mnf 8363 df-xr 8364 df-ltxr 8365 df-le 8366 df-sub 8499 df-neg 8500 df-reap 8903 df-ap 8910 df-div 9003 df-inn 9305 df-2 9363 df-3 9364 df-4 9365 df-5 9366 df-6 9367 df-7 9368 df-8 9369 df-9 9370 df-n0 9564 df-z 9645 df-uz 9922 df-q 10020 df-rp 10055 df-xneg 10174 df-xadd 10175 df-ioo 10294 df-ico 10296 df-icc 10297 df-fz 10412 df-fzo 10550 df-seqfrec 10885 df-exp 10976 df-fac 11164 df-bc 11186 df-ihash 11215 df-shft 11580 df-cj 11607 df-re 11608 df-im 11609 df-rsqrt 11764 df-abs 11765 df-clim 12045 df-sumdc 12120 df-ef 12415 df-e 12416 df-rest 13595 df-topgen 13614 df-psmet 14880 df-xmet 14881 df-met 14882 df-bl 14883 df-mopn 14884 df-top 15099 df-topon 15112 df-bases 15144 df-ntr 15197 df-cn 15289 df-cnp 15290 df-tx 15354 df-cncf 15672 df-limced 15757 df-dvap 15758 df-relog 15959

This theorem is used by: log2ublog2 16086

W3C validator