Theorem log2ublem3

Description: Lemma for log2ub . In decimal, this is a proof that the first four terms of the series for log 2 is less than 5 3 0 5 6 / 7 6 5 4 5 . (Contributed by Mario Carneiro, 17-Apr-2015) (Proof shortened by AV, 15-Sep-2021)

	Ref	Expression
Assertion	log2ublem3	$$⊢3^{7}5\cdot 7\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)\le 53056$$

Proof

Step	Hyp	Ref	Expression
1		0le0	$$⊢0\le 0$$
2		fz00m1	$$⊢\left(0\dots 0-1\right)=\varnothing$$
3	2	sumeq1i	$$⊢\sum _{n=0}^{0-1}\left(\frac{2}{3\left(2n+1\right)9^n}\right)=\sum _{n\in \varnothing }\left(\frac{2}{3\left(2n+1\right)9^n}\right)$$
4		sum0	$$⊢\sum _{n\in \varnothing }\left(\frac{2}{3\left(2n+1\right)9^n}\right)=0$$
5	3 4	eqtri	$$⊢\sum _{n=0}^{0-1}\left(\frac{2}{3\left(2n+1\right)9^n}\right)=0$$
6	5	oveq2i	$$⊢3^{7}5\cdot 7\sum _{n=0}^{0-1}\left(\frac{2}{3\left(2n+1\right)9^n}\right)=3^{7}5\cdot 7\cdot 0$$
7		3cn	$$⊢3\in ℂ$$
8		7nn0	$$⊢7\in {\mathbb{N}}_0$$
9		expcl	$$⊢\left(3\in ℂ\wedge 7\in {\mathbb{N}}_0\right)\to 3^7\in ℂ$$
10	7 8 9	mp2an	$$⊢3^7\in ℂ$$
11		5cn	$$⊢5\in ℂ$$
12		7cn	$$⊢7\in ℂ$$
13	11 12	mulcli	$$⊢5\cdot 7\in ℂ$$
14	10 13	mulcli	$$⊢3^{7}5\cdot 7\in ℂ$$
15	14	mul01i	$$⊢3^{7}5\cdot 7\cdot 0=0$$
16	6 15	eqtri	$$⊢3^{7}5\cdot 7\sum _{n=0}^{0-1}\left(\frac{2}{3\left(2n+1\right)9^n}\right)=0$$
17		2cn	$$⊢2\in ℂ$$
18	17	mul01i	$$⊢2\cdot 0=0$$
19	1 16 18	3brtr4i	$$⊢3^{7}5\cdot 7\sum _{n=0}^{0-1}\left(\frac{2}{3\left(2n+1\right)9^n}\right)\le 2\cdot 0$$
20		0nn0	$$⊢0\in {\mathbb{N}}_0$$
21		2nn0	$$⊢2\in {\mathbb{N}}_0$$
22		5nn0	$$⊢5\in {\mathbb{N}}_0$$
23	21 22	deccl	$$⊢25\in {\mathbb{N}}_0$$
24	23 22	deccl	$$⊢255\in {\mathbb{N}}_0$$
25		1nn0	$$⊢1\in {\mathbb{N}}_0$$
26	24 25	deccl	$$⊢2551\in {\mathbb{N}}_0$$
27	26 22	deccl	$$⊢25515\in {\mathbb{N}}_0$$
28		eqid	$$⊢0-1=0-1$$
29	27	nn0cni	$$⊢25515\in ℂ$$
30	29	addlidi	$$⊢0+25515=25515$$
31		3nn0	$$⊢3\in {\mathbb{N}}_0$$
32	7	addridi	$$⊢3+0=3$$
33	29	mullidi	$$⊢1\cdot 25515=25515$$
34	18	oveq1i	$$⊢2\cdot 0+1=0+1$$
35		0p1e1	$$⊢0+1=1$$
36	34 35	eqtri	$$⊢2\cdot 0+1=1$$
37	36	oveq1i	$$⊢\left(2\cdot 0+1\right)\cdot 25515=1\cdot 25515$$
38	22 8	nn0mulcli	$$⊢5\cdot 7\in {\mathbb{N}}_0$$
39	8 21	deccl	$$⊢72\in {\mathbb{N}}_0$$
40		9nn0	$$⊢9\in {\mathbb{N}}_0$$
41		2p1e3	$$⊢2+1=3$$
42		8nn0	$$⊢8\in {\mathbb{N}}_0$$
43		1p1e2	$$⊢1+1=2$$
44		9cn	$$⊢9\in ℂ$$
45		exp1	$$⊢9\in ℂ\to 9^1=9$$
46	44 45	ax-mp	$$⊢9^1=9$$
47	46	oveq1i	$$⊢9^1\cdot 9=9\cdot 9$$
48		9t9e81	$$⊢9\cdot 9=81$$
49	47 48	eqtri	$$⊢9^1\cdot 9=81$$
50	40 25 43 49	numexpp1	$$⊢9^2=81$$
51		8cn	$$⊢8\in ℂ$$
52		9t8e72	$$⊢9\cdot 8=72$$
53	44 51 52	mulcomli	$$⊢8\cdot 9=72$$
54	44	mullidi	$$⊢1\cdot 9=9$$
55	40 42 25 50 53 54	decmul1	$$⊢9^2\cdot 9=729$$
56	40 21 41 55	numexpp1	$$⊢9^3=729$$
57	31 25	deccl	$$⊢31\in {\mathbb{N}}_0$$
58		eqid	$$⊢72=72$$
59		eqid	$$⊢31=31$$
60		7t5e35	$$⊢7\cdot 5=35$$
61	12 11 60	mulcomli	$$⊢5\cdot 7=35$$
62		7p3e10	$$⊢7+3=10$$
63	12 7 62	addcomli	$$⊢3+7=10$$
64		ax-1cn	$$⊢1\in ℂ$$
65		3p1e4	$$⊢3+1=4$$
66	7 64 65	addcomli	$$⊢1+3=4$$
67	66	oveq2i	$$⊢3\cdot 7+1+3=3\cdot 7+4$$
68		4nn0	$$⊢4\in {\mathbb{N}}_0$$
69		7t3e21	$$⊢7\cdot 3=21$$
70	12 7 69	mulcomli	$$⊢3\cdot 7=21$$
71		4cn	$$⊢4\in ℂ$$
72		4p1e5	$$⊢4+1=5$$
73	71 64 72	addcomli	$$⊢1+4=5$$
74	21 25 68 70 73	decaddi	$$⊢3\cdot 7+4=25$$
75	67 74	eqtri	$$⊢3\cdot 7+1+3=25$$
76	61	oveq1i	$$⊢5\cdot 7+0=35+0$$
77	31 22	deccl	$$⊢35\in {\mathbb{N}}_0$$
78	77	nn0cni	$$⊢35\in ℂ$$
79	78	addridi	$$⊢35+0=35$$
80	76 79	eqtri	$$⊢5\cdot 7+0=35$$
81	31 22 25 20 61 63 8 22 31 75 80	decmac	$$⊢5\cdot 7\cdot 7+3+7=255$$
82	25	dec0h	$$⊢1=01$$
83		3t2e6	$$⊢3\cdot 2=6$$
84	83 35	oveq12i	$$⊢3\cdot 2+0+1=6+1$$
85		6p1e7	$$⊢6+1=7$$
86	84 85	eqtri	$$⊢3\cdot 2+0+1=7$$
87		5t2e10	$$⊢5\cdot 2=10$$
88	25 20 35 87	decsuc	$$⊢5\cdot 2+1=11$$
89	31 22 20 25 61 82 21 25 25 86 88	decmac	$$⊢5\cdot 7\cdot 2+1=71$$
90	8 21 31 25 58 59 38 25 8 81 89	decma2c	$$⊢5\cdot 7\cdot 72+31=2551$$
91		9t3e27	$$⊢9\cdot 3=27$$
92	44 7 91	mulcomli	$$⊢3\cdot 9=27$$
93		7p4e11	$$⊢7+4=11$$
94	21 8 68 92 41 25 93	decaddci	$$⊢3\cdot 9+4=31$$
95		9t5e45	$$⊢9\cdot 5=45$$
96	44 11 95	mulcomli	$$⊢5\cdot 9=45$$
97	40 31 22 61 22 68 94 96	decmul1c	$$⊢5\cdot 7\cdot 9=315$$
98	38 39 40 56 22 57 90 97	decmul2c	$$⊢5\cdot 79^3=25515$$
99	33 37 98	3eqtr4ri	$$⊢5\cdot 79^3=\left(2\cdot 0+1\right)\cdot 25515$$
100	19 20 27 20 28 30 31 32 99	log2ublem2	$$⊢3^{7}5\cdot 7\sum _{n=0}^0\left(\frac{2}{3\left(2n+1\right)9^n}\right)\le 2\cdot 25515$$
101	40 68	deccl	$$⊢94\in {\mathbb{N}}_0$$
102	101 22	deccl	$$⊢945\in {\mathbb{N}}_0$$
103		1m1e0	$$⊢1-1=0$$
104		eqid	$$⊢25515=25515$$
105		eqid	$$⊢945=945$$
106		6nn0	$$⊢6\in {\mathbb{N}}_0$$
107	21 106	deccl	$$⊢26\in {\mathbb{N}}_0$$
108	107 68	deccl	$$⊢264\in {\mathbb{N}}_0$$
109		5p1e6	$$⊢5+1=6$$
110		eqid	$$⊢2551=2551$$
111		eqid	$$⊢94=94$$
112		eqid	$$⊢255=255$$
113		eqid	$$⊢25=25$$
114	21 22 109 113	decsuc	$$⊢25+1=26$$
115		9p5e14	$$⊢9+5=14$$
116	44 11 115	addcomli	$$⊢5+9=14$$
117	23 22 40 112 114 68 116	decaddci	$$⊢255+9=264$$
118	24 25 40 68 110 111 117 73	decadd	$$⊢2551+94=2645$$
119	108 22 109 118	decsuc	$$⊢2551+94+1=2646$$
120		5p5e10	$$⊢5+5=10$$
121	26 22 101 22 104 105 119 120	decaddc2	$$⊢25515+945=26460$$
122	44	sqvali	$$⊢9^2=9\cdot 9$$
123		3t3e9	$$⊢3\cdot 3=9$$
124	123	oveq1i	$$⊢3\cdot 3\cdot 9=9\cdot 9$$
125	7 7 44	mulassi	$$⊢3\cdot 3\cdot 9=33\cdot 9$$
126	122 124 125	3eqtr2i	$$⊢9^2=33\cdot 9$$
127	126	oveq2i	$$⊢5\cdot 79^2=5\cdot 733\cdot 9$$
128	7 44	mulcli	$$⊢3\cdot 9\in ℂ$$
129	13 7 128	mul12i	$$⊢5\cdot 733\cdot 9=35\cdot 73\cdot 9$$
130	21 68	deccl	$$⊢24\in {\mathbb{N}}_0$$
131		eqid	$$⊢24=24$$
132	83 41	oveq12i	$$⊢3\cdot 2+2+1=6+3$$
133		6p3e9	$$⊢6+3=9$$
134	132 133	eqtri	$$⊢3\cdot 2+2+1=9$$
135	71	addlidi	$$⊢0+4=4$$
136	25 20 68 87 135	decaddi	$$⊢5\cdot 2+4=14$$
137	31 22 21 68 61 131 21 68 25 134 136	decmac	$$⊢5\cdot 7\cdot 2+24=94$$
138	21 25 31 70 66	decaddi	$$⊢3\cdot 7+3=24$$
139	8 31 22 61 22 31 138 61	decmul1c	$$⊢5\cdot 7\cdot 7=245$$
140	38 21 8 92 22 130 137 139	decmul2c	$$⊢5\cdot 73\cdot 9=945$$
141	140	oveq2i	$$⊢35\cdot 73\cdot 9=3\cdot 945$$
142	129 141	eqtri	$$⊢5\cdot 733\cdot 9=3\cdot 945$$
143		df-3	$$⊢3=2+1$$
144	17	mulridi	$$⊢2\cdot 1=2$$
145	144	oveq1i	$$⊢2\cdot 1+1=2+1$$
146	143 145	eqtr4i	$$⊢3=2\cdot 1+1$$
147	146	oveq1i	$$⊢3\cdot 945=\left(2\cdot 1+1\right)\cdot 945$$
148	127 142 147	3eqtri	$$⊢5\cdot 79^2=\left(2\cdot 1+1\right)\cdot 945$$
149	100 27 102 25 103 121 21 41 148	log2ublem2	$$⊢3^{7}5\cdot 7\sum _{n=0}^1\left(\frac{2}{3\left(2n+1\right)9^n}\right)\le 2\cdot 26460$$
150	108 106	deccl	$$⊢2646\in {\mathbb{N}}_0$$
151	150 20	deccl	$$⊢26460\in {\mathbb{N}}_0$$
152	106 31	deccl	$$⊢63\in {\mathbb{N}}_0$$
153		2m1e1	$$⊢2-1=1$$
154		eqid	$$⊢26460=26460$$
155		eqid	$$⊢63=63$$
156		eqid	$$⊢2646=2646$$
157		eqid	$$⊢264=264$$
158	107 68 72 157	decsuc	$$⊢264+1=265$$
159		6p6e12	$$⊢6+6=12$$
160	108 106 106 156 158 21 159	decaddci	$$⊢2646+6=2652$$
161	7	addlidi	$$⊢0+3=3$$
162	150 20 106 31 154 155 160 161	decadd	$$⊢26460+63=26523$$
163		1p2e3	$$⊢1+2=3$$
164	46	oveq2i	$$⊢5\cdot 79^1=5\cdot 7\cdot 9$$
165	11 12 44	mulassi	$$⊢5\cdot 7\cdot 9=57\cdot 9$$
166		9t7e63	$$⊢9\cdot 7=63$$
167	44 12 166	mulcomli	$$⊢7\cdot 9=63$$
168	167	oveq2i	$$⊢57\cdot 9=5\cdot 63$$
169	165 168	eqtri	$$⊢5\cdot 7\cdot 9=5\cdot 63$$
170		df-5	$$⊢5=4+1$$
171		2t2e4	$$⊢2\cdot 2=4$$
172	171	oveq1i	$$⊢2\cdot 2+1=4+1$$
173	170 172	eqtr4i	$$⊢5=2\cdot 2+1$$
174	173	oveq1i	$$⊢5\cdot 63=\left(2\cdot 2+1\right)\cdot 63$$
175	164 169 174	3eqtri	$$⊢5\cdot 79^1=\left(2\cdot 2+1\right)\cdot 63$$
176	149 151 152 21 153 162 25 163 175	log2ublem2	$$⊢3^{7}5\cdot 7\sum _{n=0}^2\left(\frac{2}{3\left(2n+1\right)9^n}\right)\le 2\cdot 26523$$
177	107 22	deccl	$$⊢265\in {\mathbb{N}}_0$$
178	177 21	deccl	$$⊢2652\in {\mathbb{N}}_0$$
179	178 31	deccl	$$⊢26523\in {\mathbb{N}}_0$$
180		3m1e2	$$⊢3-1=2$$
181		eqid	$$⊢26523=26523$$
182		5p3e8	$$⊢5+3=8$$
183	11 7 182	addcomli	$$⊢3+5=8$$
184	178 31 22 181 183	decaddi	$$⊢26523+5=26528$$
185	12 11	mulcli	$$⊢7\cdot 5\in ℂ$$
186	185	mulridi	$$⊢7\cdot 5\cdot 1=7\cdot 5$$
187	11 12	mulcomi	$$⊢5\cdot 7=7\cdot 5$$
188		exp0	$$⊢9\in ℂ\to 9^0=1$$
189	44 188	ax-mp	$$⊢9^0=1$$
190	187 189	oveq12i	$$⊢5\cdot 79^0=7\cdot 5\cdot 1$$
191		2t3e6	$$⊢2\cdot 3=6$$
192	191	oveq1i	$$⊢2\cdot 3+1=6+1$$
193		df-7	$$⊢7=6+1$$
194	192 193	eqtr4i	$$⊢2\cdot 3+1=7$$
195	194	oveq1i	$$⊢\left(2\cdot 3+1\right)\cdot 5=7\cdot 5$$
196	186 190 195	3eqtr4i	$$⊢5\cdot 79^0=\left(2\cdot 3+1\right)\cdot 5$$
197	176 179 22 31 180 184 20 161 196	log2ublem2	$$⊢3^{7}5\cdot 7\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)\le 2\cdot 26528$$
198		eqid	$$⊢26528=26528$$
199		eqid	$$⊢2652=2652$$
200		eqid	$$⊢265=265$$
201		00id	$$⊢0+0=0$$
202	20	dec0h	$$⊢0=00$$
203	201 202	eqtri	$$⊢0+0=00$$
204		eqid	$$⊢26=26$$
205	35 82	eqtri	$$⊢0+1=01$$
206	171 35	oveq12i	$$⊢2\cdot 2+0+1=4+1$$
207	206 72	eqtri	$$⊢2\cdot 2+0+1=5$$
208		6cn	$$⊢6\in ℂ$$
209		6t2e12	$$⊢6\cdot 2=12$$
210	208 17 209	mulcomli	$$⊢2\cdot 6=12$$
211	25 21 41 210	decsuc	$$⊢2\cdot 6+1=13$$
212	21 106 20 25 204 205 21 31 25 207 211	decma2c	$$⊢2\cdot 26+0+1=53$$
213	11 17 87	mulcomli	$$⊢2\cdot 5=10$$
214	213	oveq1i	$$⊢2\cdot 5+0=10+0$$
215		dec10p	$$⊢10+0=10$$
216	214 215	eqtri	$$⊢2\cdot 5+0=10$$
217	107 22 20 20 200 203 21 20 25 212 216	decma2c	$$⊢2\cdot 265+0+0=530$$
218	22	dec0h	$$⊢5=05$$
219	172 72 218	3eqtri	$$⊢2\cdot 2+1=05$$
220	177 21 20 25 199 82 21 22 20 217 219	decma2c	$$⊢2\cdot 2652+1=5305$$
221		8t2e16	$$⊢8\cdot 2=16$$
222	51 17 221	mulcomli	$$⊢2\cdot 8=16$$
223	21 178 42 198 106 25 220 222	decmul2c	$$⊢2\cdot 26528=53056$$
224	197 223	breqtri	$$⊢3^{7}5\cdot 7\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)\le 53056$$