log2ublem3 - Metamath Proof Explorer

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

Theorem log2ublem3 23867

Description: Lemma for log2ub 23868. 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 10696	. . . . . . 7
2		0re 9640	. . . . . . . . . . . . 13
3		ltm1 10442	. . . . . . . . . . . . 13
4	2, 3	ax-mp 5	. . . . . . . . . . . 12
5		0z 10945	. . . . . . . . . . . . 13
6		peano2zm 10977	. . . . . . . . . . . . . 14
7	5, 6	ax-mp 5	. . . . . . . . . . . . 13
8		fzn 11812	. . . . . . . . . . . . 13 $/\$
9	5, 7, 8	mp2an 677	. . . . . . . . . . . 12
10	4, 9	mpbi 212	. . . . . . . . . . 11
11	10	sumeq1i 13757	. . . . . . . . . 10
12		sum0 13780	. . . . . . . . . 10
13	11, 12	eqtri 2472	. . . . . . . . 9
14	13	oveq2i 6299	. . . . . . . 8
15		3cn 10681	. . . . . . . . . . 11
16		7nn0 10888	. . . . . . . . . . 11
17		expcl 12287	. . . . . . . . . . 11 $/\$
18	15, 16, 17	mp2an 677	. . . . . . . . . 10
19		5cn 10686	. . . . . . . . . . 11
20		7cn 10690	. . . . . . . . . . 11
21	19, 20	mulcli 9645	. . . . . . . . . 10
22	18, 21	mulcli 9645	. . . . . . . . 9
23	22	mul01i 9820	. . . . . . . 8
24	14, 23	eqtri 2472	. . . . . . 7
25		2cn 10677	. . . . . . . 8
26	25	mul01i 9820	. . . . . . 7
27	1, 24, 26	3brtr4i 4430	. . . . . 6
28		0nn0 10881	. . . . . 6
29		2nn0 10883	. . . . . . . . . 10
30		5nn0 10886	. . . . . . . . . 10
31	29, 30	deccl 11062	. . . . . . . . 9 ;
32	31, 30	deccl 11062	. . . . . . . 8 ;;
33		1nn0 10882	. . . . . . . 8
34	32, 33	deccl 11062	. . . . . . 7 ;;;
35	34, 30	deccl 11062	. . . . . 6 ;;;;
36		eqid 2450	. . . . . 6
37	35	nn0cni 10878	. . . . . . 7 ;;;;
38	37	addid2i 9818	. . . . . 6 ;;;; ;;;;
39		3nn0 10884	. . . . . 6
40	15	addid1i 9817	. . . . . 6
41	37	mulid2i 9643	. . . . . . 7 ;;;; ;;;;
42	26	oveq1i 6298	. . . . . . . . 9
43		0p1e1 10718	. . . . . . . . 9
44	42, 43	eqtri 2472	. . . . . . . 8
45	44	oveq1i 6298	. . . . . . 7 ;;;; ;;;;
46	30, 16	nn0mulcli 10905	. . . . . . . 8
47	16, 29	deccl 11062	. . . . . . . 8 ;
48		9nn0 10890	. . . . . . . 8
49		2p1e3 10730	. . . . . . . . 9
50		8nn0 10889	. . . . . . . . . 10
51		1p1e2 10720	. . . . . . . . . . 11
52		9cn 10694	. . . . . . . . . . . . . 14
53		exp1 12275	. . . . . . . . . . . . . 14
54	52, 53	ax-mp 5	. . . . . . . . . . . . 13
55	54	oveq1i 6298	. . . . . . . . . . . 12
56		9t9e81 11150	. . . . . . . . . . . 12 ;
57	55, 56	eqtri 2472	. . . . . . . . . . 11 ;
58	48, 33, 51, 57	numexpp1 15043	. . . . . . . . . 10 ;
59		8cn 10692	. . . . . . . . . . . . 13
60		9t8e72 11149	. . . . . . . . . . . . 13 ;
61	52, 59, 60	mulcomli 9647	. . . . . . . . . . . 12 ;
62	61	oveq1i 6298	. . . . . . . . . . 11 ;
63	47	nn0cni 10878	. . . . . . . . . . . 12 ;
64	63	addid1i 9817	. . . . . . . . . . 11 ; ;
65	62, 64	eqtri 2472	. . . . . . . . . 10 ;
66	52	mulid2i 9643	. . . . . . . . . . 11
67	48	dec0h 11064	. . . . . . . . . . 11 ;
68	66, 67	eqtri 2472	. . . . . . . . . 10 ;
69	48, 50, 33, 58, 48, 28, 65, 68	decmul1c 11095	. . . . . . . . 9 ;;
70	48, 29, 49, 69	numexpp1 15043	. . . . . . . 8 ;;
71	39, 33	deccl 11062	. . . . . . . 8 ;
72		eqid 2450	. . . . . . . . 9 ; ;
73		eqid 2450	. . . . . . . . 9 ; ;
74		7t5e35 11133	. . . . . . . . . . 11 ;
75	20, 19, 74	mulcomli 9647	. . . . . . . . . 10 ;
76		7p3e10 10752	. . . . . . . . . . . 12
77	20, 15, 76	addcomli 9822	. . . . . . . . . . 11
78		dec10 11078	. . . . . . . . . . 11 ;
79	77, 78	eqtri 2472	. . . . . . . . . 10 ;
80		ax-1cn 9594	. . . . . . . . . . . . 13
81		3p1e4 10732	. . . . . . . . . . . . 13
82	15, 80, 81	addcomli 9822	. . . . . . . . . . . 12
83	82	oveq2i 6299	. . . . . . . . . . 11
84		4nn0 10885	. . . . . . . . . . . 12
85		7t3e21 11131	. . . . . . . . . . . . 13 ;
86	20, 15, 85	mulcomli 9647	. . . . . . . . . . . 12 ;
87		4cn 10684	. . . . . . . . . . . . 13
88		4p1e5 10733	. . . . . . . . . . . . 13
89	87, 80, 88	addcomli 9822	. . . . . . . . . . . 12
90	29, 33, 84, 86, 89	decaddi 11092	. . . . . . . . . . 11 ;
91	83, 90	eqtri 2472	. . . . . . . . . 10 ;
92	75	oveq1i 6298	. . . . . . . . . . 11 ;
93	39, 30	deccl 11062	. . . . . . . . . . . . 13 ;
94	93	nn0cni 10878	. . . . . . . . . . . 12 ;
95	94	addid1i 9817	. . . . . . . . . . 11 ; ;
96	92, 95	eqtri 2472	. . . . . . . . . 10 ;
97	39, 30, 33, 28, 75, 79, 16, 30, 39, 91, 96	decmac 11087	. . . . . . . . 9 ;;
98	33	dec0h 11064	. . . . . . . . . 10 ;
99		3t2e6 10758	. . . . . . . . . . . 12
100	99, 43	oveq12i 6300	. . . . . . . . . . 11
101		6p1e7 10735	. . . . . . . . . . 11
102	100, 101	eqtri 2472	. . . . . . . . . 10
103		5t2e10 10761	. . . . . . . . . . . 12
104	103, 78	eqtri 2472	. . . . . . . . . . 11 ;
105	33, 28, 43, 104	decsuc 11071	. . . . . . . . . 10 ;
106	39, 30, 28, 33, 75, 98, 29, 33, 33, 102, 105	decmac 11087	. . . . . . . . 9 ;
107	16, 29, 39, 33, 72, 73, 46, 33, 16, 97, 106	decma2c 11088	. . . . . . . 8 ; ; ;;;
108		9t3e27 11144	. . . . . . . . . . 11 ;
109	52, 15, 108	mulcomli 9647	. . . . . . . . . 10 ;
110		7p4e11 11100	. . . . . . . . . 10 ;
111	29, 16, 84, 109, 49, 33, 110	decaddci 11093	. . . . . . . . 9 ;
112		9t5e45 11146	. . . . . . . . . 10 ;
113	52, 19, 112	mulcomli 9647	. . . . . . . . 9 ;
114	48, 39, 30, 75, 30, 84, 111, 113	decmul1c 11095	. . . . . . . 8 ;;
115	46, 47, 48, 70, 30, 71, 107, 114	decmul2c 11096	. . . . . . 7 ;;;;
116	41, 45, 115	3eqtr4ri 2483	. . . . . 6 ;;;;
117	27, 28, 35, 28, 36, 38, 39, 40, 116	log2ublem2 23866	. . . . 5 ;;;;
118	48, 84	deccl 11062	. . . . . 6 ;
119	118, 30	deccl 11062	. . . . 5 ;;
120		1m1e0 10675	. . . . 5
121		eqid 2450	. . . . . 6 ;;;; ;;;;
122		eqid 2450	. . . . . 6 ;; ;;
123		6nn0 10887	. . . . . . . . 9
124	29, 123	deccl 11062	. . . . . . . 8 ;
125	124, 84	deccl 11062	. . . . . . 7 ;;
126		5p1e6 10734	. . . . . . 7
127		eqid 2450	. . . . . . . 8 ;;; ;;;
128		eqid 2450	. . . . . . . 8 ; ;
129		eqid 2450	. . . . . . . . 9 ;; ;;
130		eqid 2450	. . . . . . . . . 10 ; ;
131	29, 30, 126, 130	decsuc 11071	. . . . . . . . 9 ; ;
132		9p5e14 11113	. . . . . . . . . 10 ;
133	52, 19, 132	addcomli 9822	. . . . . . . . 9 ;
134	31, 30, 48, 129, 131, 84, 133	decaddci 11093	. . . . . . . 8 ;; ;;
135	32, 33, 48, 84, 127, 128, 134, 89	decadd 11089	. . . . . . 7 ;;; ; ;;;
136	125, 30, 126, 135	decsuc 11071	. . . . . 6 ;;; ; ;;;
137		5p5e10 10747	. . . . . 6
138	34, 30, 118, 30, 121, 122, 136, 137	decaddc2 11091	. . . . 5 ;;;; ;; ;;;;
139	52	sqvali 12351	. . . . . . . . 9
140		3t3e9 10759	. . . . . . . . . 10
141	140	oveq1i 6298	. . . . . . . . 9
142	139, 141	eqtr4i 2475	. . . . . . . 8
143	15, 15, 52	mulassi 9649	. . . . . . . 8
144	142, 143	eqtri 2472	. . . . . . 7
145	144	oveq2i 6299	. . . . . 6
146	15, 52	mulcli 9645	. . . . . . . 8
147	21, 15, 146	mul12i 9825	. . . . . . 7
148	29, 84	deccl 11062	. . . . . . . . 9 ;
149		eqid 2450	. . . . . . . . . 10 ; ;
150	99, 49	oveq12i 6300	. . . . . . . . . . 11
151		6p3e9 10749	. . . . . . . . . . 11
152	150, 151	eqtri 2472	. . . . . . . . . 10
153	87	addid2i 9818	. . . . . . . . . . 11
154	33, 28, 84, 104, 153	decaddi 11092	. . . . . . . . . 10 ;
155	39, 30, 29, 84, 75, 149, 29, 84, 33, 152, 154	decmac 11087	. . . . . . . . 9 ; ;
156	29, 33, 39, 86, 82	decaddi 11092	. . . . . . . . . 10 ;
157	16, 39, 30, 75, 30, 39, 156, 75	decmul1c 11095	. . . . . . . . 9 ;;
158	46, 29, 16, 109, 30, 148, 155, 157	decmul2c 11096	. . . . . . . 8 ;;
159	158	oveq2i 6299	. . . . . . 7 ;;
160	147, 159	eqtri 2472	. . . . . 6 ;;
161		df-3 10666	. . . . . . . 8
162	25	mulid1i 9642	. . . . . . . . 9
163	162	oveq1i 6298	. . . . . . . 8
164	161, 163	eqtr4i 2475	. . . . . . 7
165	164	oveq1i 6298	. . . . . 6 ;; ;;
166	145, 160, 165	3eqtri 2476	. . . . 5 ;;
167	117, 35, 119, 33, 120, 138, 29, 49, 166	log2ublem2 23866	. . . 4 ;;;;
168	125, 123	deccl 11062	. . . . 5 ;;;
169	168, 28	deccl 11062	. . . 4 ;;;;
170	123, 39	deccl 11062	. . . 4 ;
171		2m1e1 10721	. . . 4
172		eqid 2450	. . . . 5 ;;;; ;;;;
173		eqid 2450	. . . . 5 ; ;
174		eqid 2450	. . . . . 6 ;;; ;;;
175		eqid 2450	. . . . . . 7 ;; ;;
176	124, 84, 88, 175	decsuc 11071	. . . . . 6 ;; ;;
177		6p6e12 11099	. . . . . 6 ;
178	125, 123, 123, 174, 176, 29, 177	decaddci 11093	. . . . 5 ;;; ;;;
179	15	addid2i 9818	. . . . 5
180	168, 28, 123, 39, 172, 173, 178, 179	decadd 11089	. . . 4 ;;;; ; ;;;;
181		1p2e3 10731	. . . 4
182	54	oveq2i 6299	. . . . 5
183	19, 20, 52	mulassi 9649	. . . . . 6
184		9t7e63 11148	. . . . . . . 8 ;
185	52, 20, 184	mulcomli 9647	. . . . . . 7 ;
186	185	oveq2i 6299	. . . . . 6 ;
187	183, 186	eqtri 2472	. . . . 5 ;
188		df-5 10668	. . . . . . 7
189		2t2e4 10756	. . . . . . . 8
190	189	oveq1i 6298	. . . . . . 7
191	188, 190	eqtr4i 2475	. . . . . 6
192	191	oveq1i 6298	. . . . 5 ; ;
193	182, 187, 192	3eqtri 2476	. . . 4 ;
194	167, 169, 170, 29, 171, 180, 33, 181, 193	log2ublem2 23866	. . 3 ;;;;
195	124, 30	deccl 11062	. . . . 5 ;;
196	195, 29	deccl 11062	. . . 4 ;;;
197	196, 39	deccl 11062	. . 3 ;;;;
198		3m1e2 10723	. . 3
199		eqid 2450	. . . 4 ;;;; ;;;;
200		5p3e8 10745	. . . . 5
201	19, 15, 200	addcomli 9822	. . . 4
202	196, 39, 30, 199, 201	decaddi 11092	. . 3 ;;;; ;;;;
203	20, 19	mulcli 9645	. . . . 5
204	203	mulid1i 9642	. . . 4
205	19, 20	mulcomi 9646	. . . . 5
206		exp0 12273	. . . . . 6
207	52, 206	ax-mp 5	. . . . 5
208	205, 207	oveq12i 6300	. . . 4
209	15, 25, 99	mulcomli 9647	. . . . . . 7
210	209	oveq1i 6298	. . . . . 6
211		df-7 10670	. . . . . 6
212	210, 211	eqtr4i 2475	. . . . 5
213	212	oveq1i 6298	. . . 4
214	204, 208, 213	3eqtr4i 2482	. . 3
215	194, 197, 30, 39, 198, 202, 28, 179, 214	log2ublem2 23866	. 2 ;;;;
216		eqid 2450	. . 3 ;;;; ;;;;
217		eqid 2450	. . . 4 ;;; ;;;
218		eqid 2450	. . . . 5 ;; ;;
219		00id 9805	. . . . . 6
220	28	dec0h 11064	. . . . . 6 ;
221	219, 220	eqtri 2472	. . . . 5 ;
222		eqid 2450	. . . . . 6 ; ;
223	43, 98	eqtri 2472	. . . . . 6 ;
224	189, 43	oveq12i 6300	. . . . . . 7
225	224, 88	eqtri 2472	. . . . . 6
226		6cn 10688	. . . . . . . 8
227		6t2e12 11125	. . . . . . . 8 ;
228	226, 25, 227	mulcomli 9647	. . . . . . 7 ;
229	33, 29, 49, 228	decsuc 11071	. . . . . 6 ;
230	29, 123, 28, 33, 222, 223, 29, 39, 33, 225, 229	decma2c 11088	. . . . 5 ; ;
231	19, 25, 103	mulcomli 9647	. . . . . . 7
232	231	oveq1i 6298	. . . . . 6
233		dec10p 11077	. . . . . 6 ;
234	232, 233	eqtri 2472	. . . . 5 ;
235	124, 30, 28, 28, 218, 221, 29, 28, 33, 230, 234	decma2c 11088	. . . 4 ;; ;;
236	30	dec0h 11064	. . . . 5 ;
237	190, 88, 236	3eqtri 2476	. . . 4 ;
238	195, 29, 28, 33, 217, 98, 29, 30, 28, 235, 237	decma2c 11088	. . 3 ;;; ;;;
239		8t2e16 11136	. . . 4 ;
240	59, 25, 239	mulcomli 9647	. . 3 ;
241	29, 196, 50, 216, 123, 33, 238, 240	decmul2c 11096	. 2 ;;;; ;;;;
242	215, 241	breqtri 4425	1 ;;;;

