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 24675

Description: Lemma for log2ub 24676. 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.) (Proof shortened by AV, 15-Sep-2021.)

**Assertion**
Ref	Expression
log2ublem3	;;;;

**Proof of Theorem log2ublem3**
Step	Hyp	Ref	Expression
1		0le0 11110	. . . . . . 7
2		risefall0lem 14757	. . . . . . . . . . 11
3	2	sumeq1i 14428	. . . . . . . . . 10
4		sum0 14452	. . . . . . . . . 10
5	3, 4	eqtri 2644	. . . . . . . . 9
6	5	oveq2i 6661	. . . . . . . 8
7		3cn 11095	. . . . . . . . . . 11
8		7nn0 11314	. . . . . . . . . . 11
9		expcl 12878	. . . . . . . . . . 11 $/\$
10	7, 8, 9	mp2an 708	. . . . . . . . . 10
11		5cn 11100	. . . . . . . . . . 11
12		7cn 11104	. . . . . . . . . . 11
13	11, 12	mulcli 10045	. . . . . . . . . 10
14	10, 13	mulcli 10045	. . . . . . . . 9
15	14	mul01i 10226	. . . . . . . 8
16	6, 15	eqtri 2644	. . . . . . 7
17		2cn 11091	. . . . . . . 8
18	17	mul01i 10226	. . . . . . 7
19	1, 16, 18	3brtr4i 4683	. . . . . 6
20		0nn0 11307	. . . . . 6
21		2nn0 11309	. . . . . . . . . 10
22		5nn0 11312	. . . . . . . . . 10
23	21, 22	deccl 11512	. . . . . . . . 9 ;
24	23, 22	deccl 11512	. . . . . . . 8 ;;
25		1nn0 11308	. . . . . . . 8
26	24, 25	deccl 11512	. . . . . . 7 ;;;
27	26, 22	deccl 11512	. . . . . 6 ;;;;
28		eqid 2622	. . . . . 6
29	27	nn0cni 11304	. . . . . . 7 ;;;;
30	29	addid2i 10224	. . . . . 6 ;;;; ;;;;
31		3nn0 11310	. . . . . 6
32	7	addid1i 10223	. . . . . 6
33	29	mulid2i 10043	. . . . . . 7 ;;;; ;;;;
34	18	oveq1i 6660	. . . . . . . . 9
35		0p1e1 11132	. . . . . . . . 9
36	34, 35	eqtri 2644	. . . . . . . 8
37	36	oveq1i 6660	. . . . . . 7 ;;;; ;;;;
38	22, 8	nn0mulcli 11331	. . . . . . . 8
39	8, 21	deccl 11512	. . . . . . . 8 ;
40		9nn0 11316	. . . . . . . 8
41		2p1e3 11151	. . . . . . . . 9
42		8nn0 11315	. . . . . . . . . 10
43		1p1e2 11134	. . . . . . . . . . 11
44		9cn 11108	. . . . . . . . . . . . . 14
45		exp1 12866	. . . . . . . . . . . . . 14
46	44, 45	ax-mp 5	. . . . . . . . . . . . 13
47	46	oveq1i 6660	. . . . . . . . . . . 12
48		9t9e81 11670	. . . . . . . . . . . 12 ;
49	47, 48	eqtri 2644	. . . . . . . . . . 11 ;
50	40, 25, 43, 49	numexpp1 15782	. . . . . . . . . 10 ;
51		8cn 11106	. . . . . . . . . . 11
52		9t8e72 11669	. . . . . . . . . . 11 ;
53	44, 51, 52	mulcomli 10047	. . . . . . . . . 10 ;
54	44	mulid2i 10043	. . . . . . . . . 10
55	40, 42, 25, 50, 40, 53, 54	decmul1 11585	. . . . . . . . 9 ;;
56	40, 21, 41, 55	numexpp1 15782	. . . . . . . 8 ;;
57	31, 25	deccl 11512	. . . . . . . 8 ;
58		eqid 2622	. . . . . . . . 9 ; ;
59		eqid 2622	. . . . . . . . 9 ; ;
60		7t5e35 11651	. . . . . . . . . . 11 ;
61	12, 11, 60	mulcomli 10047	. . . . . . . . . 10 ;
62		7p3e10 11603	. . . . . . . . . . 11 ;
63	12, 7, 62	addcomli 10228	. . . . . . . . . 10 ;
64		ax-1cn 9994	. . . . . . . . . . . . 13
65		3p1e4 11153	. . . . . . . . . . . . 13
66	7, 64, 65	addcomli 10228	. . . . . . . . . . . 12
67	66	oveq2i 6661	. . . . . . . . . . 11
68		4nn0 11311	. . . . . . . . . . . 12
69		7t3e21 11649	. . . . . . . . . . . . 13 ;
70	12, 7, 69	mulcomli 10047	. . . . . . . . . . . 12 ;
71		4cn 11098	. . . . . . . . . . . . 13
72		4p1e5 11154	. . . . . . . . . . . . 13
73	71, 64, 72	addcomli 10228	. . . . . . . . . . . 12
74	21, 25, 68, 70, 73	decaddi 11579	. . . . . . . . . . 11 ;
75	67, 74	eqtri 2644	. . . . . . . . . 10 ;
76	61	oveq1i 6660	. . . . . . . . . . 11 ;
77	31, 22	deccl 11512	. . . . . . . . . . . . 13 ;
78	77	nn0cni 11304	. . . . . . . . . . . 12 ;
79	78	addid1i 10223	. . . . . . . . . . 11 ; ;
80	76, 79	eqtri 2644	. . . . . . . . . 10 ;
81	31, 22, 25, 20, 61, 63, 8, 22, 31, 75, 80	decmac 11566	. . . . . . . . 9 ;;
82	25	dec0h 11522	. . . . . . . . . 10 ;
83		3t2e6 11179	. . . . . . . . . . . 12
84	83, 35	oveq12i 6662	. . . . . . . . . . 11
85		6p1e7 11156	. . . . . . . . . . 11
86	84, 85	eqtri 2644	. . . . . . . . . 10
87		5t2e10 11634	. . . . . . . . . . 11 ;
88	25, 20, 35, 87	decsuc 11535	. . . . . . . . . 10 ;
89	31, 22, 20, 25, 61, 82, 21, 25, 25, 86, 88	decmac 11566	. . . . . . . . 9 ;
90	8, 21, 31, 25, 58, 59, 38, 25, 8, 81, 89	decma2c 11568	. . . . . . . 8 ; ; ;;;
91		9t3e27 11664	. . . . . . . . . . 11 ;
92	44, 7, 91	mulcomli 10047	. . . . . . . . . 10 ;
93		7p4e11 11605	. . . . . . . . . 10 ;
94	21, 8, 68, 92, 41, 25, 93	decaddci 11580	. . . . . . . . 9 ;
95		9t5e45 11666	. . . . . . . . . 10 ;
96	44, 11, 95	mulcomli 10047	. . . . . . . . 9 ;
97	40, 31, 22, 61, 22, 68, 94, 96	decmul1c 11587	. . . . . . . 8 ;;
98	38, 39, 40, 56, 22, 57, 90, 97	decmul2c 11589	. . . . . . 7 ;;;;
99	33, 37, 98	3eqtr4ri 2655	. . . . . 6 ;;;;
100	19, 20, 27, 20, 28, 30, 31, 32, 99	log2ublem2 24674	. . . . 5 ;;;;
101	40, 68	deccl 11512	. . . . . 6 ;
102	101, 22	deccl 11512	. . . . 5 ;;
103		1m1e0 11089	. . . . 5
104		eqid 2622	. . . . . 6 ;;;; ;;;;
105		eqid 2622	. . . . . 6 ;; ;;
106		6nn0 11313	. . . . . . . . 9
107	21, 106	deccl 11512	. . . . . . . 8 ;
108	107, 68	deccl 11512	. . . . . . 7 ;;
109		5p1e6 11155	. . . . . . 7
110		eqid 2622	. . . . . . . 8 ;;; ;;;
111		eqid 2622	. . . . . . . 8 ; ;
112		eqid 2622	. . . . . . . . 9 ;; ;;
113		eqid 2622	. . . . . . . . . 10 ; ;
114	21, 22, 109, 113	decsuc 11535	. . . . . . . . 9 ; ;
115		9p5e14 11623	. . . . . . . . . 10 ;
116	44, 11, 115	addcomli 10228	. . . . . . . . 9 ;
117	23, 22, 40, 112, 114, 68, 116	decaddci 11580	. . . . . . . 8 ;; ;;
118	24, 25, 40, 68, 110, 111, 117, 73	decadd 11570	. . . . . . 7 ;;; ; ;;;
119	108, 22, 109, 118	decsuc 11535	. . . . . 6 ;;; ; ;;;
120		5p5e10 11596	. . . . . 6 ;
121	26, 22, 101, 22, 104, 105, 119, 120	decaddc2 11575	. . . . 5 ;;;; ;; ;;;;
122	44	sqvali 12943	. . . . . . . 8
123		3t3e9 11180	. . . . . . . . 9
124	123	oveq1i 6660	. . . . . . . 8
125	7, 7, 44	mulassi 10049	. . . . . . . 8
126	122, 124, 125	3eqtr2i 2650	. . . . . . 7
127	126	oveq2i 6661	. . . . . 6
128	7, 44	mulcli 10045	. . . . . . . 8
129	13, 7, 128	mul12i 10231	. . . . . . 7
130	21, 68	deccl 11512	. . . . . . . . 9 ;
131		eqid 2622	. . . . . . . . . 10 ; ;
132	83, 41	oveq12i 6662	. . . . . . . . . . 11
133		6p3e9 11170	. . . . . . . . . . 11
134	132, 133	eqtri 2644	. . . . . . . . . 10
135	71	addid2i 10224	. . . . . . . . . . 11
136	25, 20, 68, 87, 135	decaddi 11579	. . . . . . . . . 10 ;
137	31, 22, 21, 68, 61, 131, 21, 68, 25, 134, 136	decmac 11566	. . . . . . . . 9 ; ;
138	21, 25, 31, 70, 66	decaddi 11579	. . . . . . . . . 10 ;
139	8, 31, 22, 61, 22, 31, 138, 61	decmul1c 11587	. . . . . . . . 9 ;;
140	38, 21, 8, 92, 22, 130, 137, 139	decmul2c 11589	. . . . . . . 8 ;;
141	140	oveq2i 6661	. . . . . . 7 ;;
142	129, 141	eqtri 2644	. . . . . 6 ;;
143		df-3 11080	. . . . . . . 8
144	17	mulid1i 10042	. . . . . . . . 9
145	144	oveq1i 6660	. . . . . . . 8
146	143, 145	eqtr4i 2647	. . . . . . 7
147	146	oveq1i 6660	. . . . . 6 ;; ;;
148	127, 142, 147	3eqtri 2648	. . . . 5 ;;
149	100, 27, 102, 25, 103, 121, 21, 41, 148	log2ublem2 24674	. . . 4 ;;;;
150	108, 106	deccl 11512	. . . . 5 ;;;
151	150, 20	deccl 11512	. . . 4 ;;;;
152	106, 31	deccl 11512	. . . 4 ;
153		2m1e1 11135	. . . 4
154		eqid 2622	. . . . 5 ;;;; ;;;;
155		eqid 2622	. . . . 5 ; ;
156		eqid 2622	. . . . . 6 ;;; ;;;
157		eqid 2622	. . . . . . 7 ;; ;;
158	107, 68, 72, 157	decsuc 11535	. . . . . 6 ;; ;;
159		6p6e12 11602	. . . . . 6 ;
160	108, 106, 106, 156, 158, 21, 159	decaddci 11580	. . . . 5 ;;; ;;;
161	7	addid2i 10224	. . . . 5
162	150, 20, 106, 31, 154, 155, 160, 161	decadd 11570	. . . 4 ;;;; ; ;;;;
163		1p2e3 11152	. . . 4
164	46	oveq2i 6661	. . . . 5
165	11, 12, 44	mulassi 10049	. . . . . 6
166		9t7e63 11668	. . . . . . . 8 ;
167	44, 12, 166	mulcomli 10047	. . . . . . 7 ;
168	167	oveq2i 6661	. . . . . 6 ;
169	165, 168	eqtri 2644	. . . . 5 ;
170		df-5 11082	. . . . . . 7
171		2t2e4 11177	. . . . . . . 8
172	171	oveq1i 6660	. . . . . . 7
173	170, 172	eqtr4i 2647	. . . . . 6
174	173	oveq1i 6660	. . . . 5 ; ;
175	164, 169, 174	3eqtri 2648	. . . 4 ;
176	149, 151, 152, 21, 153, 162, 25, 163, 175	log2ublem2 24674	. . 3 ;;;;
177	107, 22	deccl 11512	. . . . 5 ;;
178	177, 21	deccl 11512	. . . 4 ;;;
179	178, 31	deccl 11512	. . 3 ;;;;
180		3m1e2 11137	. . 3
181		eqid 2622	. . . 4 ;;;; ;;;;
182		5p3e8 11166	. . . . 5
183	11, 7, 182	addcomli 10228	. . . 4
184	178, 31, 22, 181, 183	decaddi 11579	. . 3 ;;;; ;;;;
185	12, 11	mulcli 10045	. . . . 5
186	185	mulid1i 10042	. . . 4
187	11, 12	mulcomi 10046	. . . . 5
188		exp0 12864	. . . . . 6
189	44, 188	ax-mp 5	. . . . 5
190	187, 189	oveq12i 6662	. . . 4
191	7, 17, 83	mulcomli 10047	. . . . . . 7
192	191	oveq1i 6660	. . . . . 6
193		df-7 11084	. . . . . 6
194	192, 193	eqtr4i 2647	. . . . 5
195	194	oveq1i 6660	. . . 4
196	186, 190, 195	3eqtr4i 2654	. . 3
197	176, 179, 22, 31, 180, 184, 20, 161, 196	log2ublem2 24674	. 2 ;;;;
198		eqid 2622	. . 3 ;;;; ;;;;
199		eqid 2622	. . . 4 ;;; ;;;
200		eqid 2622	. . . . 5 ;; ;;
201		00id 10211	. . . . . 6
202	20	dec0h 11522	. . . . . 6 ;
203	201, 202	eqtri 2644	. . . . 5 ;
204		eqid 2622	. . . . . 6 ; ;
205	35, 82	eqtri 2644	. . . . . 6 ;
206	171, 35	oveq12i 6662	. . . . . . 7
207	206, 72	eqtri 2644	. . . . . 6
208		6cn 11102	. . . . . . . 8
209		6t2e12 11641	. . . . . . . 8 ;
210	208, 17, 209	mulcomli 10047	. . . . . . 7 ;
211	25, 21, 41, 210	decsuc 11535	. . . . . 6 ;
212	21, 106, 20, 25, 204, 205, 21, 31, 25, 207, 211	decma2c 11568	. . . . 5 ; ;
213	11, 17, 87	mulcomli 10047	. . . . . . 7 ;
214	213	oveq1i 6660	. . . . . 6 ;
215		dec10p 11553	. . . . . 6 ; ;
216	214, 215	eqtri 2644	. . . . 5 ;
217	107, 22, 20, 20, 200, 203, 21, 20, 25, 212, 216	decma2c 11568	. . . 4 ;; ;;
218	22	dec0h 11522	. . . . 5 ;
219	172, 72, 218	3eqtri 2648	. . . 4 ;
220	177, 21, 20, 25, 199, 82, 21, 22, 20, 217, 219	decma2c 11568	. . 3 ;;; ;;;
221		8t2e16 11654	. . . 4 ;
222	51, 17, 221	mulcomli 10047	. . 3 ;
223	21, 178, 42, 198, 106, 25, 220, 222	decmul2c 11589	. 2 ;;;; ;;;;
224	197, 223	breqtri 4678	1 ;;;;

Colors of variables: wff setvar class

Syntax hints:

wceq 1483

wcel 1990

c0 3915 class class class wbr 4653 (class class class)co 6650

cc 9934

cc0 9936

c1 9937

caddc 9939

cmul 9941

cle 10075

cmin 10266

cdiv 10684

c2 11070

c3 11071

c4 11072

c5 11073

c6 11074

c7 11075

c8 11076

c9 11077

cn0 11292 ;cdc 11493

cfz 12326

cexp 12860

csu 14416

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-oi 8415 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-rp 11833 df-fz 12327 df-fzo 12466 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-sum 14417

This theorem is referenced by: log2ub 24676

W3C validator