log2ublem3 - Metamath Proof Explorer

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

Theorem log2ublem3 23000

Description: Lemma for log2ub 23001. In decimal, this is a proof that the first four terms of the series for

is less than

. (Contributed by Mario Carneiro, 17-Apr-2015.)

**Assertion**
Ref	Expression
log2ublem3	;;;;

**Proof of Theorem log2ublem3**
Step	Hyp	Ref	Expression
1		0le0 10614	. . . . . . 7
2		0re 9585	. . . . . . . . . . . . 13
3		ltm1 10371	. . . . . . . . . . . . 13
4	2, 3	ax-mp 5	. . . . . . . . . . . 12
5		0z 10864	. . . . . . . . . . . . 13
6		peano2zm 10895	. . . . . . . . . . . . . 14
7	5, 6	ax-mp 5	. . . . . . . . . . . . 13
8		fzn 11691	. . . . . . . . . . . . 13 $/\$
9	5, 7, 8	mp2an 672	. . . . . . . . . . . 12
10	4, 9	mpbi 208	. . . . . . . . . . 11
11	10	sumeq1i 13469	. . . . . . . . . 10
12		sum0 13492	. . . . . . . . . 10
13	11, 12	eqtri 2489	. . . . . . . . 9
14	13	oveq2i 6286	. . . . . . . 8
15		3cn 10599	. . . . . . . . . . 11
16		7nn0 10806	. . . . . . . . . . 11
17		expcl 12140	. . . . . . . . . . 11 $/\$
18	15, 16, 17	mp2an 672	. . . . . . . . . 10
19		5cn 10604	. . . . . . . . . . 11
20		7cn 10608	. . . . . . . . . . 11
21	19, 20	mulcli 9590	. . . . . . . . . 10
22	18, 21	mulcli 9590	. . . . . . . . 9
23	22	mul01i 9758	. . . . . . . 8
24	14, 23	eqtri 2489	. . . . . . 7
25		2cn 10595	. . . . . . . 8
26	25	mul01i 9758	. . . . . . 7
27	1, 24, 26	3brtr4i 4468	. . . . . 6
28		0nn0 10799	. . . . . 6
29		2nn0 10801	. . . . . . . . . 10
30		5nn0 10804	. . . . . . . . . 10
31	29, 30	deccl 10979	. . . . . . . . 9 ;
32	31, 30	deccl 10979	. . . . . . . 8 ;;
33		1nn0 10800	. . . . . . . 8
34	32, 33	deccl 10979	. . . . . . 7 ;;;
35	34, 30	deccl 10979	. . . . . 6 ;;;;
36		eqid 2460	. . . . . 6
37	35	nn0cni 10796	. . . . . . 7 ;;;;
38	37	addid2i 9756	. . . . . 6 ;;;; ;;;;
39		3nn0 10802	. . . . . 6
40	15	addid1i 9755	. . . . . 6
41	37	mulid2i 9588	. . . . . . 7 ;;;; ;;;;
42	26	oveq1i 6285	. . . . . . . . 9
43		0p1e1 10636	. . . . . . . . 9
44	42, 43	eqtri 2489	. . . . . . . 8
45	44	oveq1i 6285	. . . . . . 7 ;;;; ;;;;
46	30, 16	nn0mulcli 10823	. . . . . . . 8
47	16, 29	deccl 10979	. . . . . . . 8 ;
48		9nn0 10808	. . . . . . . 8
49		2p1e3 10648	. . . . . . . . 9
50		8nn0 10807	. . . . . . . . . 10
51		1p1e2 10638	. . . . . . . . . . 11
52		9cn 10612	. . . . . . . . . . . . . 14
53		exp1 12128	. . . . . . . . . . . . . 14
54	52, 53	ax-mp 5	. . . . . . . . . . . . 13
55	54	oveq1i 6285	. . . . . . . . . . . 12
56		9t9e81 11067	. . . . . . . . . . . 12 ;
57	55, 56	eqtri 2489	. . . . . . . . . . 11 ;
58	48, 33, 51, 57	numexpp1 14412	. . . . . . . . . 10 ;
59		8cn 10610	. . . . . . . . . . . . 13
60		9t8e72 11066	. . . . . . . . . . . . 13 ;
61	52, 59, 60	mulcomli 9592	. . . . . . . . . . . 12 ;
62	61	oveq1i 6285	. . . . . . . . . . 11 ;
63	47	nn0cni 10796	. . . . . . . . . . . 12 ;
64	63	addid1i 9755	. . . . . . . . . . 11 ; ;
65	62, 64	eqtri 2489	. . . . . . . . . 10 ;
66	52	mulid2i 9588	. . . . . . . . . . 11
67	48	dec0h 10981	. . . . . . . . . . 11 ;
68	66, 67	eqtri 2489	. . . . . . . . . 10 ;
69	48, 50, 33, 58, 48, 28, 65, 68	decmul1c 11012	. . . . . . . . 9 ;;
70	48, 29, 49, 69	numexpp1 14412	. . . . . . . 8 ;;
71	39, 33	deccl 10979	. . . . . . . 8 ;
72		eqid 2460	. . . . . . . . 9 ; ;
73		eqid 2460	. . . . . . . . 9 ; ;
74		7t5e35 11050	. . . . . . . . . . 11 ;
75	20, 19, 74	mulcomli 9592	. . . . . . . . . 10 ;
76		7p3e10 10670	. . . . . . . . . . . 12
77	20, 15, 76	addcomli 9760	. . . . . . . . . . 11
78		dec10 10995	. . . . . . . . . . 11 ;
79	77, 78	eqtri 2489	. . . . . . . . . 10 ;
80		ax-1cn 9539	. . . . . . . . . . . . 13
81		3p1e4 10650	. . . . . . . . . . . . 13
82	15, 80, 81	addcomli 9760	. . . . . . . . . . . 12
83	82	oveq2i 6286	. . . . . . . . . . 11
84		4nn0 10803	. . . . . . . . . . . 12
85		7t3e21 11048	. . . . . . . . . . . . 13 ;
86	20, 15, 85	mulcomli 9592	. . . . . . . . . . . 12 ;
87		4cn 10602	. . . . . . . . . . . . 13
88		4p1e5 10651	. . . . . . . . . . . . 13
89	87, 80, 88	addcomli 9760	. . . . . . . . . . . 12
90	29, 33, 84, 86, 89	decaddi 11009	. . . . . . . . . . 11 ;
91	83, 90	eqtri 2489	. . . . . . . . . 10 ;
92	75	oveq1i 6285	. . . . . . . . . . 11 ;
93	39, 30	deccl 10979	. . . . . . . . . . . . 13 ;
94	93	nn0cni 10796	. . . . . . . . . . . 12 ;
95	94	addid1i 9755	. . . . . . . . . . 11 ; ;
96	92, 95	eqtri 2489	. . . . . . . . . 10 ;
97	39, 30, 33, 28, 75, 79, 16, 30, 39, 91, 96	decmac 11004	. . . . . . . . 9 ;;
98	33	dec0h 10981	. . . . . . . . . 10 ;
99		3t2e6 10676	. . . . . . . . . . . 12
100	99, 43	oveq12i 6287	. . . . . . . . . . 11
101		6p1e7 10653	. . . . . . . . . . 11
102	100, 101	eqtri 2489	. . . . . . . . . 10
103		5t2e10 10679	. . . . . . . . . . . 12
104	103, 78	eqtri 2489	. . . . . . . . . . 11 ;
105	33, 28, 43, 104	decsuc 10988	. . . . . . . . . 10 ;
106	39, 30, 28, 33, 75, 98, 29, 33, 33, 102, 105	decmac 11004	. . . . . . . . 9 ;
107	16, 29, 39, 33, 72, 73, 46, 33, 16, 97, 106	decma2c 11005	. . . . . . . 8 ; ; ;;;
108		9t3e27 11061	. . . . . . . . . . 11 ;
109	52, 15, 108	mulcomli 9592	. . . . . . . . . 10 ;
110		7p4e11 11017	. . . . . . . . . 10 ;
111	29, 16, 84, 109, 49, 33, 110	decaddci 11010	. . . . . . . . 9 ;
112		9t5e45 11063	. . . . . . . . . 10 ;
113	52, 19, 112	mulcomli 9592	. . . . . . . . 9 ;
114	48, 39, 30, 75, 30, 84, 111, 113	decmul1c 11012	. . . . . . . 8 ;;
115	46, 47, 48, 70, 30, 71, 107, 114	decmul2c 11013	. . . . . . 7 ;;;;
116	41, 45, 115	3eqtr4ri 2500	. . . . . 6 ;;;;
117	27, 28, 35, 28, 36, 38, 39, 40, 116	log2ublem2 22999	. . . . 5 ;;;;
118	48, 84	deccl 10979	. . . . . 6 ;
119	118, 30	deccl 10979	. . . . 5 ;;
120		1m1e0 10593	. . . . 5
121		eqid 2460	. . . . . 6 ;;;; ;;;;
122		eqid 2460	. . . . . 6 ;; ;;
123		6nn0 10805	. . . . . . . . 9
124	29, 123	deccl 10979	. . . . . . . 8 ;
125	124, 84	deccl 10979	. . . . . . 7 ;;
126		5p1e6 10652	. . . . . . 7
127		eqid 2460	. . . . . . . 8 ;;; ;;;
128		eqid 2460	. . . . . . . 8 ; ;
129		eqid 2460	. . . . . . . . 9 ;; ;;
130		eqid 2460	. . . . . . . . . 10 ; ;
131	29, 30, 126, 130	decsuc 10988	. . . . . . . . 9 ; ;
132		9p5e14 11030	. . . . . . . . . 10 ;
133	52, 19, 132	addcomli 9760	. . . . . . . . 9 ;
134	31, 30, 48, 129, 131, 84, 133	decaddci 11010	. . . . . . . 8 ;; ;;
135	32, 33, 48, 84, 127, 128, 134, 89	decadd 11006	. . . . . . 7 ;;; ; ;;;
136	125, 30, 126, 135	decsuc 10988	. . . . . 6 ;;; ; ;;;
137		5p5e10 10665	. . . . . 6
138	34, 30, 118, 30, 121, 122, 136, 137	decaddc2 11008	. . . . 5 ;;;; ;; ;;;;
139	52	sqvali 12202	. . . . . . . . 9
140		3t3e9 10677	. . . . . . . . . 10
141	140	oveq1i 6285	. . . . . . . . 9
142	139, 141	eqtr4i 2492	. . . . . . . 8
143	15, 15, 52	mulassi 9594	. . . . . . . 8
144	142, 143	eqtri 2489	. . . . . . 7
145	144	oveq2i 6286	. . . . . 6
146	15, 52	mulcli 9590	. . . . . . . 8
147	21, 15, 146	mul12i 9763	. . . . . . 7
148	29, 84	deccl 10979	. . . . . . . . 9 ;
149		eqid 2460	. . . . . . . . . 10 ; ;
150	99, 49	oveq12i 6287	. . . . . . . . . . 11
151		6p3e9 10667	. . . . . . . . . . 11
152	150, 151	eqtri 2489	. . . . . . . . . 10
153	87	addid2i 9756	. . . . . . . . . . 11
154	33, 28, 84, 104, 153	decaddi 11009	. . . . . . . . . 10 ;
155	39, 30, 29, 84, 75, 149, 29, 84, 33, 152, 154	decmac 11004	. . . . . . . . 9 ; ;
156	29, 33, 39, 86, 82	decaddi 11009	. . . . . . . . . 10 ;
157	16, 39, 30, 75, 30, 39, 156, 75	decmul1c 11012	. . . . . . . . 9 ;;
158	46, 29, 16, 109, 30, 148, 155, 157	decmul2c 11013	. . . . . . . 8 ;;
159	158	oveq2i 6286	. . . . . . 7 ;;
160	147, 159	eqtri 2489	. . . . . 6 ;;
161		df-3 10584	. . . . . . . 8
162	25	mulid1i 9587	. . . . . . . . 9
163	162	oveq1i 6285	. . . . . . . 8
164	161, 163	eqtr4i 2492	. . . . . . 7
165	164	oveq1i 6285	. . . . . 6 ;; ;;
166	145, 160, 165	3eqtri 2493	. . . . 5 ;;
167	117, 35, 119, 33, 120, 138, 29, 49, 166	log2ublem2 22999	. . . 4 ;;;;
168	125, 123	deccl 10979	. . . . 5 ;;;
169	168, 28	deccl 10979	. . . 4 ;;;;
170	123, 39	deccl 10979	. . . 4 ;
171		2m1e1 10639	. . . 4
172		eqid 2460	. . . . 5 ;;;; ;;;;
173		eqid 2460	. . . . 5 ; ;
174		eqid 2460	. . . . . 6 ;;; ;;;
175		eqid 2460	. . . . . . 7 ;; ;;
176	124, 84, 88, 175	decsuc 10988	. . . . . 6 ;; ;;
177		6p6e12 11016	. . . . . 6 ;
178	125, 123, 123, 174, 176, 29, 177	decaddci 11010	. . . . 5 ;;; ;;;
179	15	addid2i 9756	. . . . 5
180	168, 28, 123, 39, 172, 173, 178, 179	decadd 11006	. . . 4 ;;;; ; ;;;;
181		1p2e3 10649	. . . 4
182	54	oveq2i 6286	. . . . 5
183	19, 20, 52	mulassi 9594	. . . . . 6
184		9t7e63 11065	. . . . . . . 8 ;
185	52, 20, 184	mulcomli 9592	. . . . . . 7 ;
186	185	oveq2i 6286	. . . . . 6 ;
187	183, 186	eqtri 2489	. . . . 5 ;
188		df-5 10586	. . . . . . 7
189		2t2e4 10674	. . . . . . . 8
190	189	oveq1i 6285	. . . . . . 7
191	188, 190	eqtr4i 2492	. . . . . 6
192	191	oveq1i 6285	. . . . 5 ; ;
193	182, 187, 192	3eqtri 2493	. . . 4 ;
194	167, 169, 170, 29, 171, 180, 33, 181, 193	log2ublem2 22999	. . 3 ;;;;
195	124, 30	deccl 10979	. . . . 5 ;;
196	195, 29	deccl 10979	. . . 4 ;;;
197	196, 39	deccl 10979	. . 3 ;;;;
198		3m1e2 10641	. . 3
199		eqid 2460	. . . 4 ;;;; ;;;;
200		5p3e8 10663	. . . . 5
201	19, 15, 200	addcomli 9760	. . . 4
202	196, 39, 30, 199, 201	decaddi 11009	. . 3 ;;;; ;;;;
203	20, 19	mulcli 9590	. . . . 5
204	203	mulid1i 9587	. . . 4
205	19, 20	mulcomi 9591	. . . . 5
206		exp0 12126	. . . . . 6
207	52, 206	ax-mp 5	. . . . 5
208	205, 207	oveq12i 6287	. . . 4
209	15, 25, 99	mulcomli 9592	. . . . . . 7
210	209	oveq1i 6285	. . . . . 6
211		df-7 10588	. . . . . 6
212	210, 211	eqtr4i 2492	. . . . 5
213	212	oveq1i 6285	. . . 4
214	204, 208, 213	3eqtr4i 2499	. . 3
215	194, 197, 30, 39, 198, 202, 28, 179, 214	log2ublem2 22999	. 2 ;;;;
216		eqid 2460	. . 3 ;;;; ;;;;
217		eqid 2460	. . . 4 ;;; ;;;
218		eqid 2460	. . . . 5 ;; ;;
219		00id 9743	. . . . . 6
220	28	dec0h 10981	. . . . . 6 ;
221	219, 220	eqtri 2489	. . . . 5 ;
222		eqid 2460	. . . . . 6 ; ;
223	43, 98	eqtri 2489	. . . . . 6 ;
224	189, 43	oveq12i 6287	. . . . . . 7
225	224, 88	eqtri 2489	. . . . . 6
226		6cn 10606	. . . . . . . 8
227		6t2e12 11042	. . . . . . . 8 ;
228	226, 25, 227	mulcomli 9592	. . . . . . 7 ;
229	33, 29, 49, 228	decsuc 10988	. . . . . 6 ;
230	29, 123, 28, 33, 222, 223, 29, 39, 33, 225, 229	decma2c 11005	. . . . 5 ; ;
231	19, 25, 103	mulcomli 9592	. . . . . . 7
232	231	oveq1i 6285	. . . . . 6
233		dec10p 10994	. . . . . 6 ;
234	232, 233	eqtri 2489	. . . . 5 ;
235	124, 30, 28, 28, 218, 221, 29, 28, 33, 230, 234	decma2c 11005	. . . 4 ;; ;;
236	30	dec0h 10981	. . . . 5 ;
237	190, 88, 236	3eqtri 2493	. . . 4 ;
238	195, 29, 28, 33, 217, 98, 29, 30, 28, 235, 237	decma2c 11005	. . 3 ;;; ;;;
239		8t2e16 11053	. . . 4 ;
240	59, 25, 239	mulcomli 9592	. . 3 ;
241	29, 196, 50, 216, 123, 33, 238, 240	decmul2c 11013	. 2 ;;;; ;;;;
242	215, 241	breqtri 4463	1 ;;;;

