log2ublog2 - Intuitionistic Logic Explorer

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

Theorem log2ublog2 16086

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 9425	. . . . . . . . 9
2	1	oveq2i 6096	. . . . . . . 8
3	2	sumeq1i 12129	. . . . . . 7
4	3	oveq2i 6096	. . . . . 6
5		4nn0 9582	. . . . . . 7
6		log2ublog2.log2cnv	. . . . . . . 8
7	6	log2tlbndlog2 16082	. . . . . . 7
8	5, 7	ax-mp 5	. . . . . 6
9	4, 8	eqeltrri 2312	. . . . 5
10		0re 8326	. . . . . 6
11		3re 9378	. . . . . . 7
12		4nn 9468	. . . . . . . . 9
13		2nn0 9580	. . . . . . . . . 10
14		1nn 9315	. . . . . . . . . 10
15	13, 5, 14	numnncl 9786	. . . . . . . . 9
16	12, 15	nnmulcli 9326	. . . . . . . 8
17		9nn 9473	. . . . . . . . 9
18		nnexpcl 10989	. . . . . . . . 9 $/\$
19	17, 5, 18	mp2an 430	. . . . . . . 8
20	16, 19	nnmulcli 9326	. . . . . . 7
21		nndivre 9340	. . . . . . 7 $/\$
22	11, 20, 21	mp2an 430	. . . . . 6
23	10, 22	elicc2i 10341	. . . . 5 $/\$ $/\$
24	9, 23	mpbi 145	. . . 4 $/\$ $/\$
25	24	simp3i 1039	. . 3
26		2rp 10059	. . . . 5
27		relogcl 15963	. . . . 5
28	26, 27	ax-mp 5	. . . 4
29		0zd 9656	. . . . . . 7
30		3z 9673	. . . . . . . 8
31	30	a1i 9	. . . . . . 7
32	29, 31	fzfigd 10868	. . . . . 6
33		2re 9374	. . . . . . 7
34		3nn 9467	. . . . . . . . 9
35		elfznn0 10521	. . . . . . . . . . . 12
36	35	adantl 277	. . . . . . . . . . 11 $/\$
37		nn0mulcl 9599	. . . . . . . . . . 11 $/\$
38	13, 36, 37	sylancr 418	. . . . . . . . . 10 $/\$
39		nn0p1nn 9602	. . . . . . . . . 10
40	38, 39	syl 14	. . . . . . . . 9 $/\$
41		nnmulcl 9325	. . . . . . . . 9 $/\$
42	34, 40, 41	sylancr 418	. . . . . . . 8 $/\$
43		nnexpcl 10989	. . . . . . . . 9 $/\$
44	17, 36, 43	sylancr 418	. . . . . . . 8 $/\$
45	42, 44	nnmulcld 9353	. . . . . . 7 $/\$
46		nndivre 9340	. . . . . . 7 $/\$
47	33, 45, 46	sylancr 418	. . . . . 6 $/\$
48	32, 47	fsumrecl 12168	. . . . 5
49	48	mptru 1411	. . . 4
50	28, 49, 22	lesubadd2i 8836	. . 3
51	25, 50	mpbi 145	. 2
52		log2ublem3 16085	. . . . 5 ;;;;
53		3nn0 9581	. . . . 5
54		5nn0 9583	. . . . . . . . 9
55	54, 53	deccl 9791	. . . . . . . 8 ;
56		0nn0 9578	. . . . . . . 8
57	55, 56	deccl 9791	. . . . . . 7 ;;
58	57, 54	deccl 9791	. . . . . 6 ;;;
59		6nn0 9584	. . . . . 6
60	58, 59	deccl 9791	. . . . 5 ;;;;
61		1nn0 9579	. . . . 5
62		eqid 2238	. . . . 5
63		6p1e7 9443	. . . . . 6
64		eqid 2238	. . . . . 6 ;;;; ;;;;
65	58, 59, 63, 64	decsuc 9807	. . . . 5 ;;;; ;;;;
66		5nn 9469	. . . . . . . . . 10
67		7nn 9471	. . . . . . . . . 10
68	66, 67	nnmulcli 9326	. . . . . . . . 9
69	68	nnrei 9313	. . . . . . . 8
70	16	nnrei 9313	. . . . . . . 8
71		6nn 9470	. . . . . . . . . 10
72		5lt6 9484	. . . . . . . . . 10
73	53, 54, 71, 72	declt 9804	. . . . . . . . 9 ; ;
74		7cn 9388	. . . . . . . . . 10
75		5cn 9384	. . . . . . . . . 10
76		7t5e35 9888	. . . . . . . . . 10 ;
77	74, 75, 76	mulcomli 8333	. . . . . . . . 9 ;
78		4cn 9382	. . . . . . . . . . . . . 14
79		2cn 9375	. . . . . . . . . . . . . 14
80		4t2e8 9463	. . . . . . . . . . . . . 14
81	78, 79, 80	mulcomli 8333	. . . . . . . . . . . . 13
82	81	oveq1i 6095	. . . . . . . . . . . 12
83		8p1e9 9445	. . . . . . . . . . . 12
84	82, 83	eqtri 2259	. . . . . . . . . . 11
85	84	oveq2i 6096	. . . . . . . . . 10
86		9cn 9392	. . . . . . . . . . 11
87		9t4e36 9900	. . . . . . . . . . 11 ;
88	86, 78, 87	mulcomli 8333	. . . . . . . . . 10 ;
89	85, 88	eqtri 2259	. . . . . . . . 9 ;
90	73, 77, 89	3brtr4i 4160	. . . . . . . 8
91	69, 70, 90	ltleii 8428	. . . . . . 7
92	19	nngt0i 9334	. . . . . . . 8
93	19	nnrei 9313	. . . . . . . . 9
94	69, 70, 93	lemul2i 9255	. . . . . . . 8
95	92, 94	ax-mp 5	. . . . . . 7
96	91, 95	mpbi 145	. . . . . 6
97		7nn0 9585	. . . . . . . . . 10
98		nnexpcl 10989	. . . . . . . . . 10 $/\$
99	34, 97, 98	mp2an 430	. . . . . . . . 9
100	99	nncni 9314	. . . . . . . 8
101	68	nncni 9314	. . . . . . . 8
102		3cn 9379	. . . . . . . 8
103	100, 101, 102	mul32i 8473	. . . . . . 7
104	78, 79	mulcomi 8332	. . . . . . . . . . . 12
105		df-8 9369	. . . . . . . . . . . 12
106	80, 104, 105	3eqtr3i 2267	. . . . . . . . . . 11
107	106	oveq2i 6096	. . . . . . . . . 10
108		expmul 11021	. . . . . . . . . . 11 $/\$ $/\$
109	102, 13, 5, 108	mp3an 1378	. . . . . . . . . 10
110	107, 109	eqtr3i 2261	. . . . . . . . 9
111		expp1 10983	. . . . . . . . . 10 $/\$
112	102, 97, 111	mp2an 430	. . . . . . . . 9
113		sq3 11073	. . . . . . . . . 10
114	113	oveq1i 6095	. . . . . . . . 9
115	110, 112, 114	3eqtr3i 2267	. . . . . . . 8
116	115	oveq1i 6095	. . . . . . 7
117	103, 116	eqtri 2259	. . . . . 6
118	16	nncni 9314	. . . . . . . . 9
119	19	nncni 9314	. . . . . . . . 9
120	118, 119	mulcomi 8332	. . . . . . . 8
121	120	oveq1i 6095	. . . . . . 7
122	119, 118	mulcli 8331	. . . . . . . 8
123	122	mulridi 8328	. . . . . . 7
124	121, 123	eqtri 2259	. . . . . 6
125	96, 117, 124	3brtr4i 4160	. . . . 5
126	52, 49, 53, 20, 60, 61, 62, 65, 125	log2ublem1 16083	. . . 4 ;;;;
127	49, 22	readdcli 8339	. . . . 5
128	58, 97	deccl 9791	. . . . . 6 ;;;;
129	128	nn0rei 9574	. . . . 5 ;;;;
130	99, 68	nnmulcli 9326	. . . . . . 7
131	130	nnrei 9313	. . . . . 6
132	130	nngt0i 9334	. . . . . 6
133	131, 132	pm3.2i 272	. . . . 5 $/\$
134		lemuldiv2 9212	. . . . 5 $/\$ ;;;; $/\$ $/\$ ;;;; ;;;;
135	127, 129, 133, 134	mp3an 1378	. . . 4 ;;;; ;;;;
136	126, 135	mpbi 145	. . 3 ;;;;
137		8nn0 9586	. . . . . . . . . . . . 13
138	53, 137	deccl 9791	. . . . . . . . . . . 12 ;
139	138, 97	deccl 9791	. . . . . . . . . . 11 ;;
140	139, 53	deccl 9791	. . . . . . . . . 10 ;;;
141	140, 61	deccl 9791	. . . . . . . . 9 ;;;;
142	141, 59	deccl 9791	. . . . . . . 8 ;;;;;
143	141, 97	deccl 9791	. . . . . . . 8 ;;;;;
144		1lt10 9915	. . . . . . . 8 ;
145		6lt7 9489	. . . . . . . . 9
146	141, 59, 67, 145	declt 9804	. . . . . . . 8 ;;;;; ;;;;;
147	142, 143, 61, 97, 144, 146	decltc 9805	. . . . . . 7 ;;;;;; ;;;;;;
148		eqid 2238	. . . . . . . 8 ; ;
149	61, 54	deccl 9791	. . . . . . . . . . 11 ;
150		9nn0 9587	. . . . . . . . . . 11
151	149, 150	deccl 9791	. . . . . . . . . 10 ;;
152	151, 61	deccl 9791	. . . . . . . . 9 ;;;
153	152, 97	deccl 9791	. . . . . . . 8 ;;;;
154		eqid 2238	. . . . . . . . 9 ;;;; ;;;;
155		eqid 2238	. . . . . . . . 9 ;;;; ;;;;
156		eqid 2238	. . . . . . . . . 10 ;;; ;;;
157		eqid 2238	. . . . . . . . . . 11 ;;; ;;;
158		ax-1cn 8272	. . . . . . . . . . . 12
159		5p1e6 9442	. . . . . . . . . . . 12
160	75, 158, 159	addcomli 8471	. . . . . . . . . . 11
161	151, 61, 54, 157, 160	decaddi 9836	. . . . . . . . . 10 ;;; ;;;
162	61, 59	deccl 9791	. . . . . . . . . . 11 ;
163		eqid 2238	. . . . . . . . . . 11 ;; ;;
164		eqid 2238	. . . . . . . . . . . 12 ;; ;;
165		eqid 2238	. . . . . . . . . . . . 13 ; ;
166	61, 54, 159, 165	decsuc 9807	. . . . . . . . . . . 12 ; ;
167		9p4e13 9865	. . . . . . . . . . . 12 ;
168	149, 150, 5, 164, 166, 53, 167	decaddci 9837	. . . . . . . . . . 11 ;; ;;
169		eqid 2238	. . . . . . . . . . . 12 ; ;
170	162	nn0cni 9575	. . . . . . . . . . . . 13 ;
171	170	addridi 8468	. . . . . . . . . . . 12 ; ;
172		1p2e3 9439	. . . . . . . . . . . . . 14
173	172	oveq2i 6096	. . . . . . . . . . . . 13
174		5p3e8 9452	. . . . . . . . . . . . . 14
175	53, 54, 53, 77, 174	decaddi 9836	. . . . . . . . . . . . 13 ;
176	173, 175	eqtri 2259	. . . . . . . . . . . 12 ;
177		7t3e21 9886	. . . . . . . . . . . . . 14 ;
178	74, 102, 177	mulcomli 8333	. . . . . . . . . . . . 13 ;
179		6cn 9386	. . . . . . . . . . . . . 14
180	179, 158, 63	addcomli 8471	. . . . . . . . . . . . 13
181	13, 61, 59, 178, 180	decaddi 9836	. . . . . . . . . . . 12 ;
182	54, 53, 61, 59, 169, 171, 97, 97, 13, 176, 181	decmac 9828	. . . . . . . . . . 11 ; ; ;;
183	74	mul02i 8717	. . . . . . . . . . . . 13
184	183	oveq1i 6095	. . . . . . . . . . . 12
185	102	addlidi 8469	. . . . . . . . . . . . 13
186	53	dec0h 9798	. . . . . . . . . . . . 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 9828	. . . . . . . . . 10 ;; ;; ;;;
190		3p1e4 9440	. . . . . . . . . . 11
191		6p5e11 9849	. . . . . . . . . . . 12 ;
192	179, 75, 191	addcomli 8471	. . . . . . . . . . 11 ;
193	53, 54, 59, 77, 190, 61, 192	decaddci 9837	. . . . . . . . . 10 ;
194	57, 54, 151, 59, 156, 161, 97, 61, 5, 189, 193	decmac 9828	. . . . . . . . 9 ;;; ;;; ;;;;
195		7t7e49 9890	. . . . . . . . . 10 ;
196		4p1e5 9441	. . . . . . . . . 10
197		9p7e16 9868	. . . . . . . . . 10 ;
198	5, 150, 97, 195, 196, 59, 197	decaddci 9837	. . . . . . . . 9 ;
199	58, 97, 152, 97, 154, 155, 97, 59, 54, 194, 198	decmac 9828	. . . . . . . 8 ;;;; ;;;; ;;;;;
200	13	dec0h 9798	. . . . . . . . . 10 ;
201	158	addlidi 8469	. . . . . . . . . . . 12
202	61	dec0h 9798	. . . . . . . . . . . 12 ;
203	201, 202	eqtri 2259	. . . . . . . . . . 11 ;
204		00id 8467	. . . . . . . . . . . . 13
205	56	dec0h 9798	. . . . . . . . . . . . 13 ;
206	204, 205	eqtri 2259	. . . . . . . . . . . 12 ;
207		5t3e15 9877	. . . . . . . . . . . . . 14 ;
208	207	oveq1i 6095	. . . . . . . . . . . . 13 ;
209	149	nn0cni 9575	. . . . . . . . . . . . . 14 ;
210	209	addridi 8468	. . . . . . . . . . . . 13 ; ;
211	208, 210	eqtri 2259	. . . . . . . . . . . 12 ;
212		3t3e9 9462	. . . . . . . . . . . . . 14
213	212	oveq1i 6095	. . . . . . . . . . . . 13
214	86	addridi 8468	. . . . . . . . . . . . 13
215	213, 214	eqtri 2259	. . . . . . . . . . . 12
216	54, 53, 56, 56, 169, 206, 53, 211, 215	decma 9827	. . . . . . . . . . 11 ; ;;
217	102	mul02i 8717	. . . . . . . . . . . . 13
218	217	oveq1i 6095	. . . . . . . . . . . 12
219	218, 203	eqtri 2259	. . . . . . . . . . 11 ;
220	55, 56, 56, 61, 163, 203, 53, 61, 56, 216, 219	decmac 9828	. . . . . . . . . 10 ;; ;;;
221		5p2e7 9451	. . . . . . . . . . 11
222	61, 54, 13, 207, 221	decaddi 9836	. . . . . . . . . 10 ;
223	57, 54, 56, 13, 156, 200, 53, 97, 61, 220, 222	decmac 9828	. . . . . . . . 9 ;;; ;;;;
224	53, 58, 97, 154, 61, 13, 223, 177	decmul1c 9841	. . . . . . . 8 ;;;; ;;;;;
225	128, 97, 53, 148, 61, 153, 199, 224	decmul2c 9842	. . . . . . 7 ;;;; ; ;;;;;;
226	54, 54	deccl 9791	. . . . . . . . . . 11 ;
227	226, 53	deccl 9791	. . . . . . . . . 10 ;;
228	227, 53	deccl 9791	. . . . . . . . 9 ;;;
229	228, 61	deccl 9791	. . . . . . . 8 ;;;;
230	13, 54	deccl 9791	. . . . . . . . . 10 ;
231	230, 53	deccl 9791	. . . . . . . . 9 ;;
232	13, 61	deccl 9791	. . . . . . . . . 10 ;
233	232, 137	deccl 9791	. . . . . . . . 9 ;;
234	97, 13	deccl 9791	. . . . . . . . . . 11 ;
235		3t2e6 9461	. . . . . . . . . . . . 13
236	102, 79, 235	mulcomli 8333	. . . . . . . . . . . 12
237		3exp3 13217	. . . . . . . . . . . 12 ;
238	13, 97	deccl 9791	. . . . . . . . . . . . 13 ;
239		eqid 2238	. . . . . . . . . . . . 13 ; ;
240	61, 137	deccl 9791	. . . . . . . . . . . . 13 ;
241		eqid 2238	. . . . . . . . . . . . . 14 ; ;
242		2t2e4 9459	. . . . . . . . . . . . . . . 16
243	242, 172	oveq12i 6097	. . . . . . . . . . . . . . 15
244		4p3e7 9449	. . . . . . . . . . . . . . 15
245	243, 244	eqtri 2259	. . . . . . . . . . . . . 14
246		7t2e14 9885	. . . . . . . . . . . . . . 15 ;
247		1p1e2 9421	. . . . . . . . . . . . . . 15
248		8cn 9390	. . . . . . . . . . . . . . . 16
249		8p4e12 9858	. . . . . . . . . . . . . . . 16 ;
250	248, 78, 249	addcomli 8471	. . . . . . . . . . . . . . 15 ;
251	61, 5, 137, 246, 247, 13, 250	decaddci 9837	. . . . . . . . . . . . . 14 ;
252	13, 97, 61, 137, 239, 241, 13, 13, 13, 245, 251	decmac 9828	. . . . . . . . . . . . 13 ; ; ;
253	74, 79, 246	mulcomli 8333	. . . . . . . . . . . . . . 15 ;
254		4p4e8 9450	. . . . . . . . . . . . . . 15
255	61, 5, 5, 253, 254	decaddi 9836	. . . . . . . . . . . . . 14 ;
256	97, 13, 97, 239, 150, 5, 255, 195	decmul1c 9841	. . . . . . . . . . . . 13 ; ;;
257	238, 13, 97, 239, 150, 240, 252, 256	decmul2c 9842	. . . . . . . . . . . 12 ; ; ;;
258	53, 53, 236, 237, 257	numexp2x 13204	. . . . . . . . . . 11 ;;
259		eqid 2238	. . . . . . . . . . . 12 ; ;
260	236	oveq1i 6095	. . . . . . . . . . . . 13
261		6p2e8 9454	. . . . . . . . . . . . 13
262	260, 261	eqtri 2259	. . . . . . . . . . . 12
263	97, 13, 13, 259, 53, 177, 262	decrmanc 9833	. . . . . . . . . . 11 ; ;;
264		9t3e27 9899	. . . . . . . . . . 11 ;
265	53, 234, 150, 258, 97, 13, 263, 264	decmul1c 9841	. . . . . . . . . 10 ;;;
266	53, 59, 63, 265	numexpp1 13203	. . . . . . . . 9 ;;;
267	61, 97	deccl 9791	. . . . . . . . . 10 ;
268	267, 97	deccl 9791	. . . . . . . . 9 ;;
269		eqid 2238	. . . . . . . . . 10 ;; ;;
270		eqid 2238	. . . . . . . . . 10 ;; ;;
271	13, 56	deccl 9791	. . . . . . . . . . 11 ;
272	271, 53	deccl 9791	. . . . . . . . . 10 ;;
273	13, 13	deccl 9791	. . . . . . . . . . 11 ;
274		eqid 2238	. . . . . . . . . . 11 ; ;
275		eqid 2238	. . . . . . . . . . . 12 ; ;
276		eqid 2238	. . . . . . . . . . . 12 ;; ;;
277		eqid 2238	. . . . . . . . . . . . . 14 ; ;
278	79	addlidi 8469	. . . . . . . . . . . . . 14
279	158	addridi 8468	. . . . . . . . . . . . . 14
280	56, 61, 13, 56, 202, 277, 278, 279	decadd 9830	. . . . . . . . . . . . 13 ; ;
281	13, 61, 247, 280	decsuc 9807	. . . . . . . . . . . 12 ; ;
282		7p3e10 9851	. . . . . . . . . . . 12 ;
283	61, 97, 271, 53, 275, 276, 281, 282	decaddc2 9832	. . . . . . . . . . 11 ; ;; ;;
284		eqid 2238	. . . . . . . . . . . 12 ;; ;;
285		eqid 2238	. . . . . . . . . . . . 13 ; ;
286		eqid 2238	. . . . . . . . . . . . 13 ; ;
287		2p2e4 9431	. . . . . . . . . . . . 13
288	75, 79, 221	addcomli 8471	. . . . . . . . . . . . 13
289	13, 13, 13, 54, 285, 286, 287, 288	decadd 9830	. . . . . . . . . . . 12 ; ; ;
290	54	dec0h 9798	. . . . . . . . . . . . . 14 ;
291	196, 290	eqtri 2259	. . . . . . . . . . . . 13 ;
292	242, 201	oveq12i 6097	. . . . . . . . . . . . . 14
293	292, 196	eqtri 2259	. . . . . . . . . . . . 13
294		5t2e10 9876	. . . . . . . . . . . . . 14 ;
295	75	addlidi 8469	. . . . . . . . . . . . . 14
296	61, 56, 54, 294, 295	decaddi 9836	. . . . . . . . . . . . 13 ;
297	13, 54, 56, 54, 286, 291, 13, 54, 61, 293, 296	decmac 9828	. . . . . . . . . . . 12 ; ;
298	235	oveq1i 6095	. . . . . . . . . . . . 13
299		7p6e13 9854	. . . . . . . . . . . . . 14 ;
300	74, 179, 299	addcomli 8471	. . . . . . . . . . . . 13 ;
301	298, 300	eqtri 2259	. . . . . . . . . . . 12 ;
302	230, 53, 5, 97, 284, 289, 13, 53, 61, 297, 301	decmac 9828	. . . . . . . . . . 11 ;; ; ; ;;
303	231	nn0cni 9575	. . . . . . . . . . . . . 14 ;;
304	303	mulridi 8328	. . . . . . . . . . . . 13 ;; ;;
305	304	oveq1i 6095	. . . . . . . . . . . 12 ;; ;;
306	303	addridi 8468	. . . . . . . . . . . 12 ;; ;;
307	305, 306	eqtri 2259	. . . . . . . . . . 11 ;; ;;
308	13, 61, 273, 56, 274, 283, 231, 53, 230, 302, 307	decma2c 9829	. . . . . . . . . 10 ;; ; ; ;; ;;;
309	97	dec0h 9798	. . . . . . . . . . 11 ;
310	78	addlidi 8469	. . . . . . . . . . . . . 14
311	310	oveq2i 6096	. . . . . . . . . . . . 13
312		8t2e16 9891	. . . . . . . . . . . . . . 15 ;
313	248, 79, 312	mulcomli 8333	. . . . . . . . . . . . . 14 ;
314		6p4e10 9848	. . . . . . . . . . . . . 14 ;
315	61, 59, 5, 313, 247, 314	decaddci2 9838	. . . . . . . . . . . . 13 ;
316	311, 315	eqtri 2259	. . . . . . . . . . . 12 ;
317		8t5e40 9894	. . . . . . . . . . . . . 14 ;
318	248, 75, 317	mulcomli 8333	. . . . . . . . . . . . 13 ;
319	5, 56, 53, 318, 185	decaddi 9836	. . . . . . . . . . . 12 ;
320	13, 54, 56, 53, 286, 187, 137, 53, 5, 316, 319	decmac 9828	. . . . . . . . . . 11 ; ;;
321		8t3e24 9892	. . . . . . . . . . . . 13 ;
322	248, 102, 321	mulcomli 8333	. . . . . . . . . . . 12 ;
323		2p1e3 9438	. . . . . . . . . . . 12
324		7p4e11 9852	. . . . . . . . . . . . 13 ;
325	74, 78, 324	addcomli 8471	. . . . . . . . . . . 12 ;
326	13, 5, 97, 322, 323, 61, 325	decaddci 9837	. . . . . . . . . . 11 ;
327	230, 53, 56, 97, 284, 309, 137, 61, 53, 320, 326	decmac 9828	. . . . . . . . . 10 ;; ;;;
328	232, 137, 267, 97, 269, 270, 231, 61, 272, 308, 327	decma2c 9829	. . . . . . . . 9 ;; ;; ;; ;;;;
329	61, 5, 53, 253, 244	decaddi 9836	. . . . . . . . . . 11 ;
330	53, 54, 13, 77, 221	decaddi 9836	. . . . . . . . . . 11 ;
331	13, 54, 13, 286, 97, 97, 53, 329, 330	decrmac 9834	. . . . . . . . . 10 ; ;;
332	97, 230, 53, 284, 61, 13, 331, 178	decmul1c 9841	. . . . . . . . 9 ;; ;;;
333	231, 233, 97, 266, 61, 268, 328, 332	decmul2c 9842	. . . . . . . 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 6096	. . . . . . . . . . . . 13
340	339, 175	eqtri 2259	. . . . . . . . . . . 12 ;
341	54, 54, 56, 13, 337, 338, 97, 97, 53, 340, 330	decmac 9828	. . . . . . . . . . 11 ; ;;
342	13, 61, 13, 178, 172	decaddi 9836	. . . . . . . . . . 11 ;
343	226, 53, 56, 13, 336, 200, 97, 53, 13, 341, 342	decmac 9828	. . . . . . . . . 10 ;; ;;;
344	97, 227, 53, 335, 61, 13, 343, 178	decmul1c 9841	. . . . . . . . 9 ;;; ;;;;
345	74	mullidi 8329	. . . . . . . . 9
346	97, 228, 61, 334, 97, 344, 345	decmul1 9840	. . . . . . . 8 ;;;; ;;;;;
347	97, 229, 61, 333, 97, 346, 345	decmul1 9840	. . . . . . 7 ;; ;;;;;;
348	147, 225, 347	3brtr4i 4160	. . . . . 6 ;;;; ; ;;
349	97, 53	deccl 9791	. . . . . . . . 9 ;
350	128, 349	nn0mulcli 9601	. . . . . . . 8 ;;;; ;
351	350	nn0rei 9574	. . . . . . 7 ;;;; ;
352	53, 97	nn0expcli 11002	. . . . . . . . . 10
353	231, 352	nn0mulcli 9601	. . . . . . . . 9 ;;
354	353, 97	nn0mulcli 9601	. . . . . . . 8 ;;
355	354	nn0rei 9574	. . . . . . 7 ;;
356	66	nnrei 9313	. . . . . . 7
357	66	nngt0i 9334	. . . . . . 7
358	351, 355, 356, 357	ltmul1ii 9258	. . . . . 6 ;;;; ; ;; ;;;; ; ;;
359	348, 358	mpbi 145	. . . . 5 ;;;; ; ;;
360	128	nn0cni 9575	. . . . . . 7 ;;;;
361	349	nn0cni 9575	. . . . . . 7 ;
362	360, 361, 75	mulassi 8335	. . . . . 6 ;;;; ; ;;;; ;
363	53, 54, 159, 76	decsuc 9807	. . . . . . . 8 ;
364	75, 102, 207	mulcomli 8333	. . . . . . . 8 ;
365	54, 97, 53, 148, 54, 61, 363, 364	decmul1c 9841	. . . . . . 7 ; ;;
366	365	oveq2i 6096	. . . . . 6 ;;;; ; ;;;; ;;
367	362, 366	eqtri 2259	. . . . 5 ;;;; ; ;;;; ;;
368	303, 100	mulcli 8331	. . . . . . 7 ;;
369	368, 74, 75	mulassi 8335	. . . . . 6 ;; ;;
370	74, 75	mulcomi 8332	. . . . . . . 8
371	370	oveq2i 6096	. . . . . . 7 ;; ;;
372	303, 100, 101	mulassi 8335	. . . . . . 7 ;; ;;
373	371, 372	eqtri 2259	. . . . . 6 ;; ;;
374	369, 373	eqtri 2259	. . . . 5 ;; ;;
375	359, 367, 374	3brtr3i 4159	. . . 4 ;;;; ;; ;;
376	53, 59	deccl 9791	. . . . . . . 8 ;
377	376, 66	decnncl 9796	. . . . . . 7 ;;
378	377	nnrei 9313	. . . . . 6 ;;
379	377	nngt0i 9334	. . . . . 6 ;;
380	378, 379	pm3.2i 272	. . . . 5 ;; $/\$ ;;
381	231	nn0rei 9574	. . . . 5 ;;
382		lt2mul2div 9209	. . . . 5 ;;;; $/\$ ;; $/\$ ;; $/\$ ;; $/\$ $/\$ ;;;; ;; ;; ;;;; ;; ;;
383	129, 380, 381, 133, 382	mp4an 431	. . . 4 ;;;; ;; ;; ;;;; ;; ;;
384	375, 383	mpbi 145	. . 3 ;;;; ;; ;;
385		nndivre 9340	. . . . 5 ;;;; $/\$ ;;;;
386	129, 130, 385	mp2an 430	. . . 4 ;;;;
387		nndivre 9340	. . . . 5 ;; $/\$ ;; ;; ;;
388	381, 377, 387	mp2an 430	. . . 4 ;; ;;
389	127, 386, 388	lelttri 8431	. . 3 ;;;; $/\$ ;;;; ;; ;; ;; ;;
390	136, 384, 389	mp2an 430	. 2 ;; ;;
391	28, 127, 388	lelttri 8431	. 2 $/\$ ;; ;; ;; ;;
392	51, 390, 391	mp2an 430	1 ;; ;;

Colors of variables: wff set class

This proof depends on syntax axioms: $/\$ wa 104

wb 105 $/\$ w3a 1009

wceq 1402

wtru 1403

wcel 2209 class class class wbr 4130

cmpt 4192

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

cdiv 9002

cn 9304

c2 9355

c3 9356

c4 9357

c5 9358

c6 9359

c7 9360

c8 9361

c9 9362

cn0 9563

cz 9644 ;cdc 9777

crp 10054

cicc 10293

cfz 10411

cseq 10884

cexp 10975

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-dec 9778 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: birthdaylog2 16090

W3C validator