log2ublem3 - Metamath Proof Explorer

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

Theorem log2ublem3 23144

Description: Lemma for log2ub 23145. 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 10626	. . . . . . 7
2		0re 9594	. . . . . . . . . . . . 13
3		ltm1 10383	. . . . . . . . . . . . 13
4	2, 3	ax-mp 5	. . . . . . . . . . . 12
5		0z 10876	. . . . . . . . . . . . 13
6		peano2zm 10908	. . . . . . . . . . . . . 14
7	5, 6	ax-mp 5	. . . . . . . . . . . . 13
8		fzn 11706	. . . . . . . . . . . . 13 $/\$
9	5, 7, 8	mp2an 672	. . . . . . . . . . . 12
10	4, 9	mpbi 208	. . . . . . . . . . 11
11	10	sumeq1i 13494	. . . . . . . . . 10
12		sum0 13517	. . . . . . . . . 10
13	11, 12	eqtri 2470	. . . . . . . . 9
14	13	oveq2i 6288	. . . . . . . 8
15		3cn 10611	. . . . . . . . . . 11
16		7nn0 10818	. . . . . . . . . . 11
17		expcl 12158	. . . . . . . . . . 11 $/\$
18	15, 16, 17	mp2an 672	. . . . . . . . . 10
19		5cn 10616	. . . . . . . . . . 11
20		7cn 10620	. . . . . . . . . . 11
21	19, 20	mulcli 9599	. . . . . . . . . 10
22	18, 21	mulcli 9599	. . . . . . . . 9
23	22	mul01i 9768	. . . . . . . 8
24	14, 23	eqtri 2470	. . . . . . 7
25		2cn 10607	. . . . . . . 8
26	25	mul01i 9768	. . . . . . 7
27	1, 24, 26	3brtr4i 4461	. . . . . 6
28		0nn0 10811	. . . . . 6
29		2nn0 10813	. . . . . . . . . 10
30		5nn0 10816	. . . . . . . . . 10
31	29, 30	deccl 10993	. . . . . . . . 9 ;
32	31, 30	deccl 10993	. . . . . . . 8 ;;
33		1nn0 10812	. . . . . . . 8
34	32, 33	deccl 10993	. . . . . . 7 ;;;
35	34, 30	deccl 10993	. . . . . 6 ;;;;
36		eqid 2441	. . . . . 6
37	35	nn0cni 10808	. . . . . . 7 ;;;;
38	37	addid2i 9766	. . . . . 6 ;;;; ;;;;
39		3nn0 10814	. . . . . 6
40	15	addid1i 9765	. . . . . 6
41	37	mulid2i 9597	. . . . . . 7 ;;;; ;;;;
42	26	oveq1i 6287	. . . . . . . . 9
43		0p1e1 10648	. . . . . . . . 9
44	42, 43	eqtri 2470	. . . . . . . 8
45	44	oveq1i 6287	. . . . . . 7 ;;;; ;;;;
46	30, 16	nn0mulcli 10835	. . . . . . . 8
47	16, 29	deccl 10993	. . . . . . . 8 ;
48		9nn0 10820	. . . . . . . 8
49		2p1e3 10660	. . . . . . . . 9
50		8nn0 10819	. . . . . . . . . 10
51		1p1e2 10650	. . . . . . . . . . 11
52		9cn 10624	. . . . . . . . . . . . . 14
53		exp1 12146	. . . . . . . . . . . . . 14
54	52, 53	ax-mp 5	. . . . . . . . . . . . 13
55	54	oveq1i 6287	. . . . . . . . . . . 12
56		9t9e81 11081	. . . . . . . . . . . 12 ;
57	55, 56	eqtri 2470	. . . . . . . . . . 11 ;
58	48, 33, 51, 57	numexpp1 14436	. . . . . . . . . 10 ;
59		8cn 10622	. . . . . . . . . . . . 13
60		9t8e72 11080	. . . . . . . . . . . . 13 ;
61	52, 59, 60	mulcomli 9601	. . . . . . . . . . . 12 ;
62	61	oveq1i 6287	. . . . . . . . . . 11 ;
63	47	nn0cni 10808	. . . . . . . . . . . 12 ;
64	63	addid1i 9765	. . . . . . . . . . 11 ; ;
65	62, 64	eqtri 2470	. . . . . . . . . 10 ;
66	52	mulid2i 9597	. . . . . . . . . . 11
67	48	dec0h 10995	. . . . . . . . . . 11 ;
68	66, 67	eqtri 2470	. . . . . . . . . 10 ;
69	48, 50, 33, 58, 48, 28, 65, 68	decmul1c 11026	. . . . . . . . 9 ;;
70	48, 29, 49, 69	numexpp1 14436	. . . . . . . 8 ;;
71	39, 33	deccl 10993	. . . . . . . 8 ;
72		eqid 2441	. . . . . . . . 9 ; ;
73		eqid 2441	. . . . . . . . 9 ; ;
74		7t5e35 11064	. . . . . . . . . . 11 ;
75	20, 19, 74	mulcomli 9601	. . . . . . . . . 10 ;
76		7p3e10 10682	. . . . . . . . . . . 12
77	20, 15, 76	addcomli 9770	. . . . . . . . . . 11
78		dec10 11009	. . . . . . . . . . 11 ;
79	77, 78	eqtri 2470	. . . . . . . . . 10 ;
80		ax-1cn 9548	. . . . . . . . . . . . 13
81		3p1e4 10662	. . . . . . . . . . . . 13
82	15, 80, 81	addcomli 9770	. . . . . . . . . . . 12
83	82	oveq2i 6288	. . . . . . . . . . 11
84		4nn0 10815	. . . . . . . . . . . 12
85		7t3e21 11062	. . . . . . . . . . . . 13 ;
86	20, 15, 85	mulcomli 9601	. . . . . . . . . . . 12 ;
87		4cn 10614	. . . . . . . . . . . . 13
88		4p1e5 10663	. . . . . . . . . . . . 13
89	87, 80, 88	addcomli 9770	. . . . . . . . . . . 12
90	29, 33, 84, 86, 89	decaddi 11023	. . . . . . . . . . 11 ;
91	83, 90	eqtri 2470	. . . . . . . . . 10 ;
92	75	oveq1i 6287	. . . . . . . . . . 11 ;
93	39, 30	deccl 10993	. . . . . . . . . . . . 13 ;
94	93	nn0cni 10808	. . . . . . . . . . . 12 ;
95	94	addid1i 9765	. . . . . . . . . . 11 ; ;
96	92, 95	eqtri 2470	. . . . . . . . . 10 ;
97	39, 30, 33, 28, 75, 79, 16, 30, 39, 91, 96	decmac 11018	. . . . . . . . 9 ;;
98	33	dec0h 10995	. . . . . . . . . 10 ;
99		3t2e6 10688	. . . . . . . . . . . 12
100	99, 43	oveq12i 6289	. . . . . . . . . . 11
101		6p1e7 10665	. . . . . . . . . . 11
102	100, 101	eqtri 2470	. . . . . . . . . 10
103		5t2e10 10691	. . . . . . . . . . . 12
104	103, 78	eqtri 2470	. . . . . . . . . . 11 ;
105	33, 28, 43, 104	decsuc 11002	. . . . . . . . . 10 ;
106	39, 30, 28, 33, 75, 98, 29, 33, 33, 102, 105	decmac 11018	. . . . . . . . 9 ;
107	16, 29, 39, 33, 72, 73, 46, 33, 16, 97, 106	decma2c 11019	. . . . . . . 8 ; ; ;;;
108		9t3e27 11075	. . . . . . . . . . 11 ;
109	52, 15, 108	mulcomli 9601	. . . . . . . . . 10 ;
110		7p4e11 11031	. . . . . . . . . 10 ;
111	29, 16, 84, 109, 49, 33, 110	decaddci 11024	. . . . . . . . 9 ;
112		9t5e45 11077	. . . . . . . . . 10 ;
113	52, 19, 112	mulcomli 9601	. . . . . . . . 9 ;
114	48, 39, 30, 75, 30, 84, 111, 113	decmul1c 11026	. . . . . . . 8 ;;
115	46, 47, 48, 70, 30, 71, 107, 114	decmul2c 11027	. . . . . . 7 ;;;;
116	41, 45, 115	3eqtr4ri 2481	. . . . . 6 ;;;;
117	27, 28, 35, 28, 36, 38, 39, 40, 116	log2ublem2 23143	. . . . 5 ;;;;
118	48, 84	deccl 10993	. . . . . 6 ;
119	118, 30	deccl 10993	. . . . 5 ;;
120		1m1e0 10605	. . . . 5
121		eqid 2441	. . . . . 6 ;;;; ;;;;
122		eqid 2441	. . . . . 6 ;; ;;
123		6nn0 10817	. . . . . . . . 9
124	29, 123	deccl 10993	. . . . . . . 8 ;
125	124, 84	deccl 10993	. . . . . . 7 ;;
126		5p1e6 10664	. . . . . . 7
127		eqid 2441	. . . . . . . 8 ;;; ;;;
128		eqid 2441	. . . . . . . 8 ; ;
129		eqid 2441	. . . . . . . . 9 ;; ;;
130		eqid 2441	. . . . . . . . . 10 ; ;
131	29, 30, 126, 130	decsuc 11002	. . . . . . . . 9 ; ;
132		9p5e14 11044	. . . . . . . . . 10 ;
133	52, 19, 132	addcomli 9770	. . . . . . . . 9 ;
134	31, 30, 48, 129, 131, 84, 133	decaddci 11024	. . . . . . . 8 ;; ;;
135	32, 33, 48, 84, 127, 128, 134, 89	decadd 11020	. . . . . . 7 ;;; ; ;;;
136	125, 30, 126, 135	decsuc 11002	. . . . . 6 ;;; ; ;;;
137		5p5e10 10677	. . . . . 6
138	34, 30, 118, 30, 121, 122, 136, 137	decaddc2 11022	. . . . 5 ;;;; ;; ;;;;
139	52	sqvali 12221	. . . . . . . . 9
140		3t3e9 10689	. . . . . . . . . 10
141	140	oveq1i 6287	. . . . . . . . 9
142	139, 141	eqtr4i 2473	. . . . . . . 8
143	15, 15, 52	mulassi 9603	. . . . . . . 8
144	142, 143	eqtri 2470	. . . . . . 7
145	144	oveq2i 6288	. . . . . 6
146	15, 52	mulcli 9599	. . . . . . . 8
147	21, 15, 146	mul12i 9773	. . . . . . 7
148	29, 84	deccl 10993	. . . . . . . . 9 ;
149		eqid 2441	. . . . . . . . . 10 ; ;
150	99, 49	oveq12i 6289	. . . . . . . . . . 11
151		6p3e9 10679	. . . . . . . . . . 11
152	150, 151	eqtri 2470	. . . . . . . . . 10
153	87	addid2i 9766	. . . . . . . . . . 11
154	33, 28, 84, 104, 153	decaddi 11023	. . . . . . . . . 10 ;
155	39, 30, 29, 84, 75, 149, 29, 84, 33, 152, 154	decmac 11018	. . . . . . . . 9 ; ;
156	29, 33, 39, 86, 82	decaddi 11023	. . . . . . . . . 10 ;
157	16, 39, 30, 75, 30, 39, 156, 75	decmul1c 11026	. . . . . . . . 9 ;;
158	46, 29, 16, 109, 30, 148, 155, 157	decmul2c 11027	. . . . . . . 8 ;;
159	158	oveq2i 6288	. . . . . . 7 ;;
160	147, 159	eqtri 2470	. . . . . 6 ;;
161		df-3 10596	. . . . . . . 8
162	25	mulid1i 9596	. . . . . . . . 9
163	162	oveq1i 6287	. . . . . . . 8
164	161, 163	eqtr4i 2473	. . . . . . 7
165	164	oveq1i 6287	. . . . . 6 ;; ;;
166	145, 160, 165	3eqtri 2474	. . . . 5 ;;
167	117, 35, 119, 33, 120, 138, 29, 49, 166	log2ublem2 23143	. . . 4 ;;;;
168	125, 123	deccl 10993	. . . . 5 ;;;
169	168, 28	deccl 10993	. . . 4 ;;;;
170	123, 39	deccl 10993	. . . 4 ;
171		2m1e1 10651	. . . 4
172		eqid 2441	. . . . 5 ;;;; ;;;;
173		eqid 2441	. . . . 5 ; ;
174		eqid 2441	. . . . . 6 ;;; ;;;
175		eqid 2441	. . . . . . 7 ;; ;;
176	124, 84, 88, 175	decsuc 11002	. . . . . 6 ;; ;;
177		6p6e12 11030	. . . . . 6 ;
178	125, 123, 123, 174, 176, 29, 177	decaddci 11024	. . . . 5 ;;; ;;;
179	15	addid2i 9766	. . . . 5
180	168, 28, 123, 39, 172, 173, 178, 179	decadd 11020	. . . 4 ;;;; ; ;;;;
181		1p2e3 10661	. . . 4
182	54	oveq2i 6288	. . . . 5
183	19, 20, 52	mulassi 9603	. . . . . 6
184		9t7e63 11079	. . . . . . . 8 ;
185	52, 20, 184	mulcomli 9601	. . . . . . 7 ;
186	185	oveq2i 6288	. . . . . 6 ;
187	183, 186	eqtri 2470	. . . . 5 ;
188		df-5 10598	. . . . . . 7
189		2t2e4 10686	. . . . . . . 8
190	189	oveq1i 6287	. . . . . . 7
191	188, 190	eqtr4i 2473	. . . . . 6
192	191	oveq1i 6287	. . . . 5 ; ;
193	182, 187, 192	3eqtri 2474	. . . 4 ;
194	167, 169, 170, 29, 171, 180, 33, 181, 193	log2ublem2 23143	. . 3 ;;;;
195	124, 30	deccl 10993	. . . . 5 ;;
196	195, 29	deccl 10993	. . . 4 ;;;
197	196, 39	deccl 10993	. . 3 ;;;;
198		3m1e2 10653	. . 3
199		eqid 2441	. . . 4 ;;;; ;;;;
200		5p3e8 10675	. . . . 5
201	19, 15, 200	addcomli 9770	. . . 4
202	196, 39, 30, 199, 201	decaddi 11023	. . 3 ;;;; ;;;;
203	20, 19	mulcli 9599	. . . . 5
204	203	mulid1i 9596	. . . 4
205	19, 20	mulcomi 9600	. . . . 5
206		exp0 12144	. . . . . 6
207	52, 206	ax-mp 5	. . . . 5
208	205, 207	oveq12i 6289	. . . 4
209	15, 25, 99	mulcomli 9601	. . . . . . 7
210	209	oveq1i 6287	. . . . . 6
211		df-7 10600	. . . . . 6
212	210, 211	eqtr4i 2473	. . . . 5
213	212	oveq1i 6287	. . . 4
214	204, 208, 213	3eqtr4i 2480	. . 3
215	194, 197, 30, 39, 198, 202, 28, 179, 214	log2ublem2 23143	. 2 ;;;;
216		eqid 2441	. . 3 ;;;; ;;;;
217		eqid 2441	. . . 4 ;;; ;;;
218		eqid 2441	. . . . 5 ;; ;;
219		00id 9753	. . . . . 6
220	28	dec0h 10995	. . . . . 6 ;
221	219, 220	eqtri 2470	. . . . 5 ;
222		eqid 2441	. . . . . 6 ; ;
223	43, 98	eqtri 2470	. . . . . 6 ;
224	189, 43	oveq12i 6289	. . . . . . 7
225	224, 88	eqtri 2470	. . . . . 6
226		6cn 10618	. . . . . . . 8
227		6t2e12 11056	. . . . . . . 8 ;
228	226, 25, 227	mulcomli 9601	. . . . . . 7 ;
229	33, 29, 49, 228	decsuc 11002	. . . . . 6 ;
230	29, 123, 28, 33, 222, 223, 29, 39, 33, 225, 229	decma2c 11019	. . . . 5 ; ;
231	19, 25, 103	mulcomli 9601	. . . . . . 7
232	231	oveq1i 6287	. . . . . 6
233		dec10p 11008	. . . . . 6 ;
234	232, 233	eqtri 2470	. . . . 5 ;
235	124, 30, 28, 28, 218, 221, 29, 28, 33, 230, 234	decma2c 11019	. . . 4 ;; ;;
236	30	dec0h 10995	. . . . 5 ;
237	190, 88, 236	3eqtri 2474	. . . 4 ;
238	195, 29, 28, 33, 217, 98, 29, 30, 28, 235, 237	decma2c 11019	. . 3 ;;; ;;;
239		8t2e16 11067	. . . 4 ;
240	59, 25, 239	mulcomli 9601	. . 3 ;
241	29, 196, 50, 216, 123, 33, 238, 240	decmul2c 11027	. 2 ;;;; ;;;;
242	215, 241	breqtri 4456	1 ;;;;

