log2ublog2 - Intuitionistic Logic Explorer

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

Theorem log2ublog2 16069

Description:

is less than

. If written in decimal, this is because

0.693147... is less than 253/365 = 0.693151... , so this is a very tight bound, at five decimal places. The presence of the hypothesis here is a temporary measure until it can be proved as log2cnv . (Contributed by Mario Carneiro, 7-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)

**Hypothesis**
Ref	Expression
log2ublog2.log2cnv

**Assertion**
Ref	Expression
log2ublog2	;; ;;

Proof of Theorem log2ublog2 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		4m1e3 9408	. . . . . . . . 9
2	1	oveq2i 6090	. . . . . . . 8
3	2	sumeq1i 12112	. . . . . . 7
4	3	oveq2i 6090	. . . . . 6
5		4nn0 9565	. . . . . . 7
6		log2ublog2.log2cnv	. . . . . . . 8
7	6	log2tlbndlog2 16065	. . . . . . 7
8	5, 7	ax-mp 5	. . . . . 6
9	4, 8	eqeltrri 2312	. . . . 5
10		0re 8320	. . . . . 6
11		3re 9361	. . . . . . 7
12		4nn 9451	. . . . . . . . 9
13		2nn0 9563	. . . . . . . . . 10
14		1nn 9298	. . . . . . . . . 10
15	13, 5, 14	numnncl 9769	. . . . . . . . 9
16	12, 15	nnmulcli 9309	. . . . . . . 8
17		9nn 9456	. . . . . . . . 9
18		nnexpcl 10972	. . . . . . . . 9 $/\$
19	17, 5, 18	mp2an 430	. . . . . . . 8
20	16, 19	nnmulcli 9309	. . . . . . 7
21		nndivre 9323	. . . . . . 7 $/\$
22	11, 20, 21	mp2an 430	. . . . . 6
23	10, 22	elicc2i 10324	. . . . 5 $/\$ $/\$
24	9, 23	mpbi 145	. . . 4 $/\$ $/\$
25	24	simp3i 1039	. . 3
26		2rp 10042	. . . . 5
27		relogcl 15946	. . . . 5
28	26, 27	ax-mp 5	. . . 4
29		0zd 9639	. . . . . . 7
30		3z 9656	. . . . . . . 8
31	30	a1i 9	. . . . . . 7
32	29, 31	fzfigd 10851	. . . . . 6
33		2re 9357	. . . . . . 7
34		3nn 9450	. . . . . . . . 9
35		elfznn0 10504	. . . . . . . . . . . 12
36	35	adantl 277	. . . . . . . . . . 11 $/\$
37		nn0mulcl 9582	. . . . . . . . . . 11 $/\$
38	13, 36, 37	sylancr 418	. . . . . . . . . 10 $/\$
39		nn0p1nn 9585	. . . . . . . . . 10
40	38, 39	syl 14	. . . . . . . . 9 $/\$
41		nnmulcl 9308	. . . . . . . . 9 $/\$
42	34, 40, 41	sylancr 418	. . . . . . . 8 $/\$
43		nnexpcl 10972	. . . . . . . . 9 $/\$
44	17, 36, 43	sylancr 418	. . . . . . . 8 $/\$
45	42, 44	nnmulcld 9336	. . . . . . 7 $/\$
46		nndivre 9323	. . . . . . 7 $/\$
47	33, 45, 46	sylancr 418	. . . . . 6 $/\$
48	32, 47	fsumrecl 12151	. . . . 5
49	48	mptru 1411	. . . 4
50	28, 49, 22	lesubadd2i 8830	. . 3
51	25, 50	mpbi 145	. 2
52		log2ublem3 16068	. . . . 5 ;;;;
53		3nn0 9564	. . . . 5
54		5nn0 9566	. . . . . . . . 9
55	54, 53	deccl 9774	. . . . . . . 8 ;
56		0nn0 9561	. . . . . . . 8
57	55, 56	deccl 9774	. . . . . . 7 ;;
58	57, 54	deccl 9774	. . . . . 6 ;;;
59		6nn0 9567	. . . . . 6
60	58, 59	deccl 9774	. . . . 5 ;;;;
61		1nn0 9562	. . . . 5
62		eqid 2238	. . . . 5
63		6p1e7 9426	. . . . . 6
64		eqid 2238	. . . . . 6 ;;;; ;;;;
65	58, 59, 63, 64	decsuc 9790	. . . . 5 ;;;; ;;;;
66		5nn 9452	. . . . . . . . . 10
67		7nn 9454	. . . . . . . . . 10
68	66, 67	nnmulcli 9309	. . . . . . . . 9
69	68	nnrei 9296	. . . . . . . 8
70	16	nnrei 9296	. . . . . . . 8
71		6nn 9453	. . . . . . . . . 10
72		5lt6 9467	. . . . . . . . . 10
73	53, 54, 71, 72	declt 9787	. . . . . . . . 9 ; ;
74		7cn 9371	. . . . . . . . . 10
75		5cn 9367	. . . . . . . . . 10
76		7t5e35 9871	. . . . . . . . . 10 ;
77	74, 75, 76	mulcomli 8327	. . . . . . . . 9 ;
78		4cn 9365	. . . . . . . . . . . . . 14
79		2cn 9358	. . . . . . . . . . . . . 14
80		4t2e8 9446	. . . . . . . . . . . . . 14
81	78, 79, 80	mulcomli 8327	. . . . . . . . . . . . 13
82	81	oveq1i 6089	. . . . . . . . . . . 12
83		8p1e9 9428	. . . . . . . . . . . 12
84	82, 83	eqtri 2259	. . . . . . . . . . 11
85	84	oveq2i 6090	. . . . . . . . . 10
86		9cn 9375	. . . . . . . . . . 11
87		9t4e36 9883	. . . . . . . . . . 11 ;
88	86, 78, 87	mulcomli 8327	. . . . . . . . . 10 ;
89	85, 88	eqtri 2259	. . . . . . . . 9 ;
90	73, 77, 89	3brtr4i 4158	. . . . . . . 8
91	69, 70, 90	ltleii 8422	. . . . . . 7
92	19	nngt0i 9317	. . . . . . . 8
93	19	nnrei 9296	. . . . . . . . 9
94	69, 70, 93	lemul2i 9249	. . . . . . . 8
95	92, 94	ax-mp 5	. . . . . . 7
96	91, 95	mpbi 145	. . . . . 6
97		7nn0 9568	. . . . . . . . . 10
98		nnexpcl 10972	. . . . . . . . . 10 $/\$
99	34, 97, 98	mp2an 430	. . . . . . . . 9
100	99	nncni 9297	. . . . . . . 8
101	68	nncni 9297	. . . . . . . 8
102		3cn 9362	. . . . . . . 8
103	100, 101, 102	mul32i 8467	. . . . . . 7
104	78, 79	mulcomi 8326	. . . . . . . . . . . 12
105		df-8 9352	. . . . . . . . . . . 12
106	80, 104, 105	3eqtr3i 2267	. . . . . . . . . . 11
107	106	oveq2i 6090	. . . . . . . . . 10
108		expmul 11004	. . . . . . . . . . 11 $/\$ $/\$
109	102, 13, 5, 108	mp3an 1378	. . . . . . . . . 10
110	107, 109	eqtr3i 2261	. . . . . . . . 9
111		expp1 10966	. . . . . . . . . 10 $/\$
112	102, 97, 111	mp2an 430	. . . . . . . . 9
113		sq3 11056	. . . . . . . . . 10
114	113	oveq1i 6089	. . . . . . . . 9
115	110, 112, 114	3eqtr3i 2267	. . . . . . . 8
116	115	oveq1i 6089	. . . . . . 7
117	103, 116	eqtri 2259	. . . . . 6
118	16	nncni 9297	. . . . . . . . 9
119	19	nncni 9297	. . . . . . . . 9
120	118, 119	mulcomi 8326	. . . . . . . 8
121	120	oveq1i 6089	. . . . . . 7
122	119, 118	mulcli 8325	. . . . . . . 8
123	122	mulridi 8322	. . . . . . 7
124	121, 123	eqtri 2259	. . . . . 6
125	96, 117, 124	3brtr4i 4158	. . . . 5
126	52, 49, 53, 20, 60, 61, 62, 65, 125	log2ublem1 16066	. . . 4 ;;;;
127	49, 22	readdcli 8333	. . . . 5
128	58, 97	deccl 9774	. . . . . 6 ;;;;
129	128	nn0rei 9557	. . . . 5 ;;;;
130	99, 68	nnmulcli 9309	. . . . . . 7
131	130	nnrei 9296	. . . . . 6
132	130	nngt0i 9317	. . . . . 6
133	131, 132	pm3.2i 272	. . . . 5 $/\$
134		lemuldiv2 9206	. . . . 5 $/\$ ;;;; $/\$ $/\$ ;;;; ;;;;
135	127, 129, 133, 134	mp3an 1378	. . . 4 ;;;; ;;;;
136	126, 135	mpbi 145	. . 3 ;;;;
137		8nn0 9569	. . . . . . . . . . . . 13
138	53, 137	deccl 9774	. . . . . . . . . . . 12 ;
139	138, 97	deccl 9774	. . . . . . . . . . 11 ;;
140	139, 53	deccl 9774	. . . . . . . . . 10 ;;;
141	140, 61	deccl 9774	. . . . . . . . 9 ;;;;
142	141, 59	deccl 9774	. . . . . . . 8 ;;;;;
143	141, 97	deccl 9774	. . . . . . . 8 ;;;;;
144		1lt10 9898	. . . . . . . 8 ;
145		6lt7 9472	. . . . . . . . 9
146	141, 59, 67, 145	declt 9787	. . . . . . . 8 ;;;;; ;;;;;
147	142, 143, 61, 97, 144, 146	decltc 9788	. . . . . . 7 ;;;;;; ;;;;;;
148		eqid 2238	. . . . . . . 8 ; ;
149	61, 54	deccl 9774	. . . . . . . . . . 11 ;
150		9nn0 9570	. . . . . . . . . . 11
151	149, 150	deccl 9774	. . . . . . . . . 10 ;;
152	151, 61	deccl 9774	. . . . . . . . 9 ;;;
153	152, 97	deccl 9774	. . . . . . . 8 ;;;;
154		eqid 2238	. . . . . . . . 9 ;;;; ;;;;
155		eqid 2238	. . . . . . . . 9 ;;;; ;;;;
156		eqid 2238	. . . . . . . . . 10 ;;; ;;;
157		eqid 2238	. . . . . . . . . . 11 ;;; ;;;
158		ax-1cn 8266	. . . . . . . . . . . 12
159		5p1e6 9425	. . . . . . . . . . . 12
160	75, 158, 159	addcomli 8465	. . . . . . . . . . 11
161	151, 61, 54, 157, 160	decaddi 9819	. . . . . . . . . 10 ;;; ;;;
162	61, 59	deccl 9774	. . . . . . . . . . 11 ;
163		eqid 2238	. . . . . . . . . . 11 ;; ;;
164		eqid 2238	. . . . . . . . . . . 12 ;; ;;
165		eqid 2238	. . . . . . . . . . . . 13 ; ;
166	61, 54, 159, 165	decsuc 9790	. . . . . . . . . . . 12 ; ;
167		9p4e13 9848	. . . . . . . . . . . 12 ;
168	149, 150, 5, 164, 166, 53, 167	decaddci 9820	. . . . . . . . . . 11 ;; ;;
169		eqid 2238	. . . . . . . . . . . 12 ; ;
170	162	nn0cni 9558	. . . . . . . . . . . . 13 ;
171	170	addridi 8462	. . . . . . . . . . . 12 ; ;
172		1p2e3 9422	. . . . . . . . . . . . . 14
173	172	oveq2i 6090	. . . . . . . . . . . . 13
174		5p3e8 9435	. . . . . . . . . . . . . 14
175	53, 54, 53, 77, 174	decaddi 9819	. . . . . . . . . . . . 13 ;
176	173, 175	eqtri 2259	. . . . . . . . . . . 12 ;
177		7t3e21 9869	. . . . . . . . . . . . . 14 ;
178	74, 102, 177	mulcomli 8327	. . . . . . . . . . . . 13 ;
179		6cn 9369	. . . . . . . . . . . . . 14
180	179, 158, 63	addcomli 8465	. . . . . . . . . . . . 13
181	13, 61, 59, 178, 180	decaddi 9819	. . . . . . . . . . . 12 ;
182	54, 53, 61, 59, 169, 171, 97, 97, 13, 176, 181	decmac 9811	. . . . . . . . . . 11 ; ; ;;
183	74	mul02i 8711	. . . . . . . . . . . . 13
184	183	oveq1i 6089	. . . . . . . . . . . 12
185	102	addlidi 8463	. . . . . . . . . . . . 13
186	53	dec0h 9781	. . . . . . . . . . . . 13 ;
187	185, 186	eqtri 2259	. . . . . . . . . . . 12 ;
188	184, 187	eqtri 2259	. . . . . . . . . . 11 ;
189	55, 56, 162, 53, 163, 168, 97, 53, 56, 182, 188	decmac 9811	. . . . . . . . . 10 ;; ;; ;;;
190		3p1e4 9423	. . . . . . . . . . 11
191		6p5e11 9832	. . . . . . . . . . . 12 ;
192	179, 75, 191	addcomli 8465	. . . . . . . . . . 11 ;
193	53, 54, 59, 77, 190, 61, 192	decaddci 9820	. . . . . . . . . 10 ;
194	57, 54, 151, 59, 156, 161, 97, 61, 5, 189, 193	decmac 9811	. . . . . . . . 9 ;;; ;;; ;;;;
195		7t7e49 9873	. . . . . . . . . 10 ;
196		4p1e5 9424	. . . . . . . . . 10
197		9p7e16 9851	. . . . . . . . . 10 ;
198	5, 150, 97, 195, 196, 59, 197	decaddci 9820	. . . . . . . . 9 ;
199	58, 97, 152, 97, 154, 155, 97, 59, 54, 194, 198	decmac 9811	. . . . . . . 8 ;;;; ;;;; ;;;;;
200	13	dec0h 9781	. . . . . . . . . 10 ;
201	158	addlidi 8463	. . . . . . . . . . . 12
202	61	dec0h 9781	. . . . . . . . . . . 12 ;
203	201, 202	eqtri 2259	. . . . . . . . . . 11 ;
204		00id 8461	. . . . . . . . . . . . 13
205	56	dec0h 9781	. . . . . . . . . . . . 13 ;
206	204, 205	eqtri 2259	. . . . . . . . . . . 12 ;
207		5t3e15 9860	. . . . . . . . . . . . . 14 ;
208	207	oveq1i 6089	. . . . . . . . . . . . 13 ;
209	149	nn0cni 9558	. . . . . . . . . . . . . 14 ;
210	209	addridi 8462	. . . . . . . . . . . . 13 ; ;
211	208, 210	eqtri 2259	. . . . . . . . . . . 12 ;
212		3t3e9 9445	. . . . . . . . . . . . . 14
213	212	oveq1i 6089	. . . . . . . . . . . . 13
214	86	addridi 8462	. . . . . . . . . . . . 13
215	213, 214	eqtri 2259	. . . . . . . . . . . 12
216	54, 53, 56, 56, 169, 206, 53, 211, 215	decma 9810	. . . . . . . . . . 11 ; ;;
217	102	mul02i 8711	. . . . . . . . . . . . 13
218	217	oveq1i 6089	. . . . . . . . . . . 12
219	218, 203	eqtri 2259	. . . . . . . . . . 11 ;
220	55, 56, 56, 61, 163, 203, 53, 61, 56, 216, 219	decmac 9811	. . . . . . . . . 10 ;; ;;;
221		5p2e7 9434	. . . . . . . . . . 11
222	61, 54, 13, 207, 221	decaddi 9819	. . . . . . . . . 10 ;
223	57, 54, 56, 13, 156, 200, 53, 97, 61, 220, 222	decmac 9811	. . . . . . . . 9 ;;; ;;;;
224	53, 58, 97, 154, 61, 13, 223, 177	decmul1c 9824	. . . . . . . 8 ;;;; ;;;;;
225	128, 97, 53, 148, 61, 153, 199, 224	decmul2c 9825	. . . . . . 7 ;;;; ; ;;;;;;
226	54, 54	deccl 9774	. . . . . . . . . . 11 ;
227	226, 53	deccl 9774	. . . . . . . . . 10 ;;
228	227, 53	deccl 9774	. . . . . . . . 9 ;;;
229	228, 61	deccl 9774	. . . . . . . 8 ;;;;
230	13, 54	deccl 9774	. . . . . . . . . 10 ;
231	230, 53	deccl 9774	. . . . . . . . 9 ;;
232	13, 61	deccl 9774	. . . . . . . . . 10 ;
233	232, 137	deccl 9774	. . . . . . . . 9 ;;
234	97, 13	deccl 9774	. . . . . . . . . . 11 ;
235		3t2e6 9444	. . . . . . . . . . . . 13
236	102, 79, 235	mulcomli 8327	. . . . . . . . . . . 12
237		3exp3 13200	. . . . . . . . . . . 12 ;
238	13, 97	deccl 9774	. . . . . . . . . . . . 13 ;
239		eqid 2238	. . . . . . . . . . . . 13 ; ;
240	61, 137	deccl 9774	. . . . . . . . . . . . 13 ;
241		eqid 2238	. . . . . . . . . . . . . 14 ; ;
242		2t2e4 9442	. . . . . . . . . . . . . . . 16
243	242, 172	oveq12i 6091	. . . . . . . . . . . . . . 15
244		4p3e7 9432	. . . . . . . . . . . . . . 15
245	243, 244	eqtri 2259	. . . . . . . . . . . . . 14
246		7t2e14 9868	. . . . . . . . . . . . . . 15 ;
247		1p1e2 9404	. . . . . . . . . . . . . . 15
248		8cn 9373	. . . . . . . . . . . . . . . 16
249		8p4e12 9841	. . . . . . . . . . . . . . . 16 ;
250	248, 78, 249	addcomli 8465	. . . . . . . . . . . . . . 15 ;
251	61, 5, 137, 246, 247, 13, 250	decaddci 9820	. . . . . . . . . . . . . 14 ;
252	13, 97, 61, 137, 239, 241, 13, 13, 13, 245, 251	decmac 9811	. . . . . . . . . . . . 13 ; ; ;
253	74, 79, 246	mulcomli 8327	. . . . . . . . . . . . . . 15 ;
254		4p4e8 9433	. . . . . . . . . . . . . . 15
255	61, 5, 5, 253, 254	decaddi 9819	. . . . . . . . . . . . . 14 ;
256	97, 13, 97, 239, 150, 5, 255, 195	decmul1c 9824	. . . . . . . . . . . . 13 ; ;;
257	238, 13, 97, 239, 150, 240, 252, 256	decmul2c 9825	. . . . . . . . . . . 12 ; ; ;;
258	53, 53, 236, 237, 257	numexp2x 13187	. . . . . . . . . . 11 ;;
259		eqid 2238	. . . . . . . . . . . 12 ; ;
260	236	oveq1i 6089	. . . . . . . . . . . . 13
261		6p2e8 9437	. . . . . . . . . . . . 13
262	260, 261	eqtri 2259	. . . . . . . . . . . 12
263	97, 13, 13, 259, 53, 177, 262	decrmanc 9816	. . . . . . . . . . 11 ; ;;
264		9t3e27 9882	. . . . . . . . . . 11 ;
265	53, 234, 150, 258, 97, 13, 263, 264	decmul1c 9824	. . . . . . . . . 10 ;;;
266	53, 59, 63, 265	numexpp1 13186	. . . . . . . . 9 ;;;
267	61, 97	deccl 9774	. . . . . . . . . 10 ;
268	267, 97	deccl 9774	. . . . . . . . 9 ;;
269		eqid 2238	. . . . . . . . . 10 ;; ;;
270		eqid 2238	. . . . . . . . . 10 ;; ;;
271	13, 56	deccl 9774	. . . . . . . . . . 11 ;
272	271, 53	deccl 9774	. . . . . . . . . 10 ;;
273	13, 13	deccl 9774	. . . . . . . . . . 11 ;
274		eqid 2238	. . . . . . . . . . 11 ; ;
275		eqid 2238	. . . . . . . . . . . 12 ; ;
276		eqid 2238	. . . . . . . . . . . 12 ;; ;;
277		eqid 2238	. . . . . . . . . . . . . 14 ; ;
278	79	addlidi 8463	. . . . . . . . . . . . . 14
279	158	addridi 8462	. . . . . . . . . . . . . 14
280	56, 61, 13, 56, 202, 277, 278, 279	decadd 9813	. . . . . . . . . . . . 13 ; ;
281	13, 61, 247, 280	decsuc 9790	. . . . . . . . . . . 12 ; ;
282		7p3e10 9834	. . . . . . . . . . . 12 ;
283	61, 97, 271, 53, 275, 276, 281, 282	decaddc2 9815	. . . . . . . . . . 11 ; ;; ;;
284		eqid 2238	. . . . . . . . . . . 12 ;; ;;
285		eqid 2238	. . . . . . . . . . . . 13 ; ;
286		eqid 2238	. . . . . . . . . . . . 13 ; ;
287		2p2e4 9414	. . . . . . . . . . . . 13
288	75, 79, 221	addcomli 8465	. . . . . . . . . . . . 13
289	13, 13, 13, 54, 285, 286, 287, 288	decadd 9813	. . . . . . . . . . . 12 ; ; ;
290	54	dec0h 9781	. . . . . . . . . . . . . 14 ;
291	196, 290	eqtri 2259	. . . . . . . . . . . . 13 ;
292	242, 201	oveq12i 6091	. . . . . . . . . . . . . 14
293	292, 196	eqtri 2259	. . . . . . . . . . . . 13
294		5t2e10 9859	. . . . . . . . . . . . . 14 ;
295	75	addlidi 8463	. . . . . . . . . . . . . 14
296	61, 56, 54, 294, 295	decaddi 9819	. . . . . . . . . . . . 13 ;
297	13, 54, 56, 54, 286, 291, 13, 54, 61, 293, 296	decmac 9811	. . . . . . . . . . . 12 ; ;
298	235	oveq1i 6089	. . . . . . . . . . . . 13
299		7p6e13 9837	. . . . . . . . . . . . . 14 ;
300	74, 179, 299	addcomli 8465	. . . . . . . . . . . . 13 ;
301	298, 300	eqtri 2259	. . . . . . . . . . . 12 ;
302	230, 53, 5, 97, 284, 289, 13, 53, 61, 297, 301	decmac 9811	. . . . . . . . . . 11 ;; ; ; ;;
303	231	nn0cni 9558	. . . . . . . . . . . . . 14 ;;
304	303	mulridi 8322	. . . . . . . . . . . . 13 ;; ;;
305	304	oveq1i 6089	. . . . . . . . . . . 12 ;; ;;
306	303	addridi 8462	. . . . . . . . . . . 12 ;; ;;
307	305, 306	eqtri 2259	. . . . . . . . . . 11 ;; ;;
308	13, 61, 273, 56, 274, 283, 231, 53, 230, 302, 307	decma2c 9812	. . . . . . . . . 10 ;; ; ; ;; ;;;
309	97	dec0h 9781	. . . . . . . . . . 11 ;
310	78	addlidi 8463	. . . . . . . . . . . . . 14
311	310	oveq2i 6090	. . . . . . . . . . . . 13
312		8t2e16 9874	. . . . . . . . . . . . . . 15 ;
313	248, 79, 312	mulcomli 8327	. . . . . . . . . . . . . 14 ;
314		6p4e10 9831	. . . . . . . . . . . . . 14 ;
315	61, 59, 5, 313, 247, 314	decaddci2 9821	. . . . . . . . . . . . 13 ;
316	311, 315	eqtri 2259	. . . . . . . . . . . 12 ;
317		8t5e40 9877	. . . . . . . . . . . . . 14 ;
318	248, 75, 317	mulcomli 8327	. . . . . . . . . . . . 13 ;
319	5, 56, 53, 318, 185	decaddi 9819	. . . . . . . . . . . 12 ;
320	13, 54, 56, 53, 286, 187, 137, 53, 5, 316, 319	decmac 9811	. . . . . . . . . . 11 ; ;;
321		8t3e24 9875	. . . . . . . . . . . . 13 ;
322	248, 102, 321	mulcomli 8327	. . . . . . . . . . . 12 ;
323		2p1e3 9421	. . . . . . . . . . . 12
324		7p4e11 9835	. . . . . . . . . . . . 13 ;
325	74, 78, 324	addcomli 8465	. . . . . . . . . . . 12 ;
326	13, 5, 97, 322, 323, 61, 325	decaddci 9820	. . . . . . . . . . 11 ;
327	230, 53, 56, 97, 284, 309, 137, 61, 53, 320, 326	decmac 9811	. . . . . . . . . 10 ;; ;;;
328	232, 137, 267, 97, 269, 270, 231, 61, 272, 308, 327	decma2c 9812	. . . . . . . . 9 ;; ;; ;; ;;;;
329	61, 5, 53, 253, 244	decaddi 9819	. . . . . . . . . . 11 ;
330	53, 54, 13, 77, 221	decaddi 9819	. . . . . . . . . . 11 ;
331	13, 54, 13, 286, 97, 97, 53, 329, 330	decrmac 9817	. . . . . . . . . 10 ; ;;
332	97, 230, 53, 284, 61, 13, 331, 178	decmul1c 9824	. . . . . . . . 9 ;; ;;;
333	231, 233, 97, 266, 61, 268, 328, 332	decmul2c 9825	. . . . . . . 8 ;; ;;;;;
334		eqid 2238	. . . . . . . . 9 ;;;; ;;;;
335		eqid 2238	. . . . . . . . . 10 ;;; ;;;
336		eqid 2238	. . . . . . . . . . 11 ;; ;;
337		eqid 2238	. . . . . . . . . . . 12 ; ;
338	278, 200	eqtri 2259	. . . . . . . . . . . 12 ;
339	185	oveq2i 6090	. . . . . . . . . . . . 13
340	339, 175	eqtri 2259	. . . . . . . . . . . 12 ;
341	54, 54, 56, 13, 337, 338, 97, 97, 53, 340, 330	decmac 9811	. . . . . . . . . . 11 ; ;;
342	13, 61, 13, 178, 172	decaddi 9819	. . . . . . . . . . 11 ;
343	226, 53, 56, 13, 336, 200, 97, 53, 13, 341, 342	decmac 9811	. . . . . . . . . 10 ;; ;;;
344	97, 227, 53, 335, 61, 13, 343, 178	decmul1c 9824	. . . . . . . . 9 ;;; ;;;;
345	74	mullidi 8323	. . . . . . . . 9
346	97, 228, 61, 334, 97, 344, 345	decmul1 9823	. . . . . . . 8 ;;;; ;;;;;
347	97, 229, 61, 333, 97, 346, 345	decmul1 9823	. . . . . . 7 ;; ;;;;;;
348	147, 225, 347	3brtr4i 4158	. . . . . 6 ;;;; ; ;;
349	97, 53	deccl 9774	. . . . . . . . 9 ;
350	128, 349	nn0mulcli 9584	. . . . . . . 8 ;;;; ;
351	350	nn0rei 9557	. . . . . . 7 ;;;; ;
352	53, 97	nn0expcli 10985	. . . . . . . . . 10
353	231, 352	nn0mulcli 9584	. . . . . . . . 9 ;;
354	353, 97	nn0mulcli 9584	. . . . . . . 8 ;;
355	354	nn0rei 9557	. . . . . . 7 ;;
356	66	nnrei 9296	. . . . . . 7
357	66	nngt0i 9317	. . . . . . 7
358	351, 355, 356, 357	ltmul1ii 9252	. . . . . 6 ;;;; ; ;; ;;;; ; ;;
359	348, 358	mpbi 145	. . . . 5 ;;;; ; ;;
360	128	nn0cni 9558	. . . . . . 7 ;;;;
361	349	nn0cni 9558	. . . . . . 7 ;
362	360, 361, 75	mulassi 8329	. . . . . 6 ;;;; ; ;;;; ;
363	53, 54, 159, 76	decsuc 9790	. . . . . . . 8 ;
364	75, 102, 207	mulcomli 8327	. . . . . . . 8 ;
365	54, 97, 53, 148, 54, 61, 363, 364	decmul1c 9824	. . . . . . 7 ; ;;
366	365	oveq2i 6090	. . . . . 6 ;;;; ; ;;;; ;;
367	362, 366	eqtri 2259	. . . . 5 ;;;; ; ;;;; ;;
368	303, 100	mulcli 8325	. . . . . . 7 ;;
369	368, 74, 75	mulassi 8329	. . . . . 6 ;; ;;
370	74, 75	mulcomi 8326	. . . . . . . 8
371	370	oveq2i 6090	. . . . . . 7 ;; ;;
372	303, 100, 101	mulassi 8329	. . . . . . 7 ;; ;;
373	371, 372	eqtri 2259	. . . . . 6 ;; ;;
374	369, 373	eqtri 2259	. . . . 5 ;; ;;
375	359, 367, 374	3brtr3i 4157	. . . 4 ;;;; ;; ;;
376	53, 59	deccl 9774	. . . . . . . 8 ;
377	376, 66	decnncl 9779	. . . . . . 7 ;;
378	377	nnrei 9296	. . . . . 6 ;;
379	377	nngt0i 9317	. . . . . 6 ;;
380	378, 379	pm3.2i 272	. . . . 5 ;; $/\$ ;;
381	231	nn0rei 9557	. . . . 5 ;;
382		lt2mul2div 9203	. . . . 5 ;;;; $/\$ ;; $/\$ ;; $/\$ ;; $/\$ $/\$ ;;;; ;; ;; ;;;; ;; ;;
383	129, 380, 381, 133, 382	mp4an 431	. . . 4 ;;;; ;; ;; ;;;; ;; ;;
384	375, 383	mpbi 145	. . 3 ;;;; ;; ;;
385		nndivre 9323	. . . . 5 ;;;; $/\$ ;;;;
386	129, 130, 385	mp2an 430	. . . 4 ;;;;
387		nndivre 9323	. . . . 5 ;; $/\$ ;; ;; ;;
388	381, 377, 387	mp2an 430	. . . 4 ;; ;;
389	127, 386, 388	lelttri 8425	. . 3 ;;;; $/\$ ;;;; ;; ;; ;; ;;
390	136, 384, 389	mp2an 430	. 2 ;; ;;
391	28, 127, 388	lelttri 8425	. 2 $/\$ ;; ;; ;; ;;
392	51, 390, 391	mp2an 430	1 ;; ;;

Colors of variables: wff set class

Syntax hints: $/\$ wa 104

wb 105 $/\$ w3a 1009

wceq 1402

wtru 1403

wcel 2209 class class class wbr 4128

cmpt 4190

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

cdiv 8996

cn 9287

c2 9338

c3 9339

c4 9340

c5 9341

c6 9342

c7 9343

c8 9344

c9 9345

cn0 9546

cz 9627 ;cdc 9760

crp 10037

cicc 10276

cfz 10394

cseq 10867

cexp 10958

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-dec 9761 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: birthdaylog2 16073

W3C validator