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 ) x. ( 5 x. 7 ) ) x. sum_ n e. ( 0 ... 3 ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) ) <_ ; ; ; ; 5 3 0 5 6

Proof

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