log2tlbndlog2 - Intuitionistic Logic Explorer

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

Theorem log2tlbndlog2 16065

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 9639	. . . . 5
2		nn0z 9647	. . . . . 6
3		peano2zm 9665	. . . . . 6
4	2, 3	syl 14	. . . . 5
5	1, 4	fzfigd 10851	. . . 4
6		elfznn0 10504	. . . . 5
7		2re 9357	. . . . . . 7
8		3nn 9450	. . . . . . . . 9
9		2nn0 9563	. . . . . . . . . . 11
10		simpr 110	. . . . . . . . . . 11 $/\$
11		nn0mulcl 9582	. . . . . . . . . . 11 $/\$
12	9, 10, 11	sylancr 418	. . . . . . . . . 10 $/\$
13		nn0p1nn 9585	. . . . . . . . . 10
14	12, 13	syl 14	. . . . . . . . 9 $/\$
15		nnmulcl 9308	. . . . . . . . 9 $/\$
16	8, 14, 15	sylancr 418	. . . . . . . 8 $/\$
17		9nn 9456	. . . . . . . . 9
18		nnexpcl 10972	. . . . . . . . 9 $/\$
19	17, 10, 18	sylancr 418	. . . . . . . 8 $/\$
20	16, 19	nnmulcld 9336	. . . . . . 7 $/\$
21		nndivre 9323	. . . . . . 7 $/\$
22	7, 20, 21	sylancr 418	. . . . . 6 $/\$
23	22	recnd 8348	. . . . 5 $/\$
24	6, 23	sylan2 286	. . . 4 $/\$
25	5, 24	fsumcl 12150	. . 3
26		eqid 2238	. . . . 5
27		eluznn0 9982	. . . . . 6 $/\$
28		eqid 2238	. . . . . . 7
29		oveq2 6087	. . . . . . . . . . 11
30	29	oveq1d 6094	. . . . . . . . . 10
31	30	oveq2d 6095	. . . . . . . . 9
32		oveq2 6087	. . . . . . . . 9
33	31, 32	oveq12d 6097	. . . . . . . 8
34	33	oveq2d 6095	. . . . . . 7
35		id 19	. . . . . . 7
36	7	a1i 9	. . . . . . . 8
37		3rp 10043	. . . . . . . . . . 11
38	37	a1i 9	. . . . . . . . . 10
39		nn0re 9555	. . . . . . . . . . . 12
40	36, 39	remulcld 8350	. . . . . . . . . . 11
41		0le2 9377	. . . . . . . . . . . . 13
42	41	a1i 9	. . . . . . . . . . . 12
43		nn0ge0 9571	. . . . . . . . . . . 12
44	36, 39, 42, 43	mulge0d 8943	. . . . . . . . . . 11
45	40, 44	ge0p1rpd 10111	. . . . . . . . . 10
46	38, 45	rpmulcld 10097	. . . . . . . . 9
47		9re 9374	. . . . . . . . . . 11
48		9pos 9391	. . . . . . . . . . 11
49	47, 48	elrpii 10040	. . . . . . . . . 10
50		nn0z 9647	. . . . . . . . . 10
51		rpexpcl 10978	. . . . . . . . . 10 $/\$
52	49, 50, 51	sylancr 418	. . . . . . . . 9
53	46, 52	rpmulcld 10097	. . . . . . . 8
54	36, 53	rerpdivcld 10112	. . . . . . 7
55	28, 34, 35, 54	fvmptd3 5796	. . . . . 6
56	27, 55	syl 14	. . . . 5 $/\$
57	27, 22	syldan 282	. . . . 5 $/\$
58		log2tlbnd.log2cnv	. . . . . . 7
59		seqex 10869	. . . . . . . 8
60		2rp 10042	. . . . . . . . . 10
61		relogcl 15946	. . . . . . . . . 10
62	60, 61	ax-mp 5	. . . . . . . . 9
63	62	elexi 2834	. . . . . . . 8
64	59, 63	breldm 4983	. . . . . . 7
65	58, 64	mp1i 10	. . . . . 6
66		nn0uz 9940	. . . . . . 7
67		id 19	. . . . . . 7
68	55	adantl 277	. . . . . . . 8 $/\$
69	68, 23	eqeltrd 2315	. . . . . . 7 $/\$
70	66, 67, 69	iserex 12088	. . . . . 6
71	65, 70	mpbid 147	. . . . 5
72	26, 2, 56, 57, 71	isumrecl 12179	. . . 4
73	72	recnd 8348	. . 3
74	58	a1i 9	. . . . 5
75	66, 1, 68, 23, 74	isumclim 12171	. . . 4
76	66, 26, 67, 68, 23, 65	isumsplit 12241	. . . 4
77	75, 76	eqtr3d 2273	. . 3
78	25, 73, 77	mvrladdd 8687	. 2
79	7	a1i 9	. . . . . 6 $/\$
80	41	a1i 9	. . . . . 6 $/\$
81	20	nnred 9300	. . . . . 6 $/\$
82	20	nngt0d 9331	. . . . . 6 $/\$
83		divge0 9197	. . . . . 6 $/\$ $/\$ $/\$
84	79, 80, 81, 82, 83	syl22anc 1279	. . . . 5 $/\$
85	27, 84	syldan 282	. . . 4 $/\$
86	26, 2, 56, 57, 71, 85	isumge0 12180	. . 3
87		eqid 2238	. . . . . . . 8
88		oveq2 6087	. . . . . . . . 9
89	88	oveq2d 6095	. . . . . . . 8
90	60	a1i 9	. . . . . . . . . . 11 $/\$
91	37	a1i 9	. . . . . . . . . . . 12 $/\$
92	9	a1i 9	. . . . . . . . . . . . . . . 16
93	92, 67	nn0mulcld 9608	. . . . . . . . . . . . . . 15
94		nn0p1nn 9585	. . . . . . . . . . . . . . 15
95	93, 94	syl 14	. . . . . . . . . . . . . 14
96	95	nnrpd 10078	. . . . . . . . . . . . 13
97	96	adantr 276	. . . . . . . . . . . 12 $/\$
98	91, 97	rpmulcld 10097	. . . . . . . . . . 11 $/\$
99	90, 98	rpdivcld 10098	. . . . . . . . . 10 $/\$
100	99	rpred 10080	. . . . . . . . 9 $/\$
101		1z 9653	. . . . . . . . . . . . . 14
102		znq 10007	. . . . . . . . . . . . . 14 $/\$
103	101, 17, 102	mp2an 430	. . . . . . . . . . . . 13
104		qre 10008	. . . . . . . . . . . . 13
105	103, 104	ax-mp 5	. . . . . . . . . . . 12
106	105	a1i 9	. . . . . . . . . . 11
107	106, 35	reexpcld 11111	. . . . . . . . . 10
108	107	adantl 277	. . . . . . . . 9 $/\$
109	100, 108	remulcld 8350	. . . . . . . 8 $/\$
110	87, 89, 10, 109	fvmptd3 5796	. . . . . . 7 $/\$
111		9cn 9375	. . . . . . . . . . 11
112	111	a1i 9	. . . . . . . . . 10 $/\$
113	47, 48	gt0ap0ii 8950	. . . . . . . . . . 11 #
114	113	a1i 9	. . . . . . . . . 10 $/\$ #
115	50	adantl 277	. . . . . . . . . 10 $/\$
116	112, 114, 115	exprecapd 11102	. . . . . . . . 9 $/\$
117	116	oveq2d 6095	. . . . . . . 8 $/\$
118		nn0mulcl 9582	. . . . . . . . . . . . . . 15 $/\$
119	9, 118	mpan 428	. . . . . . . . . . . . . 14
120	119, 94	syl 14	. . . . . . . . . . . . 13
121		nnmulcl 9308	. . . . . . . . . . . . 13 $/\$
122	8, 120, 121	sylancr 418	. . . . . . . . . . . 12
123		nndivre 9323	. . . . . . . . . . . 12 $/\$
124	7, 122, 123	sylancr 418	. . . . . . . . . . 11
125	124	recnd 8348	. . . . . . . . . 10
126	125	adantr 276	. . . . . . . . 9 $/\$
127	19	nncnd 9301	. . . . . . . . 9 $/\$
128	19	nnap0d 9333	. . . . . . . . 9 $/\$ #
129	126, 127, 128	divrecapd 9117	. . . . . . . 8 $/\$
130		2cnd 9360	. . . . . . . . 9 $/\$
131	122	adantr 276	. . . . . . . . . 10 $/\$
132	131	nncnd 9301	. . . . . . . . 9 $/\$
133	131	nnap0d 9333	. . . . . . . . 9 $/\$ #
134	130, 132, 127, 133, 128	divdivap1d 9146	. . . . . . . 8 $/\$
135	117, 129, 134	3eqtr2d 2277	. . . . . . 7 $/\$
136	110, 135	eqtrd 2271	. . . . . 6 $/\$
137	27, 136	syldan 282	. . . . 5 $/\$
138	131, 19	nnmulcld 9336	. . . . . . 7 $/\$
139		nndivre 9323	. . . . . . 7 $/\$
140	7, 138, 139	sylancr 418	. . . . . 6 $/\$
141	27, 140	syldan 282	. . . . 5 $/\$
142	119	adantr 276	. . . . . . . . . 10 $/\$
143	142	nn0red 9604	. . . . . . . . 9 $/\$
144	9, 27, 11	sylancr 418	. . . . . . . . . 10 $/\$
145	144	nn0red 9604	. . . . . . . . 9 $/\$
146		1red 8335	. . . . . . . . 9 $/\$
147		eluzle 9917	. . . . . . . . . . 11
148	147	adantl 277	. . . . . . . . . 10 $/\$
149		nn0re 9555	. . . . . . . . . . . 12
150	149	adantr 276	. . . . . . . . . . 11 $/\$
151	27	nn0red 9604	. . . . . . . . . . 11 $/\$
152	7	a1i 9	. . . . . . . . . . 11 $/\$
153		2pos 9378	. . . . . . . . . . . 12
154	153	a1i 9	. . . . . . . . . . 11 $/\$
155		lemul2 9181	. . . . . . . . . . 11 $/\$ $/\$ $/\$
156	150, 151, 152, 154, 155	syl112anc 1282	. . . . . . . . . 10 $/\$
157	148, 156	mpbid 147	. . . . . . . . 9 $/\$
158	143, 145, 146, 157	leadd1dd 8881	. . . . . . . 8 $/\$
159	120	adantr 276	. . . . . . . . . 10 $/\$
160	159	nnred 9300	. . . . . . . . 9 $/\$
161	27, 14	syldan 282	. . . . . . . . . 10 $/\$
162	161	nnred 9300	. . . . . . . . 9 $/\$
163		3re 9361	. . . . . . . . . 10
164	163	a1i 9	. . . . . . . . 9 $/\$
165		3pos 9381	. . . . . . . . . 10
166	165	a1i 9	. . . . . . . . 9 $/\$
167		lemul2 9181	. . . . . . . . 9 $/\$ $/\$ $/\$
168	160, 162, 164, 166, 167	syl112anc 1282	. . . . . . . 8 $/\$
169	158, 168	mpbid 147	. . . . . . 7 $/\$
170	122	adantr 276	. . . . . . . . 9 $/\$
171	170	nnred 9300	. . . . . . . 8 $/\$
172	27, 16	syldan 282	. . . . . . . . 9 $/\$
173	172	nnred 9300	. . . . . . . 8 $/\$
174	17, 27, 18	sylancr 418	. . . . . . . . 9 $/\$
175	174	nnred 9300	. . . . . . . 8 $/\$
176	174	nngt0d 9331	. . . . . . . 8 $/\$
177		lemul1 8915	. . . . . . . 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 9300	. . . . . . 7 $/\$
182	180	nngt0d 9331	. . . . . . 7 $/\$
183	27, 81	syldan 282	. . . . . . 7 $/\$
184	27, 82	syldan 282	. . . . . . 7 $/\$
185		lediv2 9215	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
186	181, 182, 183, 184, 152, 154, 185	syl222anc 1294	. . . . . 6 $/\$
187	179, 186	mpbid 147	. . . . 5 $/\$
188		seqex 10869	. . . . . 6
189	49	a1i 9	. . . . . . . . 9
190		8nn 9455	. . . . . . . . . . . 12
191	190	a1i 9	. . . . . . . . . . 11
192	191	nnrpd 10078	. . . . . . . . . 10
193		nnexpcl 10972	. . . . . . . . . . . 12 $/\$
194	17, 193	mpan 428	. . . . . . . . . . 11
195	194	nnrpd 10078	. . . . . . . . . 10
196	192, 195	rpmulcld 10097	. . . . . . . . 9
197	189, 196	rpdivcld 10098	. . . . . . . 8
198	197	rpred 10080	. . . . . . 7
199	124, 198	remulcld 8350	. . . . . 6
200	105	recni 8332	. . . . . . . . . 10
201	200	a1i 9	. . . . . . . . 9
202		0re 8320	. . . . . . . . . . . . 13
203	47, 48	recgt0ii 9231	. . . . . . . . . . . . 13
204	202, 105, 203	ltleii 8422	. . . . . . . . . . . 12
205		absid 11820	. . . . . . . . . . . 12 $/\$
206	105, 204, 205	mp2an 430	. . . . . . . . . . 11
207		1lt9 9492	. . . . . . . . . . . . 13
208		recgt1i 9222	. . . . . . . . . . . . 13 $/\$ $/\$
209	47, 207, 208	mp2an 430	. . . . . . . . . . . 12 $/\$
210	209	simpri 113	. . . . . . . . . . 11
211	206, 210	eqbrtri 4149	. . . . . . . . . 10
212	211	a1i 9	. . . . . . . . 9
213		eqid 2238	. . . . . . . . . . 11
214	213, 88, 35, 107	fvmptd3 5796	. . . . . . . . . 10
215	27, 214	syl 14	. . . . . . . . 9 $/\$
216	201, 212, 67, 215	geolim2 12262	. . . . . . . 8
217	111	a1i 9	. . . . . . . . . . 11
218	113	a1i 9	. . . . . . . . . . 11 #
219	217, 218, 2	exprecapd 11102	. . . . . . . . . 10
220	111, 113	dividapi 9069	. . . . . . . . . . . . 13
221	220	oveq1i 6089	. . . . . . . . . . . 12
222		ax-1cn 8266	. . . . . . . . . . . . . 14
223	111, 113	pm3.2i 272	. . . . . . . . . . . . . 14 $/\$ #
224		divsubdirap 9032	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ #
225	111, 222, 223, 224	mp3an 1378	. . . . . . . . . . . . 13
226		9m1e8 9413	. . . . . . . . . . . . . 14
227	226	oveq1i 6089	. . . . . . . . . . . . 13
228	225, 227	eqtr3i 2261	. . . . . . . . . . . 12
229	221, 228	eqtr3i 2261	. . . . . . . . . . 11
230	229	a1i 9	. . . . . . . . . 10
231	219, 230	oveq12d 6097	. . . . . . . . 9
232	222	a1i 9	. . . . . . . . . 10
233	194	nncnd 9301	. . . . . . . . . 10
234		8cn 9373	. . . . . . . . . . . 12
235	234, 111, 113	divclapi 9078	. . . . . . . . . . 11
236	235	a1i 9	. . . . . . . . . 10
237	194	nnap0d 9333	. . . . . . . . . 10 #
238	190	nnap0i 9318	. . . . . . . . . . . 12 #
239	234, 111, 238, 113	divap0i 9084	. . . . . . . . . . 11 #
240	239	a1i 9	. . . . . . . . . 10 #
241	232, 233, 236, 237, 240	divdiv32apd 9140	. . . . . . . . 9
242		recdivap 9042	. . . . . . . . . . . 12 $/\$ # $/\$ $/\$ #
243	234, 238, 111, 113, 242	mp4an 431	. . . . . . . . . . 11
244	243	oveq1i 6089	. . . . . . . . . 10
245	234	a1i 9	. . . . . . . . . . 11
246	238	a1i 9	. . . . . . . . . . 11 #
247	217, 245, 233, 246, 237	divdivap1d 9146	. . . . . . . . . 10
248	244, 247	eqtrid 2283	. . . . . . . . 9
249	231, 241, 248	3eqtrd 2275	. . . . . . . 8
250	216, 249	breqtrd 4154	. . . . . . 7
251		expcl 10977	. . . . . . . . 9 $/\$
252	200, 27, 251	sylancr 418	. . . . . . . 8 $/\$
253	215, 252	eqeltrd 2315	. . . . . . 7 $/\$
254	27, 110	syldan 282	. . . . . . . 8 $/\$
255	215	oveq2d 6095	. . . . . . . 8 $/\$
256	254, 255	eqtr4d 2274	. . . . . . 7 $/\$
257	26, 2, 125, 250, 253, 256	isermulc2 12089	. . . . . 6
258		breldmg 4985	. . . . . 6 $/\$ $/\$
259	188, 199, 257, 258	mp3an2i 1383	. . . . 5
260	26, 2, 56, 57, 137, 141, 187, 71, 259	isumle 12245	. . . 4
261	141	recnd 8348	. . . . 5 $/\$
262		3cn 9362	. . . . . . . . . . . 12
263		4cn 9365	. . . . . . . . . . . 12
264		2cn 9358	. . . . . . . . . . . 12
265		4ap0 9386	. . . . . . . . . . . 12 #
266		3ap0 9383	. . . . . . . . . . . 12 #
267		2ap0 9380	. . . . . . . . . . . 12 #
268	262, 263, 264, 262, 265, 266, 267	divdivdivapi 9099	. . . . . . . . . . 11
269		3t3e9 9445	. . . . . . . . . . . 12
270		4t2e8 9446	. . . . . . . . . . . 12
271	269, 270	oveq12i 6091	. . . . . . . . . . 11
272	268, 271	eqtri 2259	. . . . . . . . . 10
273	272	oveq2i 6090	. . . . . . . . 9
274	262, 263, 265	divclapi 9078	. . . . . . . . . 10
275	264, 262, 266	divclapi 9078	. . . . . . . . . 10
276	264, 262, 267, 266	divap0i 9084	. . . . . . . . . 10 #
277	274, 275, 276	divcanap2i 9079	. . . . . . . . 9
278	273, 277	eqtr3i 2261	. . . . . . . 8
279	278	oveq1i 6089	. . . . . . 7
280		2cnd 9360	. . . . . . . . . 10
281	262	a1i 9	. . . . . . . . . 10
282	120	nncnd 9301	. . . . . . . . . 10
283	266	a1i 9	. . . . . . . . . 10 #
284	120	nnap0d 9333	. . . . . . . . . 10 #
285	280, 281, 282, 283, 284	divdivap1d 9146	. . . . . . . . 9
286	285, 247	oveq12d 6097	. . . . . . . 8
287	275	a1i 9	. . . . . . . . 9
288	111, 234, 238	divclapi 9078	. . . . . . . . . 10
289	288	a1i 9	. . . . . . . . 9
290	287, 282, 289, 233, 284, 237	divmuldivapd 9156	. . . . . . . 8
291	286, 290	eqtr3d 2273	. . . . . . 7
292	263	a1i 9	. . . . . . . . . 10
293	292, 282, 233	mulassd 8343	. . . . . . . . 9
294	293	oveq2d 6095	. . . . . . . 8
295	120, 194	nnmulcld 9336	. . . . . . . . . 10
296	295	nncnd 9301	. . . . . . . . 9
297	265	a1i 9	. . . . . . . . 9 #
298	282, 233, 284, 237	mulap0d 8980	. . . . . . . . 9 #
299	281, 292, 296, 297, 298	divdivap1d 9146	. . . . . . . 8
300	294, 299	eqtr4d 2274	. . . . . . 7
301	279, 291, 300	3eqtr4a 2297	. . . . . 6
302	257, 301	breqtrd 4154	. . . . 5
303	26, 2, 137, 261, 302	isumclim 12171	. . . 4
304	260, 303	breqtrd 4154	. . 3
305		4nn 9451	. . . . . . 7
306		nnmulcl 9308	. . . . . . 7 $/\$
307	305, 120, 306	sylancr 418	. . . . . 6
308	307, 194	nnmulcld 9336	. . . . 5
309		nndivre 9323	. . . . 5 $/\$
310	163, 308, 309	sylancr 418	. . . 4
311		elicc2 10323	. . . 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

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $/\$ w3a 1009

