Metamath Proof Explorer


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 7 n = 0 3 2 3 2 n + 1 9 n 53056

Proof

Step Hyp Ref Expression
1 0le0 0 0
2 risefall0lem 0 0 1 =
3 2 sumeq1i n = 0 0 1 2 3 2 n + 1 9 n = n 2 3 2 n + 1 9 n
4 sum0 n 2 3 2 n + 1 9 n = 0
5 3 4 eqtri n = 0 0 1 2 3 2 n + 1 9 n = 0
6 5 oveq2i 3 7 5 7 n = 0 0 1 2 3 2 n + 1 9 n = 3 7 5 7 0
7 3cn 3
8 7nn0 7 0
9 expcl 3 7 0 3 7
10 7 8 9 mp2an 3 7
11 5cn 5
12 7cn 7
13 11 12 mulcli 5 7
14 10 13 mulcli 3 7 5 7
15 14 mul01i 3 7 5 7 0 = 0
16 6 15 eqtri 3 7 5 7 n = 0 0 1 2 3 2 n + 1 9 n = 0
17 2cn 2
18 17 mul01i 2 0 = 0
19 1 16 18 3brtr4i 3 7 5 7 n = 0 0 1 2 3 2 n + 1 9 n 2 0
20 0nn0 0 0
21 2nn0 2 0
22 5nn0 5 0
23 21 22 deccl 25 0
24 23 22 deccl 255 0
25 1nn0 1 0
26 24 25 deccl 2551 0
27 26 22 deccl 25515 0
28 eqid 0 1 = 0 1
29 27 nn0cni 25515
30 29 addid2i 0 + 25515 = 25515
31 3nn0 3 0
32 7 addid1i 3 + 0 = 3
33 29 mulid2i 1 25515 = 25515
34 18 oveq1i 2 0 + 1 = 0 + 1
35 0p1e1 0 + 1 = 1
36 34 35 eqtri 2 0 + 1 = 1
37 36 oveq1i 2 0 + 1 25515 = 1 25515
38 22 8 nn0mulcli 5 7 0
39 8 21 deccl 72 0
40 9nn0 9 0
41 2p1e3 2 + 1 = 3
42 8nn0 8 0
43 1p1e2 1 + 1 = 2
44 9cn 9
45 exp1 9 9 1 = 9
46 44 45 ax-mp 9 1 = 9
47 46 oveq1i 9 1 9 = 9 9
48 9t9e81 9 9 = 81
49 47 48 eqtri 9 1 9 = 81
50 40 25 43 49 numexpp1 9 2 = 81
51 8cn 8
52 9t8e72 9 8 = 72
53 44 51 52 mulcomli 8 9 = 72
54 44 mulid2i 1 9 = 9
55 40 42 25 50 53 54 decmul1 9 2 9 = 729
56 40 21 41 55 numexpp1 9 3 = 729
57 31 25 deccl 31 0
58 eqid 72 = 72
59 eqid 31 = 31
60 7t5e35 7 5 = 35
61 12 11 60 mulcomli 5 7 = 35
62 7p3e10 7 + 3 = 10
63 12 7 62 addcomli 3 + 7 = 10
64 ax-1cn 1
65 3p1e4 3 + 1 = 4
66 7 64 65 addcomli 1 + 3 = 4
67 66 oveq2i 3 7 + 1 + 3 = 3 7 + 4
68 4nn0 4 0
69 7t3e21 7 3 = 21
70 12 7 69 mulcomli 3 7 = 21
71 4cn 4
72 4p1e5 4 + 1 = 5
73 71 64 72 addcomli 1 + 4 = 5
74 21 25 68 70 73 decaddi 3 7 + 4 = 25
75 67 74 eqtri 3 7 + 1 + 3 = 25
76 61 oveq1i 5 7 + 0 = 35 + 0
77 31 22 deccl 35 0
78 77 nn0cni 35
79 78 addid1i 35 + 0 = 35
80 76 79 eqtri 5 7 + 0 = 35
81 31 22 25 20 61 63 8 22 31 75 80 decmac 5 7 7 + 3 + 7 = 255
82 25 dec0h 1 = 01
83 3t2e6 3 2 = 6
84 83 35 oveq12i 3 2 + 0 + 1 = 6 + 1
85 6p1e7 6 + 1 = 7
86 84 85 eqtri 3 2 + 0 + 1 = 7
87 5t2e10 5 2 = 10
88 25 20 35 87 decsuc 5 2 + 1 = 11
89 31 22 20 25 61 82 21 25 25 86 88 decmac 5 7 2 + 1 = 71
90 8 21 31 25 58 59 38 25 8 81 89 decma2c 5 7 72 + 31 = 2551
91 9t3e27 9 3 = 27
92 44 7 91 mulcomli 3 9 = 27
93 7p4e11 7 + 4 = 11
94 21 8 68 92 41 25 93 decaddci 3 9 + 4 = 31
95 9t5e45 9 5 = 45
96 44 11 95 mulcomli 5 9 = 45
97 40 31 22 61 22 68 94 96 decmul1c 5 7 9 = 315
98 38 39 40 56 22 57 90 97 decmul2c 5 7 9 3 = 25515
99 33 37 98 3eqtr4ri 5 7 9 3 = 2 0 + 1 25515
100 19 20 27 20 28 30 31 32 99 log2ublem2 3 7 5 7 n = 0 0 2 3 2 n + 1 9 n 2 25515
101 40 68 deccl 94 0
102 101 22 deccl 945 0
103 1m1e0 1 1 = 0
104 eqid 25515 = 25515
105 eqid 945 = 945
106 6nn0 6 0
107 21 106 deccl 26 0
108 107 68 deccl 264 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 9
123 3t3e9 3 3 = 9
124 123 oveq1i 3 3 9 = 9 9
125 7 7 44 mulassi 3 3 9 = 3 3 9
126 122 124 125 3eqtr2i 9 2 = 3 3 9
127 126 oveq2i 5 7 9 2 = 5 7 3 3 9
128 7 44 mulcli 3 9
129 13 7 128 mul12i 5 7 3 3 9 = 3 5 7 3 9
130 21 68 deccl 24 0
131 eqid 24 = 24
132 83 41 oveq12i 3 2 + 2 + 1 = 6 + 3
133 6p3e9 6 + 3 = 9
134 132 133 eqtri 3 2 + 2 + 1 = 9
135 71 addid2i 0 + 4 = 4
136 25 20 68 87 135 decaddi 5 2 + 4 = 14
137 31 22 21 68 61 131 21 68 25 134 136 decmac 5 7 2 + 24 = 94
138 21 25 31 70 66 decaddi 3 7 + 3 = 24
139 8 31 22 61 22 31 138 61 decmul1c 5 7 7 = 245
140 38 21 8 92 22 130 137 139 decmul2c 5 7 3 9 = 945
141 140 oveq2i 3 5 7 3 9 = 3 945
142 129 141 eqtri 5 7 3 3 9 = 3 945
143 df-3 3 = 2 + 1
144 17 mulid1i 2 1 = 2
145 144 oveq1i 2 1 + 1 = 2 + 1
146 143 145 eqtr4i 3 = 2 1 + 1
147 146 oveq1i 3 945 = 2 1 + 1 945
148 127 142 147 3eqtri 5 7 9 2 = 2 1 + 1 945
149 100 27 102 25 103 121 21 41 148 log2ublem2 3 7 5 7 n = 0 1 2 3 2 n + 1 9 n 2 26460
150 108 106 deccl 2646 0
151 150 20 deccl 26460 0
152 106 31 deccl 63 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 addid2i 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 7 9 1 = 5 7 9
165 11 12 44 mulassi 5 7 9 = 5 7 9
166 9t7e63 9 7 = 63
167 44 12 166 mulcomli 7 9 = 63
168 167 oveq2i 5 7 9 = 5 63
169 165 168 eqtri 5 7 9 = 5 63
170 df-5 5 = 4 + 1
171 2t2e4 2 2 = 4
172 171 oveq1i 2 2 + 1 = 4 + 1
173 170 172 eqtr4i 5 = 2 2 + 1
174 173 oveq1i 5 63 = 2 2 + 1 63
175 164 169 174 3eqtri 5 7 9 1 = 2 2 + 1 63
176 149 151 152 21 153 162 25 163 175 log2ublem2 3 7 5 7 n = 0 2 2 3 2 n + 1 9 n 2 26523
177 107 22 deccl 265 0
178 177 21 deccl 2652 0
179 178 31 deccl 26523 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 5
186 185 mulid1i 7 5 1 = 7 5
187 11 12 mulcomi 5 7 = 7 5
188 exp0 9 9 0 = 1
189 44 188 ax-mp 9 0 = 1
190 187 189 oveq12i 5 7 9 0 = 7 5 1
191 7 17 83 mulcomli 2 3 = 6
192 191 oveq1i 2 3 + 1 = 6 + 1
193 df-7 7 = 6 + 1
194 192 193 eqtr4i 2 3 + 1 = 7
195 194 oveq1i 2 3 + 1 5 = 7 5
196 186 190 195 3eqtr4i 5 7 9 0 = 2 3 + 1 5
197 176 179 22 31 180 184 20 161 196 log2ublem2 3 7 5 7 n = 0 3 2 3 2 n + 1 9 n 2 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 2 + 0 + 1 = 4 + 1
207 206 72 eqtri 2 2 + 0 + 1 = 5
208 6cn 6
209 6t2e12 6 2 = 12
210 208 17 209 mulcomli 2 6 = 12
211 25 21 41 210 decsuc 2 6 + 1 = 13
212 21 106 20 25 204 205 21 31 25 207 211 decma2c 2 26 + 0 + 1 = 53
213 11 17 87 mulcomli 2 5 = 10
214 213 oveq1i 2 5 + 0 = 10 + 0
215 dec10p 10 + 0 = 10
216 214 215 eqtri 2 5 + 0 = 10
217 107 22 20 20 200 203 21 20 25 212 216 decma2c 2 265 + 0 + 0 = 530
218 22 dec0h 5 = 05
219 172 72 218 3eqtri 2 2 + 1 = 05
220 177 21 20 25 199 82 21 22 20 217 219 decma2c 2 2652 + 1 = 5305
221 8t2e16 8 2 = 16
222 51 17 221 mulcomli 2 8 = 16
223 21 178 42 198 106 25 220 222 decmul2c 2 26528 = 53056
224 197 223 breqtri 3 7 5 7 n = 0 3 2 3 2 n + 1 9 n 53056