log2ublem3 - Metamath Proof Explorer

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

Theorem log2ublem3 23860

Description: Lemma for log2ub 23861. 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 10699	. . . . . . 7
2		0re 9643	. . . . . . . . . . . . 13
3		ltm1 10445	. . . . . . . . . . . . 13
4	2, 3	ax-mp 5	. . . . . . . . . . . 12
5		0z 10948	. . . . . . . . . . . . 13
6		peano2zm 10980	. . . . . . . . . . . . . 14
7	5, 6	ax-mp 5	. . . . . . . . . . . . 13
8		fzn 11815	. . . . . . . . . . . . 13 $/\$
9	5, 7, 8	mp2an 676	. . . . . . . . . . . 12
10	4, 9	mpbi 211	. . . . . . . . . . 11
11	10	sumeq1i 13751	. . . . . . . . . 10
12		sum0 13774	. . . . . . . . . 10
13	11, 12	eqtri 2451	. . . . . . . . 9
14	13	oveq2i 6312	. . . . . . . 8
15		3cn 10684	. . . . . . . . . . 11
16		7nn0 10891	. . . . . . . . . . 11
17		expcl 12289	. . . . . . . . . . 11 $/\$
18	15, 16, 17	mp2an 676	. . . . . . . . . 10
19		5cn 10689	. . . . . . . . . . 11
20		7cn 10693	. . . . . . . . . . 11
21	19, 20	mulcli 9648	. . . . . . . . . 10
22	18, 21	mulcli 9648	. . . . . . . . 9
23	22	mul01i 9823	. . . . . . . 8
24	14, 23	eqtri 2451	. . . . . . 7
25		2cn 10680	. . . . . . . 8
26	25	mul01i 9823	. . . . . . 7
27	1, 24, 26	3brtr4i 4449	. . . . . 6
28		0nn0 10884	. . . . . 6
29		2nn0 10886	. . . . . . . . . 10
30		5nn0 10889	. . . . . . . . . 10
31	29, 30	deccl 11065	. . . . . . . . 9 ;
32	31, 30	deccl 11065	. . . . . . . 8 ;;
33		1nn0 10885	. . . . . . . 8
34	32, 33	deccl 11065	. . . . . . 7 ;;;
35	34, 30	deccl 11065	. . . . . 6 ;;;;
36		eqid 2422	. . . . . 6
37	35	nn0cni 10881	. . . . . . 7 ;;;;
38	37	addid2i 9821	. . . . . 6 ;;;; ;;;;
39		3nn0 10887	. . . . . 6
40	15	addid1i 9820	. . . . . 6
41	37	mulid2i 9646	. . . . . . 7 ;;;; ;;;;
42	26	oveq1i 6311	. . . . . . . . 9
43		0p1e1 10721	. . . . . . . . 9
44	42, 43	eqtri 2451	. . . . . . . 8
45	44	oveq1i 6311	. . . . . . 7 ;;;; ;;;;
46	30, 16	nn0mulcli 10908	. . . . . . . 8
47	16, 29	deccl 11065	. . . . . . . 8 ;
48		9nn0 10893	. . . . . . . 8
49		2p1e3 10733	. . . . . . . . 9
50		8nn0 10892	. . . . . . . . . 10
51		1p1e2 10723	. . . . . . . . . . 11
52		9cn 10697	. . . . . . . . . . . . . 14
53		exp1 12277	. . . . . . . . . . . . . 14
54	52, 53	ax-mp 5	. . . . . . . . . . . . 13
55	54	oveq1i 6311	. . . . . . . . . . . 12
56		9t9e81 11153	. . . . . . . . . . . 12 ;
57	55, 56	eqtri 2451	. . . . . . . . . . 11 ;
58	48, 33, 51, 57	numexpp1 15037	. . . . . . . . . 10 ;
59		8cn 10695	. . . . . . . . . . . . 13
60		9t8e72 11152	. . . . . . . . . . . . 13 ;
61	52, 59, 60	mulcomli 9650	. . . . . . . . . . . 12 ;
62	61	oveq1i 6311	. . . . . . . . . . 11 ;
63	47	nn0cni 10881	. . . . . . . . . . . 12 ;
64	63	addid1i 9820	. . . . . . . . . . 11 ; ;
65	62, 64	eqtri 2451	. . . . . . . . . 10 ;
66	52	mulid2i 9646	. . . . . . . . . . 11
67	48	dec0h 11067	. . . . . . . . . . 11 ;
68	66, 67	eqtri 2451	. . . . . . . . . 10 ;
69	48, 50, 33, 58, 48, 28, 65, 68	decmul1c 11098	. . . . . . . . 9 ;;
70	48, 29, 49, 69	numexpp1 15037	. . . . . . . 8 ;;
71	39, 33	deccl 11065	. . . . . . . 8 ;
72		eqid 2422	. . . . . . . . 9 ; ;
73		eqid 2422	. . . . . . . . 9 ; ;
74		7t5e35 11136	. . . . . . . . . . 11 ;
75	20, 19, 74	mulcomli 9650	. . . . . . . . . 10 ;
76		7p3e10 10755	. . . . . . . . . . . 12
77	20, 15, 76	addcomli 9825	. . . . . . . . . . 11
78		dec10 11081	. . . . . . . . . . 11 ;
79	77, 78	eqtri 2451	. . . . . . . . . 10 ;
80		ax-1cn 9597	. . . . . . . . . . . . 13
81		3p1e4 10735	. . . . . . . . . . . . 13
82	15, 80, 81	addcomli 9825	. . . . . . . . . . . 12
83	82	oveq2i 6312	. . . . . . . . . . 11
84		4nn0 10888	. . . . . . . . . . . 12
85		7t3e21 11134	. . . . . . . . . . . . 13 ;
86	20, 15, 85	mulcomli 9650	. . . . . . . . . . . 12 ;
87		4cn 10687	. . . . . . . . . . . . 13
88		4p1e5 10736	. . . . . . . . . . . . 13
89	87, 80, 88	addcomli 9825	. . . . . . . . . . . 12
90	29, 33, 84, 86, 89	decaddi 11095	. . . . . . . . . . 11 ;
91	83, 90	eqtri 2451	. . . . . . . . . 10 ;
92	75	oveq1i 6311	. . . . . . . . . . 11 ;
93	39, 30	deccl 11065	. . . . . . . . . . . . 13 ;
94	93	nn0cni 10881	. . . . . . . . . . . 12 ;
95	94	addid1i 9820	. . . . . . . . . . 11 ; ;
96	92, 95	eqtri 2451	. . . . . . . . . 10 ;
97	39, 30, 33, 28, 75, 79, 16, 30, 39, 91, 96	decmac 11090	. . . . . . . . 9 ;;
98	33	dec0h 11067	. . . . . . . . . 10 ;
99		3t2e6 10761	. . . . . . . . . . . 12
100	99, 43	oveq12i 6313	. . . . . . . . . . 11
101		6p1e7 10738	. . . . . . . . . . 11
102	100, 101	eqtri 2451	. . . . . . . . . 10
103		5t2e10 10764	. . . . . . . . . . . 12
104	103, 78	eqtri 2451	. . . . . . . . . . 11 ;
105	33, 28, 43, 104	decsuc 11074	. . . . . . . . . 10 ;
106	39, 30, 28, 33, 75, 98, 29, 33, 33, 102, 105	decmac 11090	. . . . . . . . 9 ;
107	16, 29, 39, 33, 72, 73, 46, 33, 16, 97, 106	decma2c 11091	. . . . . . . 8 ; ; ;;;
108		9t3e27 11147	. . . . . . . . . . 11 ;
109	52, 15, 108	mulcomli 9650	. . . . . . . . . 10 ;
110		7p4e11 11103	. . . . . . . . . 10 ;
111	29, 16, 84, 109, 49, 33, 110	decaddci 11096	. . . . . . . . 9 ;
112		9t5e45 11149	. . . . . . . . . 10 ;
113	52, 19, 112	mulcomli 9650	. . . . . . . . 9 ;
114	48, 39, 30, 75, 30, 84, 111, 113	decmul1c 11098	. . . . . . . 8 ;;
115	46, 47, 48, 70, 30, 71, 107, 114	decmul2c 11099	. . . . . . 7 ;;;;
116	41, 45, 115	3eqtr4ri 2462	. . . . . 6 ;;;;
117	27, 28, 35, 28, 36, 38, 39, 40, 116	log2ublem2 23859	. . . . 5 ;;;;
118	48, 84	deccl 11065	. . . . . 6 ;
119	118, 30	deccl 11065	. . . . 5 ;;
120		1m1e0 10678	. . . . 5
121		eqid 2422	. . . . . 6 ;;;; ;;;;
122		eqid 2422	. . . . . 6 ;; ;;
123		6nn0 10890	. . . . . . . . 9
124	29, 123	deccl 11065	. . . . . . . 8 ;
125	124, 84	deccl 11065	. . . . . . 7 ;;
126		5p1e6 10737	. . . . . . 7
127		eqid 2422	. . . . . . . 8 ;;; ;;;
128		eqid 2422	. . . . . . . 8 ; ;
129		eqid 2422	. . . . . . . . 9 ;; ;;
130		eqid 2422	. . . . . . . . . 10 ; ;
131	29, 30, 126, 130	decsuc 11074	. . . . . . . . 9 ; ;
132		9p5e14 11116	. . . . . . . . . 10 ;
133	52, 19, 132	addcomli 9825	. . . . . . . . 9 ;
134	31, 30, 48, 129, 131, 84, 133	decaddci 11096	. . . . . . . 8 ;; ;;
135	32, 33, 48, 84, 127, 128, 134, 89	decadd 11092	. . . . . . 7 ;;; ; ;;;
136	125, 30, 126, 135	decsuc 11074	. . . . . 6 ;;; ; ;;;
137		5p5e10 10750	. . . . . 6
138	34, 30, 118, 30, 121, 122, 136, 137	decaddc2 11094	. . . . 5 ;;;; ;; ;;;;
139	52	sqvali 12353	. . . . . . . . 9
140		3t3e9 10762	. . . . . . . . . 10
141	140	oveq1i 6311	. . . . . . . . 9
142	139, 141	eqtr4i 2454	. . . . . . . 8
143	15, 15, 52	mulassi 9652	. . . . . . . 8
144	142, 143	eqtri 2451	. . . . . . 7
145	144	oveq2i 6312	. . . . . 6
146	15, 52	mulcli 9648	. . . . . . . 8
147	21, 15, 146	mul12i 9828	. . . . . . 7
148	29, 84	deccl 11065	. . . . . . . . 9 ;
149		eqid 2422	. . . . . . . . . 10 ; ;
150	99, 49	oveq12i 6313	. . . . . . . . . . 11
151		6p3e9 10752	. . . . . . . . . . 11
152	150, 151	eqtri 2451	. . . . . . . . . 10
153	87	addid2i 9821	. . . . . . . . . . 11
154	33, 28, 84, 104, 153	decaddi 11095	. . . . . . . . . 10 ;
155	39, 30, 29, 84, 75, 149, 29, 84, 33, 152, 154	decmac 11090	. . . . . . . . 9 ; ;
156	29, 33, 39, 86, 82	decaddi 11095	. . . . . . . . . 10 ;
157	16, 39, 30, 75, 30, 39, 156, 75	decmul1c 11098	. . . . . . . . 9 ;;
158	46, 29, 16, 109, 30, 148, 155, 157	decmul2c 11099	. . . . . . . 8 ;;
159	158	oveq2i 6312	. . . . . . 7 ;;
160	147, 159	eqtri 2451	. . . . . 6 ;;
161		df-3 10669	. . . . . . . 8
162	25	mulid1i 9645	. . . . . . . . 9
163	162	oveq1i 6311	. . . . . . . 8
164	161, 163	eqtr4i 2454	. . . . . . 7
165	164	oveq1i 6311	. . . . . 6 ;; ;;
166	145, 160, 165	3eqtri 2455	. . . . 5 ;;
167	117, 35, 119, 33, 120, 138, 29, 49, 166	log2ublem2 23859	. . . 4 ;;;;
168	125, 123	deccl 11065	. . . . 5 ;;;
169	168, 28	deccl 11065	. . . 4 ;;;;
170	123, 39	deccl 11065	. . . 4 ;
171		2m1e1 10724	. . . 4
172		eqid 2422	. . . . 5 ;;;; ;;;;
173		eqid 2422	. . . . 5 ; ;
174		eqid 2422	. . . . . 6 ;;; ;;;
175		eqid 2422	. . . . . . 7 ;; ;;
176	124, 84, 88, 175	decsuc 11074	. . . . . 6 ;; ;;
177		6p6e12 11102	. . . . . 6 ;
178	125, 123, 123, 174, 176, 29, 177	decaddci 11096	. . . . 5 ;;; ;;;
179	15	addid2i 9821	. . . . 5
180	168, 28, 123, 39, 172, 173, 178, 179	decadd 11092	. . . 4 ;;;; ; ;;;;
181		1p2e3 10734	. . . 4
182	54	oveq2i 6312	. . . . 5
183	19, 20, 52	mulassi 9652	. . . . . 6
184		9t7e63 11151	. . . . . . . 8 ;
185	52, 20, 184	mulcomli 9650	. . . . . . 7 ;
186	185	oveq2i 6312	. . . . . 6 ;
187	183, 186	eqtri 2451	. . . . 5 ;
188		df-5 10671	. . . . . . 7
189		2t2e4 10759	. . . . . . . 8
190	189	oveq1i 6311	. . . . . . 7
191	188, 190	eqtr4i 2454	. . . . . 6
192	191	oveq1i 6311	. . . . 5 ; ;
193	182, 187, 192	3eqtri 2455	. . . 4 ;
194	167, 169, 170, 29, 171, 180, 33, 181, 193	log2ublem2 23859	. . 3 ;;;;
195	124, 30	deccl 11065	. . . . 5 ;;
196	195, 29	deccl 11065	. . . 4 ;;;
197	196, 39	deccl 11065	. . 3 ;;;;
198		3m1e2 10726	. . 3
199		eqid 2422	. . . 4 ;;;; ;;;;
200		5p3e8 10748	. . . . 5
201	19, 15, 200	addcomli 9825	. . . 4
202	196, 39, 30, 199, 201	decaddi 11095	. . 3 ;;;; ;;;;
203	20, 19	mulcli 9648	. . . . 5
204	203	mulid1i 9645	. . . 4
205	19, 20	mulcomi 9649	. . . . 5
206		exp0 12275	. . . . . 6
207	52, 206	ax-mp 5	. . . . 5
208	205, 207	oveq12i 6313	. . . 4
209	15, 25, 99	mulcomli 9650	. . . . . . 7
210	209	oveq1i 6311	. . . . . 6
211		df-7 10673	. . . . . 6
212	210, 211	eqtr4i 2454	. . . . 5
213	212	oveq1i 6311	. . . 4
214	204, 208, 213	3eqtr4i 2461	. . 3
215	194, 197, 30, 39, 198, 202, 28, 179, 214	log2ublem2 23859	. 2 ;;;;
216		eqid 2422	. . 3 ;;;; ;;;;
217		eqid 2422	. . . 4 ;;; ;;;
218		eqid 2422	. . . . 5 ;; ;;
219		00id 9808	. . . . . 6
220	28	dec0h 11067	. . . . . 6 ;
221	219, 220	eqtri 2451	. . . . 5 ;
222		eqid 2422	. . . . . 6 ; ;
223	43, 98	eqtri 2451	. . . . . 6 ;
224	189, 43	oveq12i 6313	. . . . . . 7
225	224, 88	eqtri 2451	. . . . . 6
226		6cn 10691	. . . . . . . 8
227		6t2e12 11128	. . . . . . . 8 ;
228	226, 25, 227	mulcomli 9650	. . . . . . 7 ;
229	33, 29, 49, 228	decsuc 11074	. . . . . 6 ;
230	29, 123, 28, 33, 222, 223, 29, 39, 33, 225, 229	decma2c 11091	. . . . 5 ; ;
231	19, 25, 103	mulcomli 9650	. . . . . . 7
232	231	oveq1i 6311	. . . . . 6
233		dec10p 11080	. . . . . 6 ;
234	232, 233	eqtri 2451	. . . . 5 ;
235	124, 30, 28, 28, 218, 221, 29, 28, 33, 230, 234	decma2c 11091	. . . 4 ;; ;;
236	30	dec0h 11067	. . . . 5 ;
237	190, 88, 236	3eqtri 2455	. . . 4 ;
238	195, 29, 28, 33, 217, 98, 29, 30, 28, 235, 237	decma2c 11091	. . 3 ;;; ;;;
239		8t2e16 11139	. . . 4 ;
240	59, 25, 239	mulcomli 9650	. . 3 ;
241	29, 196, 50, 216, 123, 33, 238, 240	decmul2c 11099	. 2 ;;;; ;;;;
242	215, 241	breqtri 4444	1 ;;;;