wceq 1402

wcel 2209

cvv 2821 class class class wbr 4128

cmpt 4190

cdm 4772

cfv 5375 (class class class)co 6079

cc 8171

cr 8172

cc0 8173

c1 8174

caddc 8176

cmul 8178

clt 8354

cle 8355

cmin 8491 # cap 8903

cdiv 8996

cn 9287

c2 9338

c3 9339

c4 9340

c8 9344

c9 9345

cn0 9546

cz 9627

cuz 9904

cq 10002

crp 10037

cicc 10276

cfz 10394

cseq 10867

cexp 10958

cabs 11746

cli 12027

csu 12102

clog 15940

This theorem was proved from 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 4244 ax-sep 4247 ax-nul 4257 ax-pow 4309 ax-pr 4344 ax-un 4576 ax-setind 4682 ax-iinf 4733 ax-cnex 8264 ax-resscn 8265 ax-1cn 8266 ax-1re 8267 ax-icn 8268 ax-addcl 8269 ax-addrcl 8270 ax-mulcl 8271 ax-mulrcl 8272 ax-addcom 8273 ax-mulcom 8274 ax-addass 8275 ax-mulass 8276 ax-distr 8277 ax-i2m1 8278 ax-0lt1 8279 ax-1rid 8280 ax-0id 8281 ax-rnegex 8282 ax-precex 8283 ax-cnre 8284 ax-pre-ltirr 8285 ax-pre-ltwlin 8286 ax-pre-lttrn 8287 ax-pre-apti 8288 ax-pre-ltadd 8289 ax-pre-mulgt0 8290 ax-pre-mulext 8291 ax-arch 8292 ax-caucvg 8293 ax-pre-suploc 8294 ax-addf 8295 ax-mulf 8296