Colors of variables: wff setvar class

Syntax hints:

wb 184

wceq 1374

wcel 1762

c0 3778 class class class wbr 4440 (class class class)co 6275

cc 9479

cr 9480

cc0 9481

c1 9482

caddc 9484

cmul 9486

clt 9617

cle 9618

cmin 9794

cdiv 10195

c2 10574

c3 10575

c4 10576

c5 10577

c6 10578

c7 10579

c8 10580

c9 10581

c10 10582

cn0 10784

cz 10853 ;cdc 10965

cfz 11661

cexp 12122

csu 13457

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1714 ax-7 1734 ax-8 1764 ax-9 1766 ax-10 1781 ax-11 1786 ax-12 1798 ax-13 1961 ax-ext 2438 ax-rep 4551 ax-sep 4561 ax-nul 4569 ax-pow 4618 ax-pr 4679 ax-un 6567 ax-inf2 8047 ax-cnex 9537 ax-resscn 9538 ax-1cn 9539 ax-icn 9540 ax-addcl 9541 ax-addrcl 9542 ax-mulcl 9543 ax-mulrcl 9544 ax-mulcom 9545 ax-addass 9546 ax-mulass 9547 ax-distr 9548 ax-i2m1 9549 ax-1ne0 9550 ax-1rid 9551 ax-rnegex 9552 ax-rrecex 9553 ax-cnre 9554 ax-pre-lttri 9555 ax-pre-lttrn 9556 ax-pre-ltadd 9557 ax-pre-mulgt0 9558 ax-pre-sup 9559

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 969 df-3an 970 df-tru 1377 df-fal 1380 df-ex 1592 df-nf 1595 df-sb 1707 df-eu 2272 df-mo 2273 df-clab 2446 df-cleq 2452 df-clel 2455 df-nfc 2610 df-ne 2657 df-nel 2658 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3108 df-sbc 3325 df-csb 3429 df-dif 3472 df-un 3474 df-in 3476 df-ss 3483 df-pss 3485 df-nul 3779 df-if 3933 df-pw 4005 df-sn 4021 df-pr 4023 df-tp 4025 df-op 4027 df-uni 4239 df-int 4276 df-iun 4320 df-br 4441 df-opab 4499 df-mpt 4500 df-tr 4534 df-eprel 4784 df-id 4788 df-po 4793 df-so 4794 df-fr 4831 df-se 4832 df-we 4833 df-ord 4874 df-on 4875 df-lim 4876 df-suc 4877 df-xp 4998 df-rel 4999 df-cnv 5000 df-co 5001 df-dm 5002 df-rn 5003 df-res 5004 df-ima 5005 df-iota 5542 df-fun 5581 df-fn 5582 df-f 5583 df-f1 5584 df-fo 5585 df-f1o 5586 df-fv 5587 df-isom 5588 df-riota 6236 df-ov 6278 df-oprab 6279 df-mpt2 6280 df-om 6672 df-1st 6774 df-2nd 6775 df-recs 7032 df-rdg 7066 df-1o 7120 df-oadd 7124 df-er 7301 df-en 7507 df-dom 7508 df-sdom 7509 df-fin 7510 df-sup 7890 df-oi 7924 df-card 8309 df-pnf 9619 df-mnf 9620 df-xr 9621 df-ltxr 9622 df-le 9623 df-sub 9796 df-neg 9797 df-div 10196 df-nn 10526 df-2 10583 df-3 10584 df-4 10585 df-5 10586 df-6 10587 df-7 10588 df-8 10589 df-9 10590 df-10 10591 df-n0 10785 df-z 10854 df-dec 10966 df-uz 11072 df-rp 11210 df-fz 11662 df-fzo 11782 df-seq 12064 df-exp 12123 df-hash 12361 df-cj 12882 df-re 12883 df-im 12884 df-sqr 13018 df-abs 13019 df-clim 13260 df-sum 13458

This theorem is referenced by: log2ub 23001

W3C validator