log2ublem3 - Metamath Proof Explorer

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

Theorem log2ublem3 22456

Description: Lemma for log2ub 22457. 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 10509	. . . . . . 7
2		0re 9484	. . . . . . . . . . . . 13
3		ltm1 10267	. . . . . . . . . . . . 13
4	2, 3	ax-mp 5	. . . . . . . . . . . 12
5		0z 10755	. . . . . . . . . . . . 13
6		peano2zm 10786	. . . . . . . . . . . . . 14
7	5, 6	ax-mp 5	. . . . . . . . . . . . 13
8		fzn 11564	. . . . . . . . . . . . 13 $/\$
9	5, 7, 8	mp2an 672	. . . . . . . . . . . 12
10	4, 9	mpbi 208	. . . . . . . . . . 11
11	10	sumeq1i 13274	. . . . . . . . . 10
12		sum0 13297	. . . . . . . . . 10
13	11, 12	eqtri 2479	. . . . . . . . 9
14	13	oveq2i 6198	. . . . . . . 8
15		3cn 10494	. . . . . . . . . . 11
16		7nn0 10699	. . . . . . . . . . 11
17		expcl 11981	. . . . . . . . . . 11 $/\$
18	15, 16, 17	mp2an 672	. . . . . . . . . 10
19		5cn 10499	. . . . . . . . . . 11
20		7cn 10503	. . . . . . . . . . 11
21	19, 20	mulcli 9489	. . . . . . . . . 10
22	18, 21	mulcli 9489	. . . . . . . . 9
23	22	mul01i 9657	. . . . . . . 8
24	14, 23	eqtri 2479	. . . . . . 7
25		2cn 10490	. . . . . . . 8
26	25	mul01i 9657	. . . . . . 7
27	1, 24, 26	3brtr4i 4415	. . . . . 6
28		0nn0 10692	. . . . . 6
29		2nn0 10694	. . . . . . . . . 10
30		5nn0 10697	. . . . . . . . . 10
31	29, 30	deccl 10867	. . . . . . . . 9 ;
32	31, 30	deccl 10867	. . . . . . . 8 ;;
33		1nn0 10693	. . . . . . . 8
34	32, 33	deccl 10867	. . . . . . 7 ;;;
35	34, 30	deccl 10867	. . . . . 6 ;;;;
36		eqid 2451	. . . . . 6
37	35	nn0cni 10689	. . . . . . 7 ;;;;
38	37	addid2i 9655	. . . . . 6 ;;;; ;;;;
39		3nn0 10695	. . . . . 6
40	15	addid1i 9654	. . . . . 6
41	37	mulid2i 9487	. . . . . . 7 ;;;; ;;;;
42	26	oveq1i 6197	. . . . . . . . 9
43		0p1e1 10531	. . . . . . . . 9
44	42, 43	eqtri 2479	. . . . . . . 8
45	44	oveq1i 6197	. . . . . . 7 ;;;; ;;;;
46	30, 16	nn0mulcli 10716	. . . . . . . 8
47	16, 29	deccl 10867	. . . . . . . 8 ;
48		9nn0 10701	. . . . . . . 8
49		2p1e3 10543	. . . . . . . . 9
50		8nn0 10700	. . . . . . . . . 10
51		1p1e2 10533	. . . . . . . . . . 11
52		9cn 10507	. . . . . . . . . . . . . 14
53		exp1 11969	. . . . . . . . . . . . . 14
54	52, 53	ax-mp 5	. . . . . . . . . . . . 13
55	54	oveq1i 6197	. . . . . . . . . . . 12
56		9t9e81 10955	. . . . . . . . . . . 12 ;
57	55, 56	eqtri 2479	. . . . . . . . . . 11 ;
58	48, 33, 51, 57	numexpp1 14206	. . . . . . . . . 10 ;
59		8cn 10505	. . . . . . . . . . . . 13
60		9t8e72 10954	. . . . . . . . . . . . 13 ;
61	52, 59, 60	mulcomli 9491	. . . . . . . . . . . 12 ;
62	61	oveq1i 6197	. . . . . . . . . . 11 ;
63	47	nn0cni 10689	. . . . . . . . . . . 12 ;
64	63	addid1i 9654	. . . . . . . . . . 11 ; ;
65	62, 64	eqtri 2479	. . . . . . . . . 10 ;
66	52	mulid2i 9487	. . . . . . . . . . 11
67	48	dec0h 10869	. . . . . . . . . . 11 ;
68	66, 67	eqtri 2479	. . . . . . . . . 10 ;
69	48, 50, 33, 58, 48, 28, 65, 68	decmul1c 10900	. . . . . . . . 9 ;;
70	48, 29, 49, 69	numexpp1 14206	. . . . . . . 8 ;;
71	39, 33	deccl 10867	. . . . . . . 8 ;
72		eqid 2451	. . . . . . . . 9 ; ;
73		eqid 2451	. . . . . . . . 9 ; ;
74		7t5e35 10938	. . . . . . . . . . 11 ;
75	20, 19, 74	mulcomli 9491	. . . . . . . . . 10 ;
76		7p3e10 10565	. . . . . . . . . . . 12
77	20, 15, 76	addcomli 9659	. . . . . . . . . . 11
78		dec10 10883	. . . . . . . . . . 11 ;
79	77, 78	eqtri 2479	. . . . . . . . . 10 ;
80		ax-1cn 9438	. . . . . . . . . . . . 13
81		3p1e4 10545	. . . . . . . . . . . . 13
82	15, 80, 81	addcomli 9659	. . . . . . . . . . . 12
83	82	oveq2i 6198	. . . . . . . . . . 11
84		4nn0 10696	. . . . . . . . . . . 12
85		7t3e21 10936	. . . . . . . . . . . . 13 ;
86	20, 15, 85	mulcomli 9491	. . . . . . . . . . . 12 ;
87		4cn 10497	. . . . . . . . . . . . 13
88		4p1e5 10546	. . . . . . . . . . . . 13
89	87, 80, 88	addcomli 9659	. . . . . . . . . . . 12
90	29, 33, 84, 86, 89	decaddi 10897	. . . . . . . . . . 11 ;
91	83, 90	eqtri 2479	. . . . . . . . . 10 ;
92	75	oveq1i 6197	. . . . . . . . . . 11 ;
93	39, 30	deccl 10867	. . . . . . . . . . . . 13 ;
94	93	nn0cni 10689	. . . . . . . . . . . 12 ;
95	94	addid1i 9654	. . . . . . . . . . 11 ; ;
96	92, 95	eqtri 2479	. . . . . . . . . 10 ;
97	39, 30, 33, 28, 75, 79, 16, 30, 39, 91, 96	decmac 10892	. . . . . . . . 9 ;;
98	33	dec0h 10869	. . . . . . . . . 10 ;
99		3t2e6 10571	. . . . . . . . . . . 12
100	99, 43	oveq12i 6199	. . . . . . . . . . 11
101		6p1e7 10548	. . . . . . . . . . 11
102	100, 101	eqtri 2479	. . . . . . . . . 10
103		5t2e10 10574	. . . . . . . . . . . 12
104	103, 78	eqtri 2479	. . . . . . . . . . 11 ;
105	33, 28, 43, 104	decsuc 10876	. . . . . . . . . 10 ;
106	39, 30, 28, 33, 75, 98, 29, 33, 33, 102, 105	decmac 10892	. . . . . . . . 9 ;
107	16, 29, 39, 33, 72, 73, 46, 33, 16, 97, 106	decma2c 10893	. . . . . . . 8 ; ; ;;;
108		9t3e27 10949	. . . . . . . . . . 11 ;
109	52, 15, 108	mulcomli 9491	. . . . . . . . . 10 ;
110		7p4e11 10905	. . . . . . . . . 10 ;
111	29, 16, 84, 109, 49, 33, 110	decaddci 10898	. . . . . . . . 9 ;
112		9t5e45 10951	. . . . . . . . . 10 ;
113	52, 19, 112	mulcomli 9491	. . . . . . . . 9 ;
114	48, 39, 30, 75, 30, 84, 111, 113	decmul1c 10900	. . . . . . . 8 ;;
115	46, 47, 48, 70, 30, 71, 107, 114	decmul2c 10901	. . . . . . 7 ;;;;
116	41, 45, 115	3eqtr4ri 2490	. . . . . 6 ;;;;
117	27, 28, 35, 28, 36, 38, 39, 40, 116	log2ublem2 22455	. . . . 5 ;;;;
118	48, 84	deccl 10867	. . . . . 6 ;
119	118, 30	deccl 10867	. . . . 5 ;;
120		1m1e0 10488	. . . . 5
121		eqid 2451	. . . . . 6 ;;;; ;;;;
122		eqid 2451	. . . . . 6 ;; ;;
123		6nn0 10698	. . . . . . . . 9
124	29, 123	deccl 10867	. . . . . . . 8 ;
125	124, 84	deccl 10867	. . . . . . 7 ;;
126		5p1e6 10547	. . . . . . 7
127		eqid 2451	. . . . . . . 8 ;;; ;;;
128		eqid 2451	. . . . . . . 8 ; ;
129		eqid 2451	. . . . . . . . 9 ;; ;;
130		eqid 2451	. . . . . . . . . 10 ; ;
131	29, 30, 126, 130	decsuc 10876	. . . . . . . . 9 ; ;
132		9p5e14 10918	. . . . . . . . . 10 ;
133	52, 19, 132	addcomli 9659	. . . . . . . . 9 ;
134	31, 30, 48, 129, 131, 84, 133	decaddci 10898	. . . . . . . 8 ;; ;;
135	32, 33, 48, 84, 127, 128, 134, 89	decadd 10894	. . . . . . 7 ;;; ; ;;;
136	125, 30, 126, 135	decsuc 10876	. . . . . 6 ;;; ; ;;;
137		5p5e10 10560	. . . . . 6
138	34, 30, 118, 30, 121, 122, 136, 137	decaddc2 10896	. . . . 5 ;;;; ;; ;;;;
139	52	sqvali 12043	. . . . . . . . 9
140		3t3e9 10572	. . . . . . . . . 10
141	140	oveq1i 6197	. . . . . . . . 9
142	139, 141	eqtr4i 2482	. . . . . . . 8
143	15, 15, 52	mulassi 9493	. . . . . . . 8
144	142, 143	eqtri 2479	. . . . . . 7
145	144	oveq2i 6198	. . . . . 6
146	15, 52	mulcli 9489	. . . . . . . 8
147	21, 15, 146	mul12i 9662	. . . . . . 7
148	29, 84	deccl 10867	. . . . . . . . 9 ;
149		eqid 2451	. . . . . . . . . 10 ; ;
150	99, 49	oveq12i 6199	. . . . . . . . . . 11
151		6p3e9 10562	. . . . . . . . . . 11
152	150, 151	eqtri 2479	. . . . . . . . . 10
153	87	addid2i 9655	. . . . . . . . . . 11
154	33, 28, 84, 104, 153	decaddi 10897	. . . . . . . . . 10 ;
155	39, 30, 29, 84, 75, 149, 29, 84, 33, 152, 154	decmac 10892	. . . . . . . . 9 ; ;
156	29, 33, 39, 86, 82	decaddi 10897	. . . . . . . . . 10 ;
157	16, 39, 30, 75, 30, 39, 156, 75	decmul1c 10900	. . . . . . . . 9 ;;
158	46, 29, 16, 109, 30, 148, 155, 157	decmul2c 10901	. . . . . . . 8 ;;
159	158	oveq2i 6198	. . . . . . 7 ;;
160	147, 159	eqtri 2479	. . . . . 6 ;;
161		df-3 10479	. . . . . . . 8
162	25	mulid1i 9486	. . . . . . . . 9
163	162	oveq1i 6197	. . . . . . . 8
164	161, 163	eqtr4i 2482	. . . . . . 7
165	164	oveq1i 6197	. . . . . 6 ;; ;;
166	145, 160, 165	3eqtri 2483	. . . . 5 ;;
167	117, 35, 119, 33, 120, 138, 29, 49, 166	log2ublem2 22455	. . . 4 ;;;;
168	125, 123	deccl 10867	. . . . 5 ;;;
169	168, 28	deccl 10867	. . . 4 ;;;;
170	123, 39	deccl 10867	. . . 4 ;
171		2m1e1 10534	. . . 4
172		eqid 2451	. . . . 5 ;;;; ;;;;
173		eqid 2451	. . . . 5 ; ;
174		eqid 2451	. . . . . 6 ;;; ;;;
175		eqid 2451	. . . . . . 7 ;; ;;
176	124, 84, 88, 175	decsuc 10876	. . . . . 6 ;; ;;
177		6p6e12 10904	. . . . . 6 ;
178	125, 123, 123, 174, 176, 29, 177	decaddci 10898	. . . . 5 ;;; ;;;
179	15	addid2i 9655	. . . . 5
180	168, 28, 123, 39, 172, 173, 178, 179	decadd 10894	. . . 4 ;;;; ; ;;;;
181		1p2e3 10544	. . . 4
182	54	oveq2i 6198	. . . . 5
183	19, 20, 52	mulassi 9493	. . . . . 6
184		9t7e63 10953	. . . . . . . 8 ;
185	52, 20, 184	mulcomli 9491	. . . . . . 7 ;
186	185	oveq2i 6198	. . . . . 6 ;
187	183, 186	eqtri 2479	. . . . 5 ;
188		df-5 10481	. . . . . . 7
189		2t2e4 10569	. . . . . . . 8
190	189	oveq1i 6197	. . . . . . 7
191	188, 190	eqtr4i 2482	. . . . . 6
192	191	oveq1i 6197	. . . . 5 ; ;
193	182, 187, 192	3eqtri 2483	. . . 4 ;
194	167, 169, 170, 29, 171, 180, 33, 181, 193	log2ublem2 22455	. . 3 ;;;;
195	124, 30	deccl 10867	. . . . 5 ;;
196	195, 29	deccl 10867	. . . 4 ;;;
197	196, 39	deccl 10867	. . 3 ;;;;
198		3m1e2 10536	. . 3
199		eqid 2451	. . . 4 ;;;; ;;;;
200		5p3e8 10558	. . . . 5
201	19, 15, 200	addcomli 9659	. . . 4
202	196, 39, 30, 199, 201	decaddi 10897	. . 3 ;;;; ;;;;
203	20, 19	mulcli 9489	. . . . 5
204	203	mulid1i 9486	. . . 4
205	19, 20	mulcomi 9490	. . . . 5
206		exp0 11967	. . . . . 6
207	52, 206	ax-mp 5	. . . . 5
208	205, 207	oveq12i 6199	. . . 4
209	15, 25, 99	mulcomli 9491	. . . . . . 7
210	209	oveq1i 6197	. . . . . 6
211		df-7 10483	. . . . . 6
212	210, 211	eqtr4i 2482	. . . . 5
213	212	oveq1i 6197	. . . 4
214	204, 208, 213	3eqtr4i 2489	. . 3
215	194, 197, 30, 39, 198, 202, 28, 179, 214	log2ublem2 22455	. 2 ;;;;
216		eqid 2451	. . 3 ;;;; ;;;;
217		eqid 2451	. . . 4 ;;; ;;;
218		eqid 2451	. . . . 5 ;; ;;
219		00id 9642	. . . . . 6
220	28	dec0h 10869	. . . . . 6 ;
221	219, 220	eqtri 2479	. . . . 5 ;
222		eqid 2451	. . . . . 6 ; ;
223	43, 98	eqtri 2479	. . . . . 6 ;
224	189, 43	oveq12i 6199	. . . . . . 7
225	224, 88	eqtri 2479	. . . . . 6
226		6cn 10501	. . . . . . . 8
227		6t2e12 10930	. . . . . . . 8 ;
228	226, 25, 227	mulcomli 9491	. . . . . . 7 ;
229	33, 29, 49, 228	decsuc 10876	. . . . . 6 ;
230	29, 123, 28, 33, 222, 223, 29, 39, 33, 225, 229	decma2c 10893	. . . . 5 ; ;
231	19, 25, 103	mulcomli 9491	. . . . . . 7
232	231	oveq1i 6197	. . . . . 6
233		dec10p 10882	. . . . . 6 ;
234	232, 233	eqtri 2479	. . . . 5 ;
235	124, 30, 28, 28, 218, 221, 29, 28, 33, 230, 234	decma2c 10893	. . . 4 ;; ;;
236	30	dec0h 10869	. . . . 5 ;
237	190, 88, 236	3eqtri 2483	. . . 4 ;
238	195, 29, 28, 33, 217, 98, 29, 30, 28, 235, 237	decma2c 10893	. . 3 ;;; ;;;
239		8t2e16 10941	. . . 4 ;
240	59, 25, 239	mulcomli 9491	. . 3 ;
241	29, 196, 50, 216, 123, 33, 238, 240	decmul2c 10901	. 2 ;;;; ;;;;
242	215, 241	breqtri 4410	1 ;;;;