Colors of variables: wff setvar class

Syntax hints:

wb 184

wceq 1381

wcel 1802

c0 3767 class class class wbr 4433 (class class class)co 6277

cc 9488

cr 9489

cc0 9490

c1 9491

caddc 9493

cmul 9495

clt 9626

cle 9627

cmin 9805

cdiv 10207

c2 10586

c3 10587

c4 10588

c5 10589

c6 10590

c7 10591

c8 10592

c9 10593

c10 10594

cn0 10796

cz 10865 ;cdc 10979

cfz 11676

cexp 12140

csu 13482

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1603 ax-4 1616 ax-5 1689 ax-6 1732 ax-7 1774 ax-8 1804 ax-9 1806 ax-10 1821 ax-11 1826 ax-12 1838 ax-13 1983 ax-ext 2419 ax-rep 4544 ax-sep 4554 ax-nul 4562 ax-pow 4611 ax-pr 4672 ax-un 6573 ax-inf2 8056 ax-cnex 9546 ax-resscn 9547 ax-1cn 9548 ax-icn 9549 ax-addcl 9550 ax-addrcl 9551 ax-mulcl 9552 ax-mulrcl 9553 ax-mulcom 9554 ax-addass 9555 ax-mulass 9556 ax-distr 9557 ax-i2m1 9558 ax-1ne0 9559 ax-1rid 9560 ax-rnegex 9561 ax-rrecex 9562 ax-cnre 9563 ax-pre-lttri 9564 ax-pre-lttrn 9565 ax-pre-ltadd 9566 ax-pre-mulgt0 9567 ax-pre-sup 9568

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 973 df-3an 974 df-tru 1384 df-fal 1387 df-ex 1598 df-nf 1602 df-sb 1725 df-eu 2270 df-mo 2271 df-clab 2427 df-cleq 2433 df-clel 2436 df-nfc 2591 df-ne 2638 df-nel 2639 df-ral 2796 df-rex 2797 df-reu 2798 df-rmo 2799 df-rab 2800 df-v 3095 df-sbc 3312 df-csb 3418 df-dif 3461 df-un 3463 df-in 3465 df-ss 3472 df-pss 3474 df-nul 3768 df-if 3923 df-pw 3995 df-sn 4011 df-pr 4013 df-tp 4015 df-op 4017 df-uni 4231 df-int 4268 df-iun 4313 df-br 4434 df-opab 4492 df-mpt 4493 df-tr 4527 df-eprel 4777 df-id 4781 df-po 4786 df-so 4787 df-fr 4824 df-se 4825 df-we 4826 df-ord 4867 df-on 4868 df-lim 4869 df-suc 4870 df-xp 4991 df-rel 4992 df-cnv 4993 df-co 4994 df-dm 4995 df-rn 4996 df-res 4997 df-ima 4998 df-iota 5537 df-fun 5576 df-fn 5577 df-f 5578 df-f1 5579 df-fo 5580 df-f1o 5581 df-fv 5582 df-isom 5583 df-riota 6238 df-ov 6280 df-oprab 6281 df-mpt2 6282 df-om 6682 df-1st 6781 df-2nd 6782 df-recs 7040 df-rdg 7074 df-1o 7128 df-oadd 7132 df-er 7309 df-en 7515 df-dom 7516 df-sdom 7517 df-fin 7518 df-sup 7899 df-oi 7933 df-card 8318 df-pnf 9628 df-mnf 9629 df-xr 9630 df-ltxr 9631 df-le 9632 df-sub 9807 df-neg 9808 df-div 10208 df-nn 10538 df-2 10595 df-3 10596 df-4 10597 df-5 10598 df-6 10599 df-7 10600 df-8 10601 df-9 10602 df-10 10603 df-n0 10797 df-z 10866 df-dec 10980 df-uz 11086 df-rp 11225 df-fz 11677 df-fzo 11799 df-seq 12082 df-exp 12141 df-hash 12380 df-cj 12906 df-re 12907 df-im 12908 df-sqrt 13042 df-abs 13043 df-clim 13285 df-sum 13483

This theorem is referenced by: log2ub 23145

W3C validator