Metamath Proof Explorer


Theorem log2cnv

Description: Using the Taylor series for arctan ( _i / 3 ) , produce a rapidly convergent series for log 2 . (Contributed by Mario Carneiro, 7-Apr-2015)

Ref Expression
Hypothesis log2cnv.1 F = n 0 2 3 2 n + 1 9 n
Assertion log2cnv seq 0 + F log 2

Proof

Step Hyp Ref Expression
1 log2cnv.1 F = n 0 2 3 2 n + 1 9 n
2 nn0uz 0 = 0
3 0zd 0
4 2cn 2
5 ax-icn i
6 ine0 i 0
7 4 5 6 divcli 2 i
8 7 a1i 2 i
9 3cn 3
10 3ne0 3 0
11 5 9 10 divcli i 3
12 absdiv i 3 3 0 i 3 = i 3
13 5 9 10 12 mp3an i 3 = i 3
14 absi i = 1
15 3re 3
16 0re 0
17 3pos 0 < 3
18 16 15 17 ltleii 0 3
19 absid 3 0 3 3 = 3
20 15 18 19 mp2an 3 = 3
21 14 20 oveq12i i 3 = 1 3
22 13 21 eqtri i 3 = 1 3
23 1lt3 1 < 3
24 recgt1 3 0 < 3 1 < 3 1 3 < 1
25 15 17 24 mp2an 1 < 3 1 3 < 1
26 23 25 mpbi 1 3 < 1
27 22 26 eqbrtri i 3 < 1
28 eqid n 0 1 n i 3 2 n + 1 2 n + 1 = n 0 1 n i 3 2 n + 1 2 n + 1
29 28 atantayl3 i 3 i 3 < 1 seq 0 + n 0 1 n i 3 2 n + 1 2 n + 1 arctan i 3
30 11 27 29 mp2an seq 0 + n 0 1 n i 3 2 n + 1 2 n + 1 arctan i 3
31 30 a1i seq 0 + n 0 1 n i 3 2 n + 1 2 n + 1 arctan i 3
32 oveq2 n = k 1 n = 1 k
33 oveq2 n = k 2 n = 2 k
34 33 oveq1d n = k 2 n + 1 = 2 k + 1
35 34 oveq2d n = k i 3 2 n + 1 = i 3 2 k + 1
36 35 34 oveq12d n = k i 3 2 n + 1 2 n + 1 = i 3 2 k + 1 2 k + 1
37 32 36 oveq12d n = k 1 n i 3 2 n + 1 2 n + 1 = 1 k i 3 2 k + 1 2 k + 1
38 ovex 1 k i 3 2 k + 1 2 k + 1 V
39 37 28 38 fvmpt k 0 n 0 1 n i 3 2 n + 1 2 n + 1 k = 1 k i 3 2 k + 1 2 k + 1
40 5 a1i k 0 i
41 9 a1i k 0 3
42 10 a1i k 0 3 0
43 2nn0 2 0
44 nn0mulcl 2 0 k 0 2 k 0
45 43 44 mpan k 0 2 k 0
46 peano2nn0 2 k 0 2 k + 1 0
47 45 46 syl k 0 2 k + 1 0
48 40 41 42 47 expdivd k 0 i 3 2 k + 1 = i 2 k + 1 3 2 k + 1
49 48 oveq2d k 0 1 k i 3 2 k + 1 = 1 k i 2 k + 1 3 2 k + 1
50 neg1cn 1
51 expcl 1 k 0 1 k
52 50 51 mpan k 0 1 k
53 expcl i 2 k + 1 0 i 2 k + 1
54 5 47 53 sylancr k 0 i 2 k + 1
55 3nn 3
56 nnexpcl 3 2 k + 1 0 3 2 k + 1
57 55 47 56 sylancr k 0 3 2 k + 1
58 57 nncnd k 0 3 2 k + 1
59 57 nnne0d k 0 3 2 k + 1 0
60 52 54 58 59 divassd k 0 1 k i 2 k + 1 3 2 k + 1 = 1 k i 2 k + 1 3 2 k + 1
61 expp1 i 2 k 0 i 2 k + 1 = i 2 k i
62 5 45 61 sylancr k 0 i 2 k + 1 = i 2 k i
63 expmul i 2 0 k 0 i 2 k = i 2 k
64 5 43 63 mp3an12 k 0 i 2 k = i 2 k
65 i2 i 2 = 1
66 65 oveq1i i 2 k = 1 k
67 64 66 eqtrdi k 0 i 2 k = 1 k
68 67 oveq1d k 0 i 2 k i = 1 k i
69 62 68 eqtrd k 0 i 2 k + 1 = 1 k i
70 69 oveq2d k 0 1 k i 2 k + 1 = 1 k 1 k i
71 52 52 40 mulassd k 0 1 k 1 k i = 1 k 1 k i
72 50 a1i k 0 1
73 id k 0 k 0
74 72 73 73 expaddd k 0 1 k + k = 1 k 1 k
75 expmul 1 2 0 k 0 1 2 k = -1 2 k
76 50 43 75 mp3an12 k 0 1 2 k = -1 2 k
77 neg1sqe1 1 2 = 1
78 77 oveq1i -1 2 k = 1 k
79 76 78 eqtrdi k 0 1 2 k = 1 k
80 nn0cn k 0 k
81 80 2timesd k 0 2 k = k + k
82 81 oveq2d k 0 1 2 k = 1 k + k
83 nn0z k 0 k
84 1exp k 1 k = 1
85 83 84 syl k 0 1 k = 1
86 79 82 85 3eqtr3d k 0 1 k + k = 1
87 74 86 eqtr3d k 0 1 k 1 k = 1
88 87 oveq1d k 0 1 k 1 k i = 1 i
89 5 mulid2i 1 i = i
90 88 89 eqtrdi k 0 1 k 1 k i = i
91 70 71 90 3eqtr2d k 0 1 k i 2 k + 1 = i
92 91 oveq1d k 0 1 k i 2 k + 1 3 2 k + 1 = i 3 2 k + 1
93 49 60 92 3eqtr2d k 0 1 k i 3 2 k + 1 = i 3 2 k + 1
94 93 oveq1d k 0 1 k i 3 2 k + 1 2 k + 1 = i 3 2 k + 1 2 k + 1
95 expcl i 3 2 k + 1 0 i 3 2 k + 1
96 11 47 95 sylancr k 0 i 3 2 k + 1
97 nn0p1nn 2 k 0 2 k + 1
98 45 97 syl k 0 2 k + 1
99 98 nncnd k 0 2 k + 1
100 98 nnne0d k 0 2 k + 1 0
101 52 96 99 100 divassd k 0 1 k i 3 2 k + 1 2 k + 1 = 1 k i 3 2 k + 1 2 k + 1
102 40 58 99 59 100 divdiv1d k 0 i 3 2 k + 1 2 k + 1 = i 3 2 k + 1 2 k + 1
103 94 101 102 3eqtr3d k 0 1 k i 3 2 k + 1 2 k + 1 = i 3 2 k + 1 2 k + 1
104 58 99 mulcomd k 0 3 2 k + 1 2 k + 1 = 2 k + 1 3 2 k + 1
105 104 oveq2d k 0 i 3 2 k + 1 2 k + 1 = i 2 k + 1 3 2 k + 1
106 39 103 105 3eqtrd k 0 n 0 1 n i 3 2 n + 1 2 n + 1 k = i 2 k + 1 3 2 k + 1
107 98 57 nnmulcld k 0 2 k + 1 3 2 k + 1
108 107 nncnd k 0 2 k + 1 3 2 k + 1
109 107 nnne0d k 0 2 k + 1 3 2 k + 1 0
110 40 108 109 divcld k 0 i 2 k + 1 3 2 k + 1
111 106 110 eqeltrd k 0 n 0 1 n i 3 2 n + 1 2 n + 1 k
112 111 adantl k 0 n 0 1 n i 3 2 n + 1 2 n + 1 k
113 34 oveq2d n = k 3 2 n + 1 = 3 2 k + 1
114 oveq2 n = k 9 n = 9 k
115 113 114 oveq12d n = k 3 2 n + 1 9 n = 3 2 k + 1 9 k
116 115 oveq2d n = k 2 3 2 n + 1 9 n = 2 3 2 k + 1 9 k
117 ovex 2 3 2 k + 1 9 k V
118 116 1 117 fvmpt k 0 F k = 2 3 2 k + 1 9 k
119 expp1 3 2 k 0 3 2 k + 1 = 3 2 k 3
120 9 45 119 sylancr k 0 3 2 k + 1 = 3 2 k 3
121 expmul 3 2 0 k 0 3 2 k = 3 2 k
122 9 43 121 mp3an12 k 0 3 2 k = 3 2 k
123 sq3 3 2 = 9
124 123 oveq1i 3 2 k = 9 k
125 122 124 eqtrdi k 0 3 2 k = 9 k
126 125 oveq1d k 0 3 2 k 3 = 9 k 3
127 9nn 9
128 nnexpcl 9 k 0 9 k
129 127 128 mpan k 0 9 k
130 129 nncnd k 0 9 k
131 mulcom 9 k 3 9 k 3 = 3 9 k
132 130 9 131 sylancl k 0 9 k 3 = 3 9 k
133 120 126 132 3eqtrd k 0 3 2 k + 1 = 3 9 k
134 91 133 oveq12d k 0 1 k i 2 k + 1 3 2 k + 1 = i 3 9 k
135 49 60 134 3eqtr2d k 0 1 k i 3 2 k + 1 = i 3 9 k
136 135 oveq1d k 0 1 k i 3 2 k + 1 2 k + 1 = i 3 9 k 2 k + 1
137 nnmulcl 3 9 k 3 9 k
138 55 129 137 sylancr k 0 3 9 k
139 138 nncnd k 0 3 9 k
140 138 nnne0d k 0 3 9 k 0
141 40 139 99 140 100 divdiv1d k 0 i 3 9 k 2 k + 1 = i 3 9 k 2 k + 1
142 136 101 141 3eqtr3d k 0 1 k i 3 2 k + 1 2 k + 1 = i 3 9 k 2 k + 1
143 41 130 99 mul32d k 0 3 9 k 2 k + 1 = 3 2 k + 1 9 k
144 143 oveq2d k 0 i 3 9 k 2 k + 1 = i 3 2 k + 1 9 k
145 39 142 144 3eqtrd k 0 n 0 1 n i 3 2 n + 1 2 n + 1 k = i 3 2 k + 1 9 k
146 145 oveq2d k 0 2 i n 0 1 n i 3 2 n + 1 2 n + 1 k = 2 i i 3 2 k + 1 9 k
147 nnmulcl 3 2 k + 1 3 2 k + 1
148 55 98 147 sylancr k 0 3 2 k + 1
149 148 129 nnmulcld k 0 3 2 k + 1 9 k
150 149 nncnd k 0 3 2 k + 1 9 k
151 149 nnne0d k 0 3 2 k + 1 9 k 0
152 40 150 151 divcld k 0 i 3 2 k + 1 9 k
153 mulcom i 3 2 k + 1 9 k 2 i i 3 2 k + 1 9 k 2 i = 2 i i 3 2 k + 1 9 k
154 152 7 153 sylancl k 0 i 3 2 k + 1 9 k 2 i = 2 i i 3 2 k + 1 9 k
155 4 a1i k 0 2
156 6 a1i k 0 i 0
157 155 40 150 156 151 dmdcand k 0 i 3 2 k + 1 9 k 2 i = 2 3 2 k + 1 9 k
158 146 154 157 3eqtr2d k 0 2 i n 0 1 n i 3 2 n + 1 2 n + 1 k = 2 3 2 k + 1 9 k
159 118 158 eqtr4d k 0 F k = 2 i n 0 1 n i 3 2 n + 1 2 n + 1 k
160 159 adantl k 0 F k = 2 i n 0 1 n i 3 2 n + 1 2 n + 1 k
161 2 3 8 31 112 160 isermulc2 seq 0 + F 2 i arctan i 3
162 161 mptru seq 0 + F 2 i arctan i 3
163 bndatandm i 3 i 3 < 1 i 3 dom arctan
164 11 27 163 mp2an i 3 dom arctan
165 atanval i 3 dom arctan arctan i 3 = i 2 log 1 i i 3 log 1 + i i 3
166 164 165 ax-mp arctan i 3 = i 2 log 1 i i 3 log 1 + i i 3
167 df-4 4 = 3 + 1
168 167 oveq1i 4 3 = 3 + 1 3
169 ax-1cn 1
170 9 169 9 10 divdiri 3 + 1 3 = 3 3 + 1 3
171 9 10 dividi 3 3 = 1
172 171 oveq1i 3 3 + 1 3 = 1 + 1 3
173 168 170 172 3eqtri 4 3 = 1 + 1 3
174 169 9 10 divcli 1 3
175 169 174 subnegi 1 1 3 = 1 + 1 3
176 divneg 1 3 3 0 1 3 = 1 3
177 169 9 10 176 mp3an 1 3 = 1 3
178 ixi i i = 1
179 178 oveq1i i i 3 = 1 3
180 5 5 9 10 divassi i i 3 = i i 3
181 177 179 180 3eqtr2i 1 3 = i i 3
182 181 oveq2i 1 1 3 = 1 i i 3
183 173 175 182 3eqtr2ri 1 i i 3 = 4 3
184 183 fveq2i log 1 i i 3 = log 4 3
185 9 10 pm3.2i 3 3 0
186 divsubdir 3 1 3 3 0 3 1 3 = 3 3 1 3
187 9 169 185 186 mp3an 3 1 3 = 3 3 1 3
188 3m1e2 3 1 = 2
189 188 oveq1i 3 1 3 = 2 3
190 171 oveq1i 3 3 1 3 = 1 1 3
191 187 189 190 3eqtr3i 2 3 = 1 1 3
192 169 174 negsubi 1 + 1 3 = 1 1 3
193 181 oveq2i 1 + 1 3 = 1 + i i 3
194 191 192 193 3eqtr2ri 1 + i i 3 = 2 3
195 194 fveq2i log 1 + i i 3 = log 2 3
196 184 195 oveq12i log 1 i i 3 log 1 + i i 3 = log 4 3 log 2 3
197 4re 4
198 4pos 0 < 4
199 197 198 elrpii 4 +
200 3rp 3 +
201 rpdivcl 4 + 3 + 4 3 +
202 199 200 201 mp2an 4 3 +
203 2rp 2 +
204 rpdivcl 2 + 3 + 2 3 +
205 203 200 204 mp2an 2 3 +
206 relogdiv 4 3 + 2 3 + log 4 3 2 3 = log 4 3 log 2 3
207 202 205 206 mp2an log 4 3 2 3 = log 4 3 log 2 3
208 4cn 4
209 2cnne0 2 2 0
210 divcan7 4 2 2 0 3 3 0 4 3 2 3 = 4 2
211 208 209 185 210 mp3an 4 3 2 3 = 4 2
212 4d2e2 4 2 = 2
213 211 212 eqtri 4 3 2 3 = 2
214 213 fveq2i log 4 3 2 3 = log 2
215 196 207 214 3eqtr2i log 1 i i 3 log 1 + i i 3 = log 2
216 215 oveq2i i 2 log 1 i i 3 log 1 + i i 3 = i 2 log 2
217 166 216 eqtri arctan i 3 = i 2 log 2
218 217 oveq2i 2 i arctan i 3 = 2 i i 2 log 2
219 2ne0 2 0
220 5 4 219 divcli i 2
221 logcl 2 2 0 log 2
222 4 219 221 mp2an log 2
223 7 220 222 mulassi 2 i i 2 log 2 = 2 i i 2 log 2
224 218 223 eqtr4i 2 i arctan i 3 = 2 i i 2 log 2
225 divcan6 2 2 0 i i 0 2 i i 2 = 1
226 4 219 5 6 225 mp4an 2 i i 2 = 1
227 226 oveq1i 2 i i 2 log 2 = 1 log 2
228 222 mulid2i 1 log 2 = log 2
229 224 227 228 3eqtri 2 i arctan i 3 = log 2
230 162 229 breqtri seq 0 + F log 2