Theorem log2ub

Description: log 2 is less than 2 5 3 / 3 6 5 . If written in decimal, this is because log 2 = 0.693147... is less than 253/365 = 0.693151... , so this is a very tight bound, at five decimal places. (Contributed by Mario Carneiro, 7-Apr-2015) (Proof shortened by AV, 16-Sep-2021)

	Ref	Expression
Assertion	log2ub	$$⊢\log 2<\frac{253}{365}$$

Proof

Step	Hyp	Ref	Expression
1		4m1e3	$$⊢4-1=3$$
2	1	oveq2i	$$⊢\left(0\dots 4-1\right)=\left(0\dots 3\right)$$
3	2	sumeq1i	$$⊢\sum _{n=0}^{4-1}\left(\frac{2}{3\left(2n+1\right)9^n}\right)=\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)$$
4	3	oveq2i	$$⊢\log 2-\sum _{n=0}^{4-1}\left(\frac{2}{3\left(2n+1\right)9^n}\right)=\log 2-\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)$$
5		4nn0	$$⊢4\in {\mathbb{N}}_0$$
6		log2tlbnd	$$⊢4\in {\mathbb{N}}_0\to \log 2-\sum _{n=0}^{4-1}\left(\frac{2}{3\left(2n+1\right)9^n}\right)\in \left[0,\frac{3}{4\left(2\cdot 4+1\right)9^4}\right]$$
7	5 6	ax-mp	$$⊢\log 2-\sum _{n=0}^{4-1}\left(\frac{2}{3\left(2n+1\right)9^n}\right)\in \left[0,\frac{3}{4\left(2\cdot 4+1\right)9^4}\right]$$
8	4 7	eqeltrri	$$⊢\log 2-\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)\in \left[0,\frac{3}{4\left(2\cdot 4+1\right)9^4}\right]$$
9		0re	$$⊢0\in ℝ$$
10		3re	$$⊢3\in ℝ$$
11		4nn	$$⊢4\in \mathbb{N}$$
12		2nn0	$$⊢2\in {\mathbb{N}}_0$$
13		1nn	$$⊢1\in \mathbb{N}$$
14	12 5 13	numnncl	$$⊢2\cdot 4+1\in \mathbb{N}$$
15	11 14	nnmulcli	$$⊢4\left(2\cdot 4+1\right)\in \mathbb{N}$$
16		9nn	$$⊢9\in \mathbb{N}$$
17		nnexpcl	$$⊢\left(9\in \mathbb{N}\wedge 4\in {\mathbb{N}}_0\right)\to 9^4\in \mathbb{N}$$
18	16 5 17	mp2an	$$⊢9^4\in \mathbb{N}$$
19	15 18	nnmulcli	$$⊢4\left(2\cdot 4+1\right)9^4\in \mathbb{N}$$
20		nndivre	$$⊢\left(3\in ℝ\wedge 4\left(2\cdot 4+1\right)9^4\in \mathbb{N}\right)\to \frac{3}{4\left(2\cdot 4+1\right)9^4}\in ℝ$$
21	10 19 20	mp2an	$$⊢\frac{3}{4\left(2\cdot 4+1\right)9^4}\in ℝ$$
22	9 21	elicc2i	$$⊢\log 2-\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)\in \left[0,\frac{3}{4\left(2\cdot 4+1\right)9^4}\right]\leftrightarrow \left(\log 2-\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)\in ℝ\wedge 0\le \log 2-\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)\wedge \log 2-\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)\le \frac{3}{4\left(2\cdot 4+1\right)9^4}\right)$$
23	8 22	mpbi	$$⊢\left(\log 2-\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)\in ℝ\wedge 0\le \log 2-\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)\wedge \log 2-\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)\le \frac{3}{4\left(2\cdot 4+1\right)9^4}\right)$$
24	23	simp3i	$$⊢\log 2-\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)\le \frac{3}{4\left(2\cdot 4+1\right)9^4}$$
25		2rp	$$⊢2\in {ℝ}^{+}$$
26		relogcl	$$⊢2\in {ℝ}^{+}\to \log 2\in ℝ$$
27	25 26	ax-mp	$$⊢\log 2\in ℝ$$
28		fzfid	$$⊢\top \to \left(0\dots 3\right)\in \mathrm{Fin}$$
29		2re	$$⊢2\in ℝ$$
30		3nn	$$⊢3\in \mathbb{N}$$
31		elfznn0	$$⊢n\in \left(0\dots 3\right)\to n\in {\mathbb{N}}_0$$
32	31	adantl	$$⊢\left(\top \wedge n\in \left(0\dots 3\right)\right)\to n\in {\mathbb{N}}_0$$
33		nn0mulcl	$$⊢\left(2\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\to 2n\in {\mathbb{N}}_0$$
34	12 32 33	sylancr	$$⊢\left(\top \wedge n\in \left(0\dots 3\right)\right)\to 2n\in {\mathbb{N}}_0$$
35		nn0p1nn	$$⊢2n\in {\mathbb{N}}_0\to 2n+1\in \mathbb{N}$$
36	34 35	syl	$$⊢\left(\top \wedge n\in \left(0\dots 3\right)\right)\to 2n+1\in \mathbb{N}$$
37		nnmulcl	$$⊢\left(3\in \mathbb{N}\wedge 2n+1\in \mathbb{N}\right)\to 3\left(2n+1\right)\in \mathbb{N}$$
38	30 36 37	sylancr	$$⊢\left(\top \wedge n\in \left(0\dots 3\right)\right)\to 3\left(2n+1\right)\in \mathbb{N}$$
39		nnexpcl	$$⊢\left(9\in \mathbb{N}\wedge n\in {\mathbb{N}}_0\right)\to 9^n\in \mathbb{N}$$
40	16 32 39	sylancr	$$⊢\left(\top \wedge n\in \left(0\dots 3\right)\right)\to 9^n\in \mathbb{N}$$
41	38 40	nnmulcld	$$⊢\left(\top \wedge n\in \left(0\dots 3\right)\right)\to 3\left(2n+1\right)9^n\in \mathbb{N}$$
42		nndivre	$$⊢\left(2\in ℝ\wedge 3\left(2n+1\right)9^n\in \mathbb{N}\right)\to \frac{2}{3\left(2n+1\right)9^n}\in ℝ$$
43	29 41 42	sylancr	$$⊢\left(\top \wedge n\in \left(0\dots 3\right)\right)\to \frac{2}{3\left(2n+1\right)9^n}\in ℝ$$
44	28 43	fsumrecl	$$⊢\top \to \sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)\in ℝ$$
45	44	mptru	$$⊢\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)\in ℝ$$
46	27 45 21	lesubadd2i	$$⊢\log 2-\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)\le \frac{3}{4\left(2\cdot 4+1\right)9^4}\leftrightarrow \log 2\le \sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)+\left(\frac{3}{4\left(2\cdot 4+1\right)9^4}\right)$$
47	24 46	mpbi	$$⊢\log 2\le \sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)+\left(\frac{3}{4\left(2\cdot 4+1\right)9^4}\right)$$
48		log2ublem3	$$⊢3^{7}5\cdot 7\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)\le 53056$$
49		3nn0	$$⊢3\in {\mathbb{N}}_0$$
50		5nn0	$$⊢5\in {\mathbb{N}}_0$$
51	50 49	deccl	$$⊢53\in {\mathbb{N}}_0$$
52		0nn0	$$⊢0\in {\mathbb{N}}_0$$
53	51 52	deccl	$$⊢530\in {\mathbb{N}}_0$$
54	53 50	deccl	$$⊢5305\in {\mathbb{N}}_0$$
55		6nn0	$$⊢6\in {\mathbb{N}}_0$$
56	54 55	deccl	$$⊢53056\in {\mathbb{N}}_0$$
57		1nn0	$$⊢1\in {\mathbb{N}}_0$$
58		eqid	$$⊢\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)+\left(\frac{3}{4\left(2\cdot 4+1\right)9^4}\right)=\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)+\left(\frac{3}{4\left(2\cdot 4+1\right)9^4}\right)$$
59		6p1e7	$$⊢6+1=7$$
60		eqid	$$⊢53056=53056$$
61	54 55 59 60	decsuc	$$⊢53056+1=53057$$
62		5nn	$$⊢5\in \mathbb{N}$$
63		7nn	$$⊢7\in \mathbb{N}$$
64	62 63	nnmulcli	$$⊢5\cdot 7\in \mathbb{N}$$
65	64	nnrei	$$⊢5\cdot 7\in ℝ$$
66	15	nnrei	$$⊢4\left(2\cdot 4+1\right)\in ℝ$$
67		6nn	$$⊢6\in \mathbb{N}$$
68		5lt6	$$⊢5<6$$
69	49 50 67 68	declt	$$⊢35<36$$
70		7cn	$$⊢7\in ℂ$$
71		5cn	$$⊢5\in ℂ$$
72		7t5e35	$$⊢7\cdot 5=35$$
73	70 71 72	mulcomli	$$⊢5\cdot 7=35$$
74		4cn	$$⊢4\in ℂ$$
75		2cn	$$⊢2\in ℂ$$
76		4t2e8	$$⊢4\cdot 2=8$$
77	74 75 76	mulcomli	$$⊢2\cdot 4=8$$
78	77	oveq1i	$$⊢2\cdot 4+1=8+1$$
79		8p1e9	$$⊢8+1=9$$
80	78 79	eqtri	$$⊢2\cdot 4+1=9$$
81	80	oveq2i	$$⊢4\left(2\cdot 4+1\right)=4\cdot 9$$
82		9cn	$$⊢9\in ℂ$$
83		9t4e36	$$⊢9\cdot 4=36$$
84	82 74 83	mulcomli	$$⊢4\cdot 9=36$$
85	81 84	eqtri	$$⊢4\left(2\cdot 4+1\right)=36$$
86	69 73 85	3brtr4i	$$⊢5\cdot 7<4\left(2\cdot 4+1\right)$$
87	65 66 86	ltleii	$$⊢5\cdot 7\le 4\left(2\cdot 4+1\right)$$
88	18	nngt0i	$$⊢0<9^4$$
89	18	nnrei	$$⊢9^4\in ℝ$$
90	65 66 89	lemul2i	$$⊢0<9^4\to \left(5\cdot 7\le 4\left(2\cdot 4+1\right)\leftrightarrow 9^{4}5\cdot 7\le 9^{4}4\left(2\cdot 4+1\right)\right)$$
91	88 90	ax-mp	$$⊢5\cdot 7\le 4\left(2\cdot 4+1\right)\leftrightarrow 9^{4}5\cdot 7\le 9^{4}4\left(2\cdot 4+1\right)$$
92	87 91	mpbi	$$⊢9^{4}5\cdot 7\le 9^{4}4\left(2\cdot 4+1\right)$$
93		7nn0	$$⊢7\in {\mathbb{N}}_0$$
94		nnexpcl	$$⊢\left(3\in \mathbb{N}\wedge 7\in {\mathbb{N}}_0\right)\to 3^7\in \mathbb{N}$$
95	30 93 94	mp2an	$$⊢3^7\in \mathbb{N}$$
96	95	nncni	$$⊢3^7\in ℂ$$
97	64	nncni	$$⊢5\cdot 7\in ℂ$$
98		3cn	$$⊢3\in ℂ$$
99	96 97 98	mul32i	$$⊢3^{7}5\cdot 7\cdot 3=3^7\cdot 35\cdot 7$$
100	74 75	mulcomi	$$⊢4\cdot 2=2\cdot 4$$
101		df-8	$$⊢8=7+1$$
102	76 100 101	3eqtr3i	$$⊢2\cdot 4=7+1$$
103	102	oveq2i	$$⊢3^{2\cdot 4}=3^{7+1}$$
104		expmul	$$⊢\left(3\in ℂ\wedge 2\in {\mathbb{N}}_0\wedge 4\in {\mathbb{N}}_0\right)\to 3^{2\cdot 4}={\left(3^2\right)}^4$$
105	98 12 5 104	mp3an	$$⊢3^{2\cdot 4}={\left(3^2\right)}^4$$
106	103 105	eqtr3i	$$⊢3^{7+1}={\left(3^2\right)}^4$$
107		expp1	$$⊢\left(3\in ℂ\wedge 7\in {\mathbb{N}}_0\right)\to 3^{7+1}=3^7\cdot 3$$
108	98 93 107	mp2an	$$⊢3^{7+1}=3^7\cdot 3$$
109		sq3	$$⊢3^2=9$$
110	109	oveq1i	$$⊢{\left(3^2\right)}^4=9^4$$
111	106 108 110	3eqtr3i	$$⊢3^7\cdot 3=9^4$$
112	111	oveq1i	$$⊢3^7\cdot 35\cdot 7=9^{4}5\cdot 7$$
113	99 112	eqtri	$$⊢3^{7}5\cdot 7\cdot 3=9^{4}5\cdot 7$$
114	15	nncni	$$⊢4\left(2\cdot 4+1\right)\in ℂ$$
115	18	nncni	$$⊢9^4\in ℂ$$
116	114 115	mulcomi	$$⊢4\left(2\cdot 4+1\right)9^4=9^{4}4\left(2\cdot 4+1\right)$$
117	116	oveq1i	$$⊢4\left(2\cdot 4+1\right)9^4\cdot 1=9^{4}4\left(2\cdot 4+1\right)\cdot 1$$
118	115 114	mulcli	$$⊢9^{4}4\left(2\cdot 4+1\right)\in ℂ$$
119	118	mulridi	$$⊢9^{4}4\left(2\cdot 4+1\right)\cdot 1=9^{4}4\left(2\cdot 4+1\right)$$
120	117 119	eqtri	$$⊢4\left(2\cdot 4+1\right)9^4\cdot 1=9^{4}4\left(2\cdot 4+1\right)$$
121	92 113 120	3brtr4i	$$⊢3^{7}5\cdot 7\cdot 3\le 4\left(2\cdot 4+1\right)9^4\cdot 1$$
122	48 45 49 19 56 57 58 61 121	log2ublem1	$$⊢3^{7}5\cdot 7\left(\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)+\left(\frac{3}{4\left(2\cdot 4+1\right)9^4}\right)\right)\le 53057$$
123	45 21	readdcli	$$⊢\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)+\left(\frac{3}{4\left(2\cdot 4+1\right)9^4}\right)\in ℝ$$
124	54 93	deccl	$$⊢53057\in {\mathbb{N}}_0$$
125	124	nn0rei	$$⊢53057\in ℝ$$
126	95 64	nnmulcli	$$⊢3^{7}5\cdot 7\in \mathbb{N}$$
127	126	nnrei	$$⊢3^{7}5\cdot 7\in ℝ$$
128	126	nngt0i	$$⊢0<3^{7}5\cdot 7$$
129	127 128	pm3.2i	$$⊢\left(3^{7}5\cdot 7\in ℝ\wedge 0<3^{7}5\cdot 7\right)$$
130		lemuldiv2	$$⊢\left(\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)+\left(\frac{3}{4\left(2\cdot 4+1\right)9^4}\right)\in ℝ\wedge 53057\in ℝ\wedge \left(3^{7}5\cdot 7\in ℝ\wedge 0<3^{7}5\cdot 7\right)\right)\to \left(3^{7}5\cdot 7\left(\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)+\left(\frac{3}{4\left(2\cdot 4+1\right)9^4}\right)\right)\le 53057\leftrightarrow \sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)+\left(\frac{3}{4\left(2\cdot 4+1\right)9^4}\right)\le \frac{53057}{3^{7}5\cdot 7}\right)$$
131	123 125 129 130	mp3an	$$⊢3^{7}5\cdot 7\left(\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)+\left(\frac{3}{4\left(2\cdot 4+1\right)9^4}\right)\right)\le 53057\leftrightarrow \sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)+\left(\frac{3}{4\left(2\cdot 4+1\right)9^4}\right)\le \frac{53057}{3^{7}5\cdot 7}$$
132	122 131	mpbi	$$⊢\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)+\left(\frac{3}{4\left(2\cdot 4+1\right)9^4}\right)\le \frac{53057}{3^{7}5\cdot 7}$$
133		8nn0	$$⊢8\in {\mathbb{N}}_0$$
134	49 133	deccl	$$⊢38\in {\mathbb{N}}_0$$
135	134 93	deccl	$$⊢387\in {\mathbb{N}}_0$$
136	135 49	deccl	$$⊢3873\in {\mathbb{N}}_0$$
137	136 57	deccl	$$⊢38731\in {\mathbb{N}}_0$$
138	137 55	deccl	$$⊢387316\in {\mathbb{N}}_0$$
139	137 93	deccl	$$⊢387317\in {\mathbb{N}}_0$$
140		1lt10	$$⊢1<10$$
141		6lt7	$$⊢6<7$$
142	137 55 63 141	declt	$$⊢387316<387317$$
143	138 139 57 93 140 142	decltc	$$⊢3873161<3873177$$
144		eqid	$$⊢73=73$$
145	57 50	deccl	$$⊢15\in {\mathbb{N}}_0$$
146		9nn0	$$⊢9\in {\mathbb{N}}_0$$
147	145 146	deccl	$$⊢159\in {\mathbb{N}}_0$$
148	147 57	deccl	$$⊢1591\in {\mathbb{N}}_0$$
149	148 93	deccl	$$⊢15917\in {\mathbb{N}}_0$$
150		eqid	$$⊢53057=53057$$
151		eqid	$$⊢15917=15917$$
152		eqid	$$⊢5305=5305$$
153		eqid	$$⊢1591=1591$$
154		ax-1cn	$$⊢1\in ℂ$$
155		5p1e6	$$⊢5+1=6$$
156	71 154 155	addcomli	$$⊢1+5=6$$
157	147 57 50 153 156	decaddi	$$⊢1591+5=1596$$
158	57 55	deccl	$$⊢16\in {\mathbb{N}}_0$$
159		eqid	$$⊢530=530$$
160		eqid	$$⊢159=159$$
161		eqid	$$⊢15=15$$
162	57 50 155 161	decsuc	$$⊢15+1=16$$
163		9p4e13	$$⊢9+4=13$$
164	145 146 5 160 162 49 163	decaddci	$$⊢159+4=163$$
165		eqid	$$⊢53=53$$
166	158	nn0cni	$$⊢16\in ℂ$$
167	166	addridi	$$⊢16+0=16$$
168		1p2e3	$$⊢1+2=3$$
169	168	oveq2i	$$⊢5\cdot 7+1+2=5\cdot 7+3$$
170		5p3e8	$$⊢5+3=8$$
171	49 50 49 73 170	decaddi	$$⊢5\cdot 7+3=38$$
172	169 171	eqtri	$$⊢5\cdot 7+1+2=38$$
173		7t3e21	$$⊢7\cdot 3=21$$
174	70 98 173	mulcomli	$$⊢3\cdot 7=21$$
175		6cn	$$⊢6\in ℂ$$
176	175 154 59	addcomli	$$⊢1+6=7$$
177	12 57 55 174 176	decaddi	$$⊢3\cdot 7+6=27$$
178	50 49 57 55 165 167 93 93 12 172 177	decmac	$$⊢53\cdot 7+16+0=387$$
179	70	mul02i	$$⊢0\cdot 7=0$$
180	179	oveq1i	$$⊢0\cdot 7+3=0+3$$
181	98	addlidi	$$⊢0+3=3$$
182	49	dec0h	$$⊢3=03$$
183	181 182	eqtri	$$⊢0+3=03$$
184	180 183	eqtri	$$⊢0\cdot 7+3=03$$
185	51 52 158 49 159 164 93 49 52 178 184	decmac	$$⊢530\cdot 7+159+4=3873$$
186		3p1e4	$$⊢3+1=4$$
187		6p5e11	$$⊢6+5=11$$
188	175 71 187	addcomli	$$⊢5+6=11$$
189	49 50 55 73 186 57 188	decaddci	$$⊢5\cdot 7+6=41$$
190	53 50 147 55 152 157 93 57 5 185 189	decmac	$$⊢5305\cdot 7+1591+5=38731$$
191		7t7e49	$$⊢7\cdot 7=49$$
192		4p1e5	$$⊢4+1=5$$
193		9p7e16	$$⊢9+7=16$$
194	5 146 93 191 192 55 193	decaddci	$$⊢7\cdot 7+7=56$$
195	54 93 148 93 150 151 93 55 50 190 194	decmac	$$⊢53057\cdot 7+15917=387316$$
196	12	dec0h	$$⊢2=02$$
197	154	addlidi	$$⊢0+1=1$$
198	57	dec0h	$$⊢1=01$$
199	197 198	eqtri	$$⊢0+1=01$$
200		00id	$$⊢0+0=0$$
201	52	dec0h	$$⊢0=00$$
202	200 201	eqtri	$$⊢0+0=00$$
203		5t3e15	$$⊢5\cdot 3=15$$
204	203	oveq1i	$$⊢5\cdot 3+0=15+0$$
205	145	nn0cni	$$⊢15\in ℂ$$
206	205	addridi	$$⊢15+0=15$$
207	204 206	eqtri	$$⊢5\cdot 3+0=15$$
208		3t3e9	$$⊢3\cdot 3=9$$
209	208	oveq1i	$$⊢3\cdot 3+0=9+0$$
210	82	addridi	$$⊢9+0=9$$
211	209 210	eqtri	$$⊢3\cdot 3+0=9$$
212	50 49 52 52 165 202 49 207 211	decma	$$⊢53\cdot 3+0+0=159$$
213	98	mul02i	$$⊢0\cdot 3=0$$
214	213	oveq1i	$$⊢0\cdot 3+1=0+1$$
215	214 199	eqtri	$$⊢0\cdot 3+1=01$$
216	51 52 52 57 159 199 49 57 52 212 215	decmac	$$⊢530\cdot 3+0+1=1591$$
217		5p2e7	$$⊢5+2=7$$
218	57 50 12 203 217	decaddi	$$⊢5\cdot 3+2=17$$
219	53 50 52 12 152 196 49 93 57 216 218	decmac	$$⊢5305\cdot 3+2=15917$$
220	49 54 93 150 57 12 219 173	decmul1c	$$⊢53057\cdot 3=159171$$
221	124 93 49 144 57 149 195 220	decmul2c	$$⊢53057\cdot 73=3873161$$
222	50 50	deccl	$$⊢55\in {\mathbb{N}}_0$$
223	222 49	deccl	$$⊢553\in {\mathbb{N}}_0$$
224	223 49	deccl	$$⊢5533\in {\mathbb{N}}_0$$
225	224 57	deccl	$$⊢55331\in {\mathbb{N}}_0$$
226	12 50	deccl	$$⊢25\in {\mathbb{N}}_0$$
227	226 49	deccl	$$⊢253\in {\mathbb{N}}_0$$
228	12 57	deccl	$$⊢21\in {\mathbb{N}}_0$$
229	228 133	deccl	$$⊢218\in {\mathbb{N}}_0$$
230	93 12	deccl	$$⊢72\in {\mathbb{N}}_0$$
231		3t2e6	$$⊢3\cdot 2=6$$
232	98 75 231	mulcomli	$$⊢2\cdot 3=6$$
233		3exp3	$$⊢3^3=27$$
234	12 93	deccl	$$⊢27\in {\mathbb{N}}_0$$
235		eqid	$$⊢27=27$$
236	57 133	deccl	$$⊢18\in {\mathbb{N}}_0$$
237		eqid	$$⊢18=18$$
238		2t2e4	$$⊢2\cdot 2=4$$
239	238 168	oveq12i	$$⊢2\cdot 2+1+2=4+3$$
240		4p3e7	$$⊢4+3=7$$
241	239 240	eqtri	$$⊢2\cdot 2+1+2=7$$
242		7t2e14	$$⊢7\cdot 2=14$$
243		1p1e2	$$⊢1+1=2$$
244		8cn	$$⊢8\in ℂ$$
245		8p4e12	$$⊢8+4=12$$
246	244 74 245	addcomli	$$⊢4+8=12$$
247	57 5 133 242 243 12 246	decaddci	$$⊢7\cdot 2+8=22$$
248	12 93 57 133 235 237 12 12 12 241 247	decmac	$$⊢27\cdot 2+18=72$$
249	70 75 242	mulcomli	$$⊢2\cdot 7=14$$
250		4p4e8	$$⊢4+4=8$$
251	57 5 5 249 250	decaddi	$$⊢2\cdot 7+4=18$$
252	93 12 93 235 146 5 251 191	decmul1c	$$⊢27\cdot 7=189$$
253	234 12 93 235 146 236 248 252	decmul2c	$$⊢27\cdot 27=729$$
254	49 49 232 233 253	numexp2x	$$⊢3^6=729$$
255		eqid	$$⊢72=72$$
256	232	oveq1i	$$⊢2\cdot 3+2=6+2$$
257		6p2e8	$$⊢6+2=8$$
258	256 257	eqtri	$$⊢2\cdot 3+2=8$$
259	93 12 12 255 49 173 258	decrmanc	$$⊢72\cdot 3+2=218$$
260		9t3e27	$$⊢9\cdot 3=27$$
261	49 230 146 254 93 12 259 260	decmul1c	$$⊢3^6\cdot 3=2187$$
262	49 55 59 261	numexpp1	$$⊢3^7=2187$$
263	57 93	deccl	$$⊢17\in {\mathbb{N}}_0$$
264	263 93	deccl	$$⊢177\in {\mathbb{N}}_0$$
265		eqid	$$⊢218=218$$
266		eqid	$$⊢177=177$$
267	12 52	deccl	$$⊢20\in {\mathbb{N}}_0$$
268	267 49	deccl	$$⊢203\in {\mathbb{N}}_0$$
269	12 12	deccl	$$⊢22\in {\mathbb{N}}_0$$
270		eqid	$$⊢21=21$$
271		eqid	$$⊢17=17$$
272		eqid	$$⊢203=203$$
273		eqid	$$⊢20=20$$
274	75	addlidi	$$⊢0+2=2$$
275	154	addridi	$$⊢1+0=1$$
276	52 57 12 52 198 273 274 275	decadd	$$⊢1+20=21$$
277	12 57 243 276	decsuc	$$⊢1+20+1=22$$
278		7p3e10	$$⊢7+3=10$$
279	57 93 267 49 271 272 277 278	decaddc2	$$⊢17+203=220$$
280		eqid	$$⊢253=253$$
281		eqid	$$⊢22=22$$
282		eqid	$$⊢25=25$$
283		2p2e4	$$⊢2+2=4$$
284	71 75 217	addcomli	$$⊢2+5=7$$
285	12 12 12 50 281 282 283 284	decadd	$$⊢22+25=47$$
286	50	dec0h	$$⊢5=05$$
287	192 286	eqtri	$$⊢4+1=05$$
288	238 197	oveq12i	$$⊢2\cdot 2+0+1=4+1$$
289	288 192	eqtri	$$⊢2\cdot 2+0+1=5$$
290		5t2e10	$$⊢5\cdot 2=10$$
291	71	addlidi	$$⊢0+5=5$$
292	57 52 50 290 291	decaddi	$$⊢5\cdot 2+5=15$$
293	12 50 52 50 282 287 12 50 57 289 292	decmac	$$⊢25\cdot 2+4+1=55$$
294	231	oveq1i	$$⊢3\cdot 2+7=6+7$$
295		7p6e13	$$⊢7+6=13$$
296	70 175 295	addcomli	$$⊢6+7=13$$
297	294 296	eqtri	$$⊢3\cdot 2+7=13$$
298	226 49 5 93 280 285 12 49 57 293 297	decmac	$$⊢253\cdot 2+22+25=553$$
299	227	nn0cni	$$⊢253\in ℂ$$
300	299	mulridi	$$⊢253\cdot 1=253$$
301	300	oveq1i	$$⊢253\cdot 1+0=253+0$$
302	299	addridi	$$⊢253+0=253$$
303	301 302	eqtri	$$⊢253\cdot 1+0=253$$
304	12 57 269 52 270 279 227 49 226 298 303	decma2c	$$⊢253\cdot 21+17+203=5533$$
305	93	dec0h	$$⊢7=07$$
306	74	addlidi	$$⊢0+4=4$$
307	306	oveq2i	$$⊢2\cdot 8+0+4=2\cdot 8+4$$
308		8t2e16	$$⊢8\cdot 2=16$$
309	244 75 308	mulcomli	$$⊢2\cdot 8=16$$
310		6p4e10	$$⊢6+4=10$$
311	57 55 5 309 243 310	decaddci2	$$⊢2\cdot 8+4=20$$
312	307 311	eqtri	$$⊢2\cdot 8+0+4=20$$
313		8t5e40	$$⊢8\cdot 5=40$$
314	244 71 313	mulcomli	$$⊢5\cdot 8=40$$
315	5 52 49 314 181	decaddi	$$⊢5\cdot 8+3=43$$
316	12 50 52 49 282 183 133 49 5 312 315	decmac	$$⊢25\cdot 8+0+3=203$$
317		8t3e24	$$⊢8\cdot 3=24$$
318	244 98 317	mulcomli	$$⊢3\cdot 8=24$$
319		2p1e3	$$⊢2+1=3$$
320		7p4e11	$$⊢7+4=11$$
321	70 74 320	addcomli	$$⊢4+7=11$$
322	12 5 93 318 319 57 321	decaddci	$$⊢3\cdot 8+7=31$$
323	226 49 52 93 280 305 133 57 49 316 322	decmac	$$⊢253\cdot 8+7=2031$$
324	228 133 263 93 265 266 227 57 268 304 323	decma2c	$$⊢253\cdot 218+177=55331$$
325	57 5 49 249 240	decaddi	$$⊢2\cdot 7+3=17$$
326	49 50 12 73 217	decaddi	$$⊢5\cdot 7+2=37$$
327	12 50 12 282 93 93 49 325 326	decrmac	$$⊢25\cdot 7+2=177$$
328	93 226 49 280 57 12 327 174	decmul1c	$$⊢253\cdot 7=1771$$
329	227 229 93 262 57 264 324 328	decmul2c	$$⊢2533^7=553311$$
330		eqid	$$⊢55331=55331$$
331		eqid	$$⊢5533=5533$$
332		eqid	$$⊢553=553$$
333		eqid	$$⊢55=55$$
334	274 196	eqtri	$$⊢0+2=02$$
335	181	oveq2i	$$⊢5\cdot 7+0+3=5\cdot 7+3$$
336	335 171	eqtri	$$⊢5\cdot 7+0+3=38$$
337	50 50 52 12 333 334 93 93 49 336 326	decmac	$$⊢55\cdot 7+0+2=387$$
338	12 57 12 174 168	decaddi	$$⊢3\cdot 7+2=23$$
339	222 49 52 12 332 196 93 49 12 337 338	decmac	$$⊢553\cdot 7+2=3873$$
340	93 223 49 331 57 12 339 174	decmul1c	$$⊢5533\cdot 7=38731$$
341	70	mullidi	$$⊢1\cdot 7=7$$
342	93 224 57 330 340 341	decmul1	$$⊢55331\cdot 7=387317$$
343	93 225 57 329 342 341	decmul1	$$⊢2533^7\cdot 7=3873177$$
344	143 221 343	3brtr4i	$$⊢53057\cdot 73<2533^7\cdot 7$$
345	93 49	deccl	$$⊢73\in {\mathbb{N}}_0$$
346	124 345	nn0mulcli	$$⊢53057\cdot 73\in {\mathbb{N}}_0$$
347	346	nn0rei	$$⊢53057\cdot 73\in ℝ$$
348	49 93	nn0expcli	$$⊢3^7\in {\mathbb{N}}_0$$
349	227 348	nn0mulcli	$$⊢2533^7\in {\mathbb{N}}_0$$
350	349 93	nn0mulcli	$$⊢2533^7\cdot 7\in {\mathbb{N}}_0$$
351	350	nn0rei	$$⊢2533^7\cdot 7\in ℝ$$
352	62	nnrei	$$⊢5\in ℝ$$
353	62	nngt0i	$$⊢0<5$$
354	347 351 352 353	ltmul1ii	$$⊢53057\cdot 73<2533^7\cdot 7\leftrightarrow 53057\cdot 73\cdot 5<2533^7\cdot 7\cdot 5$$
355	344 354	mpbi	$$⊢53057\cdot 73\cdot 5<2533^7\cdot 7\cdot 5$$
356	124	nn0cni	$$⊢53057\in ℂ$$
357	345	nn0cni	$$⊢73\in ℂ$$
358	356 357 71	mulassi	$$⊢53057\cdot 73\cdot 5=5305773\cdot 5$$
359	49 50 155 72	decsuc	$$⊢7\cdot 5+1=36$$
360	71 98 203	mulcomli	$$⊢3\cdot 5=15$$
361	50 93 49 144 50 57 359 360	decmul1c	$$⊢73\cdot 5=365$$
362	361	oveq2i	$$⊢5305773\cdot 5=53057\cdot 365$$
363	358 362	eqtri	$$⊢53057\cdot 73\cdot 5=53057\cdot 365$$
364	299 96	mulcli	$$⊢2533^7\in ℂ$$
365	364 70 71	mulassi	$$⊢2533^7\cdot 7\cdot 5=2533^{7}7\cdot 5$$
366	70 71	mulcomi	$$⊢7\cdot 5=5\cdot 7$$
367	366	oveq2i	$$⊢2533^{7}7\cdot 5=2533^{7}5\cdot 7$$
368	299 96 97	mulassi	$$⊢2533^{7}5\cdot 7=2533^{7}5\cdot 7$$
369	367 368	eqtri	$$⊢2533^{7}7\cdot 5=2533^{7}5\cdot 7$$
370	365 369	eqtri	$$⊢2533^7\cdot 7\cdot 5=2533^{7}5\cdot 7$$
371	355 363 370	3brtr3i	$$⊢53057\cdot 365<2533^{7}5\cdot 7$$
372	49 55	deccl	$$⊢36\in {\mathbb{N}}_0$$
373	372 62	decnncl	$$⊢365\in \mathbb{N}$$
374	373	nnrei	$$⊢365\in ℝ$$
375	373	nngt0i	$$⊢0<365$$
376	374 375	pm3.2i	$$⊢\left(365\in ℝ\wedge 0<365\right)$$
377	227	nn0rei	$$⊢253\in ℝ$$
378		lt2mul2div	$$⊢\left(\left(53057\in ℝ\wedge \left(365\in ℝ\wedge 0<365\right)\right)\wedge \left(253\in ℝ\wedge \left(3^{7}5\cdot 7\in ℝ\wedge 0<3^{7}5\cdot 7\right)\right)\right)\to \left(53057\cdot 365<2533^{7}5\cdot 7\leftrightarrow \frac{53057}{3^{7}5\cdot 7}<\frac{253}{365}\right)$$
379	125 376 377 129 378	mp4an	$$⊢53057\cdot 365<2533^{7}5\cdot 7\leftrightarrow \frac{53057}{3^{7}5\cdot 7}<\frac{253}{365}$$
380	371 379	mpbi	$$⊢\frac{53057}{3^{7}5\cdot 7}<\frac{253}{365}$$
381		nndivre	$$⊢\left(53057\in ℝ\wedge 3^{7}5\cdot 7\in \mathbb{N}\right)\to \frac{53057}{3^{7}5\cdot 7}\in ℝ$$
382	125 126 381	mp2an	$$⊢\frac{53057}{3^{7}5\cdot 7}\in ℝ$$
383		nndivre	$$⊢\left(253\in ℝ\wedge 365\in \mathbb{N}\right)\to \frac{253}{365}\in ℝ$$
384	377 373 383	mp2an	$$⊢\frac{253}{365}\in ℝ$$
385	123 382 384	lelttri	$$⊢\left(\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)+\left(\frac{3}{4\left(2\cdot 4+1\right)9^4}\right)\le \frac{53057}{3^{7}5\cdot 7}\wedge \frac{53057}{3^{7}5\cdot 7}<\frac{253}{365}\right)\to \sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)+\left(\frac{3}{4\left(2\cdot 4+1\right)9^4}\right)<\frac{253}{365}$$
386	132 380 385	mp2an	$$⊢\sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)+\left(\frac{3}{4\left(2\cdot 4+1\right)9^4}\right)<\frac{253}{365}$$
387	27 123 384	lelttri	$$⊢\left(\log 2\le \sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)+\left(\frac{3}{4\left(2\cdot 4+1\right)9^4}\right)\wedge \sum _{n=0}^3\left(\frac{2}{3\left(2n+1\right)9^n}\right)+\left(\frac{3}{4\left(2\cdot 4+1\right)9^4}\right)<\frac{253}{365}\right)\to \log 2<\frac{253}{365}$$
388	47 386 387	mp2an	$$⊢\log 2<\frac{253}{365}$$