Colors of variables: wff setvar class

Syntax hints:

wb 188

wceq 1443

wcel 1886

c0 3730 class class class wbr 4401 (class class class)co 6288

cc 9534

cr 9535

cc0 9536

c1 9537

caddc 9539

cmul 9541

clt 9672

cle 9673

cmin 9857

cdiv 10266

c2 10656

c3 10657

c4 10658

c5 10659

c6 10660

c7 10661

c8 10662

c9 10663

c10 10664

cn0 10866

cz 10934 ;cdc 11048

cfz 11781

cexp 12269

csu 13745

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-rep 4514 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 ax-inf2 8143 ax-cnex 9592 ax-resscn 9593 ax-1cn 9594 ax-icn 9595 ax-addcl 9596 ax-addrcl 9597 ax-mulcl 9598 ax-mulrcl 9599 ax-mulcom 9600 ax-addass 9601 ax-mulass 9602 ax-distr 9603 ax-i2m1 9604 ax-1ne0 9605 ax-1rid 9606 ax-rnegex 9607 ax-rrecex 9608 ax-cnre 9609 ax-pre-lttri 9610 ax-pre-lttrn 9611 ax-pre-ltadd 9612 ax-pre-mulgt0 9613 ax-pre-sup 9614

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 985 df-3an 986 df-tru 1446 df-fal 1449 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-pss 3419 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-tp 3972 df-op 3974 df-uni 4198 df-int 4234 df-iun 4279 df-br 4402 df-opab 4461 df-mpt 4462 df-tr 4497 df-eprel 4744 df-id 4748 df-po 4754 df-so 4755 df-fr 4792 df-se 4793 df-we 4794 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-pred 5379 df-ord 5425 df-on 5426 df-lim 5427 df-suc 5428 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-isom 5590 df-riota 6250 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-om 6690 df-1st 6790 df-2nd 6791 df-wrecs 7025 df-recs 7087 df-rdg 7125 df-1o 7179 df-oadd 7183 df-er 7360 df-en 7567 df-dom 7568 df-sdom 7569 df-fin 7570 df-sup 7953 df-oi 8022 df-card 8370 df-pnf 9674 df-mnf 9675 df-xr 9676 df-ltxr 9677 df-le 9678 df-sub 9859 df-neg 9860 df-div 10267 df-nn 10607 df-2 10665 df-3 10666 df-4 10667 df-5 10668 df-6 10669 df-7 10670 df-8 10671 df-9 10672 df-10 10673 df-n0 10867 df-z 10935 df-dec 11049 df-uz 11157 df-rp 11300 df-fz 11782 df-fzo 11913 df-seq 12211 df-exp 12270 df-hash 12513 df-cj 13155 df-re 13156 df-im 13157 df-sqrt 13291 df-abs 13292 df-clim 13545 df-sum 13746

This theorem is referenced by: log2ub 23868

W3C validator