log2ublem3 - Metamath Proof Explorer

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

Theorem log2ublem3 23404

Description: Lemma for log2ub 23405. 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 10646	. . . . . . 7
2		0re 9613	. . . . . . . . . . . . 13
3		ltm1 10403	. . . . . . . . . . . . 13
4	2, 3	ax-mp 5	. . . . . . . . . . . 12
5		0z 10896	. . . . . . . . . . . . 13
6		peano2zm 10928	. . . . . . . . . . . . . 14
7	5, 6	ax-mp 5	. . . . . . . . . . . . 13
8		fzn 11727	. . . . . . . . . . . . 13 $/\$
9	5, 7, 8	mp2an 672	. . . . . . . . . . . 12
10	4, 9	mpbi 208	. . . . . . . . . . 11
11	10	sumeq1i 13531	. . . . . . . . . 10
12		sum0 13554	. . . . . . . . . 10
13	11, 12	eqtri 2486	. . . . . . . . 9
14	13	oveq2i 6307	. . . . . . . 8
15		3cn 10631	. . . . . . . . . . 11
16		7nn0 10838	. . . . . . . . . . 11
17		expcl 12186	. . . . . . . . . . 11 $/\$
18	15, 16, 17	mp2an 672	. . . . . . . . . 10
19		5cn 10636	. . . . . . . . . . 11
20		7cn 10640	. . . . . . . . . . 11
21	19, 20	mulcli 9618	. . . . . . . . . 10
22	18, 21	mulcli 9618	. . . . . . . . 9
23	22	mul01i 9787	. . . . . . . 8
24	14, 23	eqtri 2486	. . . . . . 7
25		2cn 10627	. . . . . . . 8
26	25	mul01i 9787	. . . . . . 7
27	1, 24, 26	3brtr4i 4484	. . . . . 6
28		0nn0 10831	. . . . . 6
29		2nn0 10833	. . . . . . . . . 10
30		5nn0 10836	. . . . . . . . . 10
31	29, 30	deccl 11014	. . . . . . . . 9 ;
32	31, 30	deccl 11014	. . . . . . . 8 ;;
33		1nn0 10832	. . . . . . . 8
34	32, 33	deccl 11014	. . . . . . 7 ;;;
35	34, 30	deccl 11014	. . . . . 6 ;;;;
36		eqid 2457	. . . . . 6
37	35	nn0cni 10828	. . . . . . 7 ;;;;
38	37	addid2i 9785	. . . . . 6 ;;;; ;;;;
39		3nn0 10834	. . . . . 6
40	15	addid1i 9784	. . . . . 6
41	37	mulid2i 9616	. . . . . . 7 ;;;; ;;;;
42	26	oveq1i 6306	. . . . . . . . 9
43		0p1e1 10668	. . . . . . . . 9
44	42, 43	eqtri 2486	. . . . . . . 8
45	44	oveq1i 6306	. . . . . . 7 ;;;; ;;;;
46	30, 16	nn0mulcli 10855	. . . . . . . 8
47	16, 29	deccl 11014	. . . . . . . 8 ;
48		9nn0 10840	. . . . . . . 8
49		2p1e3 10680	. . . . . . . . 9
50		8nn0 10839	. . . . . . . . . 10
51		1p1e2 10670	. . . . . . . . . . 11
52		9cn 10644	. . . . . . . . . . . . . 14
53		exp1 12174	. . . . . . . . . . . . . 14
54	52, 53	ax-mp 5	. . . . . . . . . . . . 13
55	54	oveq1i 6306	. . . . . . . . . . . 12
56		9t9e81 11102	. . . . . . . . . . . 12 ;
57	55, 56	eqtri 2486	. . . . . . . . . . 11 ;
58	48, 33, 51, 57	numexpp1 14575	. . . . . . . . . 10 ;
59		8cn 10642	. . . . . . . . . . . . 13
60		9t8e72 11101	. . . . . . . . . . . . 13 ;
61	52, 59, 60	mulcomli 9620	. . . . . . . . . . . 12 ;
62	61	oveq1i 6306	. . . . . . . . . . 11 ;
63	47	nn0cni 10828	. . . . . . . . . . . 12 ;
64	63	addid1i 9784	. . . . . . . . . . 11 ; ;
65	62, 64	eqtri 2486	. . . . . . . . . 10 ;
66	52	mulid2i 9616	. . . . . . . . . . 11
67	48	dec0h 11016	. . . . . . . . . . 11 ;
68	66, 67	eqtri 2486	. . . . . . . . . 10 ;
69	48, 50, 33, 58, 48, 28, 65, 68	decmul1c 11047	. . . . . . . . 9 ;;
70	48, 29, 49, 69	numexpp1 14575	. . . . . . . 8 ;;
71	39, 33	deccl 11014	. . . . . . . 8 ;
72		eqid 2457	. . . . . . . . 9 ; ;
73		eqid 2457	. . . . . . . . 9 ; ;
74		7t5e35 11085	. . . . . . . . . . 11 ;
75	20, 19, 74	mulcomli 9620	. . . . . . . . . 10 ;
76		7p3e10 10702	. . . . . . . . . . . 12
77	20, 15, 76	addcomli 9789	. . . . . . . . . . 11
78		dec10 11030	. . . . . . . . . . 11 ;
79	77, 78	eqtri 2486	. . . . . . . . . 10 ;
80		ax-1cn 9567	. . . . . . . . . . . . 13
81		3p1e4 10682	. . . . . . . . . . . . 13
82	15, 80, 81	addcomli 9789	. . . . . . . . . . . 12
83	82	oveq2i 6307	. . . . . . . . . . 11
84		4nn0 10835	. . . . . . . . . . . 12
85		7t3e21 11083	. . . . . . . . . . . . 13 ;
86	20, 15, 85	mulcomli 9620	. . . . . . . . . . . 12 ;
87		4cn 10634	. . . . . . . . . . . . 13
88		4p1e5 10683	. . . . . . . . . . . . 13
89	87, 80, 88	addcomli 9789	. . . . . . . . . . . 12
90	29, 33, 84, 86, 89	decaddi 11044	. . . . . . . . . . 11 ;
91	83, 90	eqtri 2486	. . . . . . . . . 10 ;
92	75	oveq1i 6306	. . . . . . . . . . 11 ;
93	39, 30	deccl 11014	. . . . . . . . . . . . 13 ;
94	93	nn0cni 10828	. . . . . . . . . . . 12 ;
95	94	addid1i 9784	. . . . . . . . . . 11 ; ;
96	92, 95	eqtri 2486	. . . . . . . . . 10 ;
97	39, 30, 33, 28, 75, 79, 16, 30, 39, 91, 96	decmac 11039	. . . . . . . . 9 ;;
98	33	dec0h 11016	. . . . . . . . . 10 ;
99		3t2e6 10708	. . . . . . . . . . . 12
100	99, 43	oveq12i 6308	. . . . . . . . . . 11
101		6p1e7 10685	. . . . . . . . . . 11
102	100, 101	eqtri 2486	. . . . . . . . . 10
103		5t2e10 10711	. . . . . . . . . . . 12
104	103, 78	eqtri 2486	. . . . . . . . . . 11 ;
105	33, 28, 43, 104	decsuc 11023	. . . . . . . . . 10 ;
106	39, 30, 28, 33, 75, 98, 29, 33, 33, 102, 105	decmac 11039	. . . . . . . . 9 ;
107	16, 29, 39, 33, 72, 73, 46, 33, 16, 97, 106	decma2c 11040	. . . . . . . 8 ; ; ;;;
108		9t3e27 11096	. . . . . . . . . . 11 ;
109	52, 15, 108	mulcomli 9620	. . . . . . . . . 10 ;
110		7p4e11 11052	. . . . . . . . . 10 ;
111	29, 16, 84, 109, 49, 33, 110	decaddci 11045	. . . . . . . . 9 ;
112		9t5e45 11098	. . . . . . . . . 10 ;
113	52, 19, 112	mulcomli 9620	. . . . . . . . 9 ;
114	48, 39, 30, 75, 30, 84, 111, 113	decmul1c 11047	. . . . . . . 8 ;;
115	46, 47, 48, 70, 30, 71, 107, 114	decmul2c 11048	. . . . . . 7 ;;;;
116	41, 45, 115	3eqtr4ri 2497	. . . . . 6 ;;;;
117	27, 28, 35, 28, 36, 38, 39, 40, 116	log2ublem2 23403	. . . . 5 ;;;;
118	48, 84	deccl 11014	. . . . . 6 ;
119	118, 30	deccl 11014	. . . . 5 ;;
120		1m1e0 10625	. . . . 5
121		eqid 2457	. . . . . 6 ;;;; ;;;;
122		eqid 2457	. . . . . 6 ;; ;;
123		6nn0 10837	. . . . . . . . 9
124	29, 123	deccl 11014	. . . . . . . 8 ;
125	124, 84	deccl 11014	. . . . . . 7 ;;
126		5p1e6 10684	. . . . . . 7
127		eqid 2457	. . . . . . . 8 ;;; ;;;
128		eqid 2457	. . . . . . . 8 ; ;
129		eqid 2457	. . . . . . . . 9 ;; ;;
130		eqid 2457	. . . . . . . . . 10 ; ;
131	29, 30, 126, 130	decsuc 11023	. . . . . . . . 9 ; ;
132		9p5e14 11065	. . . . . . . . . 10 ;
133	52, 19, 132	addcomli 9789	. . . . . . . . 9 ;
134	31, 30, 48, 129, 131, 84, 133	decaddci 11045	. . . . . . . 8 ;; ;;
135	32, 33, 48, 84, 127, 128, 134, 89	decadd 11041	. . . . . . 7 ;;; ; ;;;
136	125, 30, 126, 135	decsuc 11023	. . . . . 6 ;;; ; ;;;
137		5p5e10 10697	. . . . . 6
138	34, 30, 118, 30, 121, 122, 136, 137	decaddc2 11043	. . . . 5 ;;;; ;; ;;;;
139	52	sqvali 12249	. . . . . . . . 9
140		3t3e9 10709	. . . . . . . . . 10
141	140	oveq1i 6306	. . . . . . . . 9
142	139, 141	eqtr4i 2489	. . . . . . . 8
143	15, 15, 52	mulassi 9622	. . . . . . . 8
144	142, 143	eqtri 2486	. . . . . . 7
145	144	oveq2i 6307	. . . . . 6
146	15, 52	mulcli 9618	. . . . . . . 8
147	21, 15, 146	mul12i 9792	. . . . . . 7
148	29, 84	deccl 11014	. . . . . . . . 9 ;
149		eqid 2457	. . . . . . . . . 10 ; ;
150	99, 49	oveq12i 6308	. . . . . . . . . . 11
151		6p3e9 10699	. . . . . . . . . . 11
152	150, 151	eqtri 2486	. . . . . . . . . 10
153	87	addid2i 9785	. . . . . . . . . . 11
154	33, 28, 84, 104, 153	decaddi 11044	. . . . . . . . . 10 ;
155	39, 30, 29, 84, 75, 149, 29, 84, 33, 152, 154	decmac 11039	. . . . . . . . 9 ; ;
156	29, 33, 39, 86, 82	decaddi 11044	. . . . . . . . . 10 ;
157	16, 39, 30, 75, 30, 39, 156, 75	decmul1c 11047	. . . . . . . . 9 ;;
158	46, 29, 16, 109, 30, 148, 155, 157	decmul2c 11048	. . . . . . . 8 ;;
159	158	oveq2i 6307	. . . . . . 7 ;;
160	147, 159	eqtri 2486	. . . . . 6 ;;
161		df-3 10616	. . . . . . . 8
162	25	mulid1i 9615	. . . . . . . . 9
163	162	oveq1i 6306	. . . . . . . 8
164	161, 163	eqtr4i 2489	. . . . . . 7
165	164	oveq1i 6306	. . . . . 6 ;; ;;
166	145, 160, 165	3eqtri 2490	. . . . 5 ;;
167	117, 35, 119, 33, 120, 138, 29, 49, 166	log2ublem2 23403	. . . 4 ;;;;
168	125, 123	deccl 11014	. . . . 5 ;;;
169	168, 28	deccl 11014	. . . 4 ;;;;
170	123, 39	deccl 11014	. . . 4 ;
171		2m1e1 10671	. . . 4
172		eqid 2457	. . . . 5 ;;;; ;;;;
173		eqid 2457	. . . . 5 ; ;
174		eqid 2457	. . . . . 6 ;;; ;;;
175		eqid 2457	. . . . . . 7 ;; ;;
176	124, 84, 88, 175	decsuc 11023	. . . . . 6 ;; ;;
177		6p6e12 11051	. . . . . 6 ;
178	125, 123, 123, 174, 176, 29, 177	decaddci 11045	. . . . 5 ;;; ;;;
179	15	addid2i 9785	. . . . 5
180	168, 28, 123, 39, 172, 173, 178, 179	decadd 11041	. . . 4 ;;;; ; ;;;;
181		1p2e3 10681	. . . 4
182	54	oveq2i 6307	. . . . 5
183	19, 20, 52	mulassi 9622	. . . . . 6
184		9t7e63 11100	. . . . . . . 8 ;
185	52, 20, 184	mulcomli 9620	. . . . . . 7 ;
186	185	oveq2i 6307	. . . . . 6 ;
187	183, 186	eqtri 2486	. . . . 5 ;
188		df-5 10618	. . . . . . 7
189		2t2e4 10706	. . . . . . . 8
190	189	oveq1i 6306	. . . . . . 7
191	188, 190	eqtr4i 2489	. . . . . 6
192	191	oveq1i 6306	. . . . 5 ; ;
193	182, 187, 192	3eqtri 2490	. . . 4 ;
194	167, 169, 170, 29, 171, 180, 33, 181, 193	log2ublem2 23403	. . 3 ;;;;
195	124, 30	deccl 11014	. . . . 5 ;;
196	195, 29	deccl 11014	. . . 4 ;;;
197	196, 39	deccl 11014	. . 3 ;;;;
198		3m1e2 10673	. . 3
199		eqid 2457	. . . 4 ;;;; ;;;;
200		5p3e8 10695	. . . . 5
201	19, 15, 200	addcomli 9789	. . . 4
202	196, 39, 30, 199, 201	decaddi 11044	. . 3 ;;;; ;;;;
203	20, 19	mulcli 9618	. . . . 5
204	203	mulid1i 9615	. . . 4
205	19, 20	mulcomi 9619	. . . . 5
206		exp0 12172	. . . . . 6
207	52, 206	ax-mp 5	. . . . 5
208	205, 207	oveq12i 6308	. . . 4
209	15, 25, 99	mulcomli 9620	. . . . . . 7
210	209	oveq1i 6306	. . . . . 6
211		df-7 10620	. . . . . 6
212	210, 211	eqtr4i 2489	. . . . 5
213	212	oveq1i 6306	. . . 4
214	204, 208, 213	3eqtr4i 2496	. . 3
215	194, 197, 30, 39, 198, 202, 28, 179, 214	log2ublem2 23403	. 2 ;;;;
216		eqid 2457	. . 3 ;;;; ;;;;
217		eqid 2457	. . . 4 ;;; ;;;
218		eqid 2457	. . . . 5 ;; ;;
219		00id 9772	. . . . . 6
220	28	dec0h 11016	. . . . . 6 ;
221	219, 220	eqtri 2486	. . . . 5 ;
222		eqid 2457	. . . . . 6 ; ;
223	43, 98	eqtri 2486	. . . . . 6 ;
224	189, 43	oveq12i 6308	. . . . . . 7
225	224, 88	eqtri 2486	. . . . . 6
226		6cn 10638	. . . . . . . 8
227		6t2e12 11077	. . . . . . . 8 ;
228	226, 25, 227	mulcomli 9620	. . . . . . 7 ;
229	33, 29, 49, 228	decsuc 11023	. . . . . 6 ;
230	29, 123, 28, 33, 222, 223, 29, 39, 33, 225, 229	decma2c 11040	. . . . 5 ; ;
231	19, 25, 103	mulcomli 9620	. . . . . . 7
232	231	oveq1i 6306	. . . . . 6
233		dec10p 11029	. . . . . 6 ;
234	232, 233	eqtri 2486	. . . . 5 ;
235	124, 30, 28, 28, 218, 221, 29, 28, 33, 230, 234	decma2c 11040	. . . 4 ;; ;;
236	30	dec0h 11016	. . . . 5 ;
237	190, 88, 236	3eqtri 2490	. . . 4 ;
238	195, 29, 28, 33, 217, 98, 29, 30, 28, 235, 237	decma2c 11040	. . 3 ;;; ;;;
239		8t2e16 11088	. . . 4 ;
240	59, 25, 239	mulcomli 9620	. . 3 ;
241	29, 196, 50, 216, 123, 33, 238, 240	decmul2c 11048	. 2 ;;;; ;;;;
242	215, 241	breqtri 4479	1 ;;;;