Colors of variables: wff setvar class

Syntax hints:

wb 187

wceq 1437

wcel 1868

c0 3761 class class class wbr 4420 (class class class)co 6301

cc 9537

cr 9538

cc0 9539

c1 9540

caddc 9542

cmul 9544

clt 9675

cle 9676

cmin 9860

cdiv 10269

c2 10659

c3 10660

c4 10661

c5 10662

c6 10663

c7 10664

c8 10665

c9 10666

c10 10667

cn0 10869

cz 10937 ;cdc 11051

cfz 11784

cexp 12271

csu 13739

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1839 ax-8 1870 ax-9 1872 ax-10 1887 ax-11 1892 ax-12 1905 ax-13 2053 ax-ext 2400 ax-rep 4533 ax-sep 4543 ax-nul 4551 ax-pow 4598 ax-pr 4656 ax-un 6593 ax-inf2 8148 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616 ax-pre-sup 9617

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2269 df-mo 2270 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2572 df-ne 2620 df-nel 2621 df-ral 2780 df-rex 2781 df-reu 2782 df-rmo 2783 df-rab 2784 df-v 3083 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-pss 3452 df-nul 3762 df-if 3910 df-pw 3981 df-sn 3997 df-pr 3999 df-tp 4001 df-op 4003 df-uni 4217 df-int 4253 df-iun 4298 df-br 4421 df-opab 4480 df-mpt 4481 df-tr 4516 df-eprel 4760 df-id 4764 df-po 4770 df-so 4771 df-fr 4808 df-se 4809 df-we 4810 df-xp 4855 df-rel 4856 df-cnv 4857 df-co 4858 df-dm 4859 df-rn 4860 df-res 4861 df-ima 4862 df-pred 5395 df-ord 5441 df-on 5442 df-lim 5443 df-suc 5444 df-iota 5561 df-fun 5599 df-fn 5600 df-f 5601 df-f1 5602 df-fo 5603 df-f1o 5604 df-fv 5605 df-isom 5606 df-riota 6263 df-ov 6304 df-oprab 6305 df-mpt2 6306 df-om 6703 df-1st 6803 df-2nd 6804 df-wrecs 7032 df-recs 7094 df-rdg 7132 df-1o 7186 df-oadd 7190 df-er 7367 df-en 7574 df-dom 7575 df-sdom 7576 df-fin 7577 df-sup 7958 df-oi 8027 df-card 8374 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-div 10270 df-nn 10610 df-2 10668 df-3 10669 df-4 10670 df-5 10671 df-6 10672 df-7 10673 df-8 10674 df-9 10675 df-10 10676 df-n0 10870 df-z 10938 df-dec 11052 df-uz 11160 df-rp 11303 df-fz 11785 df-fzo 11916 df-seq 12213 df-exp 12272 df-hash 12515 df-cj 13150 df-re 13151 df-im 13152 df-sqrt 13286 df-abs 13287 df-clim 13539 df-sum 13740

This theorem is referenced by: log2ub 23861

W3C validator