Colors of variables: wff setvar class

Syntax hints:

wb 184

wceq 1370

wcel 1758

c0 3732 class class class wbr 4387 (class class class)co 6187

cc 9378

cr 9379

cc0 9380

c1 9381

caddc 9383

cmul 9385

clt 9516

cle 9517

cmin 9693

cdiv 10091

c2 10469

c3 10470

c4 10471

c5 10472

c6 10473

c7 10474

c8 10475

c9 10476

c10 10477

cn0 10677

cz 10744 ;cdc 10853

cfz 11535

cexp 11963

csu 13262

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-rep 4498 ax-sep 4508 ax-nul 4516 ax-pow 4565 ax-pr 4626 ax-un 6469 ax-inf2 7945 ax-cnex 9436 ax-resscn 9437 ax-1cn 9438 ax-icn 9439 ax-addcl 9440 ax-addrcl 9441 ax-mulcl 9442 ax-mulrcl 9443 ax-mulcom 9444 ax-addass 9445 ax-mulass 9446 ax-distr 9447 ax-i2m1 9448 ax-1ne0 9449 ax-1rid 9450 ax-rnegex 9451 ax-rrecex 9452 ax-cnre 9453 ax-pre-lttri 9454 ax-pre-lttrn 9455 ax-pre-ltadd 9456 ax-pre-mulgt0 9457 ax-pre-sup 9458

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-fal 1376 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2599 df-ne 2644 df-nel 2645 df-ral 2798 df-rex 2799 df-reu 2800 df-rmo 2801 df-rab 2802 df-v 3067 df-sbc 3282 df-csb 3384 df-dif 3426 df-un 3428 df-in 3430 df-ss 3437 df-pss 3439 df-nul 3733 df-if 3887 df-pw 3957 df-sn 3973 df-pr 3975 df-tp 3977 df-op 3979 df-uni 4187 df-int 4224 df-iun 4268 df-br 4388 df-opab 4446 df-mpt 4447 df-tr 4481 df-eprel 4727 df-id 4731 df-po 4736 df-so 4737 df-fr 4774 df-se 4775 df-we 4776 df-ord 4817 df-on 4818 df-lim 4819 df-suc 4820 df-xp 4941 df-rel 4942 df-cnv 4943 df-co 4944 df-dm 4945 df-rn 4946 df-res 4947 df-ima 4948 df-iota 5476 df-fun 5515 df-fn 5516 df-f 5517 df-f1 5518 df-fo 5519 df-f1o 5520 df-fv 5521 df-isom 5522 df-riota 6148 df-ov 6190 df-oprab 6191 df-mpt2 6192 df-om 6574 df-1st 6674 df-2nd 6675 df-recs 6929 df-rdg 6963 df-1o 7017 df-oadd 7021 df-er 7198 df-en 7408 df-dom 7409 df-sdom 7410 df-fin 7411 df-sup 7789 df-oi 7822 df-card 8207 df-pnf 9518 df-mnf 9519 df-xr 9520 df-ltxr 9521 df-le 9522 df-sub 9695 df-neg 9696 df-div 10092 df-nn 10421 df-2 10478 df-3 10479 df-4 10480 df-5 10481 df-6 10482 df-7 10483 df-8 10484 df-9 10485 df-10 10486 df-n0 10678 df-z 10745 df-dec 10854 df-uz 10960 df-rp 11090 df-fz 11536 df-fzo 11647 df-seq 11905 df-exp 11964 df-hash 12202 df-cj 12687 df-re 12688 df-im 12689 df-sqr 12823 df-abs 12824 df-clim 13065 df-sum 13263

This theorem is referenced by: log2ub 22457

W3C validator