This theorem 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 3714 df-pr 3715 df-op 3717 df-uni 3934 df-int 3969 df-iun 4012 df-disj 4105 df-br 4129 df-opab 4191 df-mpt 4192 df-tr 4228 df-id 4436 df-po 4439 df-iso 4440 df-iord 4509 df-on 4511 df-ilim 4512 df-suc 4514 df-iom 4736 df-xp 4778 df-rel 4779 df-cnv 4780 df-co 4781 df-dm 4782 df-rn 4783 df-res 4784 df-ima 4785 df-iota 5335 df-fun 5377 df-fn 5378 df-f 5379 df-f1 5380 df-fo 5381 df-f1o 5382 df-fv 5383 df-isom 5384 df-riota 6032 df-ov 6082 df-oprab 6083 df-mpo 6084 df-of 6296 df-1st 6368 df-2nd 6369 df-recs 6570 df-irdg 6635 df-frec 6656 df-1o 6681 df-oadd 6685 df-er 6801 df-map 6918 df-pm 6919 df-en 7017 df-dom 7018 df-fin 7019 df-sup 7318 df-inf 7319 df-pnf 8356 df-mnf 8357 df-xr 8358 df-ltxr 8359 df-le 8360 df-sub 8493 df-neg 8494 df-reap 8897 df-ap 8904 df-div 8997 df-inn 9288 df-2 9346 df-3 9347 df-4 9348 df-5 9349 df-6 9350 df-7 9351 df-8 9352 df-9 9353 df-n0 9547 df-z 9628 df-uz 9905 df-q 10003 df-rp 10038 df-xneg 10157 df-xadd 10158 df-ioo 10277 df-ico 10279 df-icc 10280 df-fz 10395 df-fzo 10533 df-seqfrec 10868 df-exp 10959 df-fac 11147 df-bc 11169 df-ihash 11198 df-shft 11563 df-cj 11590 df-re 11591 df-im 11592 df-rsqrt 11747 df-abs 11748 df-clim 12028 df-sumdc 12103 df-ef 12398 df-e 12399 df-rest 13578 df-topgen 13597 df-psmet 14863 df-xmet 14864 df-met 14865 df-bl 14866 df-mopn 14867 df-top 15082 df-topon 15095 df-bases 15127 df-ntr 15180 df-cn 15272 df-cnp 15273 df-tx 15337 df-cncf 15655 df-limced 15740 df-dvap 15741 df-relog 15942

This theorem is referenced by: log2ublog2 16069

W3C validator