Colors of variables: wff setvar class

Syntax hints:

wb 184

wceq 1395

wcel 1819

c0 3793 class class class wbr 4456 (class class class)co 6296

cc 9507

cr 9508

cc0 9509

c1 9510

caddc 9512

cmul 9514

clt 9645

cle 9646

cmin 9824

cdiv 10227

c2 10606

c3 10607

c4 10608

c5 10609

c6 10610

c7 10611

c8 10612

c9 10613

c10 10614

cn0 10816

cz 10885 ;cdc 11000

cfz 11697

cexp 12168

csu 13519

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-inf2 8075 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-fal 1401 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-se 4848 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-isom 5603 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6700 df-1st 6799 df-2nd 6800 df-recs 7060 df-rdg 7094 df-1o 7148 df-oadd 7152 df-er 7329 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-sup 7919 df-oi 7953 df-card 8337 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-2 10615 df-3 10616 df-4 10617 df-5 10618 df-6 10619 df-7 10620 df-8 10621 df-9 10622 df-10 10623 df-n0 10817 df-z 10886 df-dec 11001 df-uz 11107 df-rp 11246 df-fz 11698 df-fzo 11821 df-seq 12110 df-exp 12169 df-hash 12408 df-cj 12943 df-re 12944 df-im 12945 df-sqrt 13079 df-abs 13080 df-clim 13322 df-sum 13520

This theorem is referenced by: log2ub 23405

W3C validator