Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  leibpi Unicode version

Theorem leibpi 20735
 Description: The Leibniz formula for . This proof depends on three main facts: (1) the series is convergent, because it is an alternating series (iseralt 12433). (2) Using leibpilem2 20734 to rewrite the series as a power series, it is the special case of the Taylor series for arctan (atantayl2 20731). (3) Although we cannot directly plug into atantayl2 20731, Abel's theorem (abelth2 20311) says that the limit along any sequence converging to , such as , of the power series converges to the power series extended to , and then since arctan is continuous at (atancn 20729) we get the desired result. (Contributed by Mario Carneiro, 7-Apr-2015.)
Hypothesis
Ref Expression
leibpi.1
Assertion
Ref Expression
leibpi

Proof of Theorem leibpi
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nn0uz 10476 . . . . 5
2 0z 10249 . . . . . 6
32a1i 11 . . . . 5
4 eqidd 2405 . . . . 5
5 0cn 9040 . . . . . . . . . 10
65a1i 11 . . . . . . . . 9
7 ioran 477 . . . . . . . . . 10
8 1re 9046 . . . . . . . . . . . . . 14
98renegcli 9318 . . . . . . . . . . . . 13
10 leibpilem1 20733 . . . . . . . . . . . . . 14
1110simprd 450 . . . . . . . . . . . . 13
12 reexpcl 11353 . . . . . . . . . . . . 13
139, 11, 12sylancr 645 . . . . . . . . . . . 12
1410simpld 446 . . . . . . . . . . . 12
1513, 14nndivred 10004 . . . . . . . . . . 11
1615recnd 9070 . . . . . . . . . 10
177, 16sylan2b 462 . . . . . . . . 9
186, 17ifclda 3726 . . . . . . . 8
1918adantl 453 . . . . . . 7
20 eqid 2404 . . . . . . 7
2119, 20fmptd 5852 . . . . . 6
2221ffvelrnda 5829 . . . . 5
23 2nn0 10194 . . . . . . . . . . . . . 14
2423a1i 11 . . . . . . . . . . . . 13
25 nn0mulcl 10212 . . . . . . . . . . . . 13
2624, 25sylan 458 . . . . . . . . . . . 12
27 nn0p1nn 10215 . . . . . . . . . . . 12
2826, 27syl 16 . . . . . . . . . . 11
2928nnrecred 10001 . . . . . . . . . 10
30 eqid 2404 . . . . . . . . . 10
3129, 30fmptd 5852 . . . . . . . . 9
32 nn0mulcl 10212 . . . . . . . . . . . . . 14
3324, 32sylan 458 . . . . . . . . . . . . 13
3433nn0red 10231 . . . . . . . . . . . 12
35 peano2nn0 10216 . . . . . . . . . . . . . . 15
3635adantl 453 . . . . . . . . . . . . . 14
37 nn0mulcl 10212 . . . . . . . . . . . . . 14
3823, 36, 37sylancr 645 . . . . . . . . . . . . 13
3938nn0red 10231 . . . . . . . . . . . 12
408a1i 11 . . . . . . . . . . . 12
41 nn0re 10186 . . . . . . . . . . . . . . 15
4241adantl 453 . . . . . . . . . . . . . 14
4342lep1d 9898 . . . . . . . . . . . . 13
44 peano2re 9195 . . . . . . . . . . . . . . 15
4542, 44syl 16 . . . . . . . . . . . . . 14
46 2re 10025 . . . . . . . . . . . . . . 15
4746a1i 11 . . . . . . . . . . . . . 14
48 2pos 10038 . . . . . . . . . . . . . . 15
4948a1i 11 . . . . . . . . . . . . . 14
50 lemul2 9819 . . . . . . . . . . . . . 14
5142, 45, 47, 49, 50syl112anc 1188 . . . . . . . . . . . . 13
5243, 51mpbid 202 . . . . . . . . . . . 12
5334, 39, 40, 52leadd1dd 9596 . . . . . . . . . . 11
54 nn0p1nn 10215 . . . . . . . . . . . . . 14
5533, 54syl 16 . . . . . . . . . . . . 13
5655nnred 9971 . . . . . . . . . . . 12
5755nngt0d 9999 . . . . . . . . . . . 12
58 nn0p1nn 10215 . . . . . . . . . . . . . 14
5938, 58syl 16 . . . . . . . . . . . . 13
6059nnred 9971 . . . . . . . . . . . 12
6159nngt0d 9999 . . . . . . . . . . . 12
62 lerec 9848 . . . . . . . . . . . 12
6356, 57, 60, 61, 62syl22anc 1185 . . . . . . . . . . 11
6453, 63mpbid 202 . . . . . . . . . 10
65 oveq2 6048 . . . . . . . . . . . . . 14
6665oveq1d 6055 . . . . . . . . . . . . 13
6766oveq2d 6056 . . . . . . . . . . . 12
68 ovex 6065 . . . . . . . . . . . 12
6967, 30, 68fvmpt 5765 . . . . . . . . . . 11
7036, 69syl 16 . . . . . . . . . 10
71 oveq2 6048 . . . . . . . . . . . . . 14
7271oveq1d 6055 . . . . . . . . . . . . 13
7372oveq2d 6056 . . . . . . . . . . . 12
74 ovex 6065 . . . . . . . . . . . 12
7573, 30, 74fvmpt 5765 . . . . . . . . . . 11
7675adantl 453 . . . . . . . . . 10
7764, 70, 763brtr4d 4202 . . . . . . . . 9
78 nnuz 10477 . . . . . . . . . 10
79 1z 10267 . . . . . . . . . . 11
8079a1i 11 . . . . . . . . . 10
81 ax-1cn 9004 . . . . . . . . . . 11
82 divcnv 12588 . . . . . . . . . . 11
8381, 82mp1i 12 . . . . . . . . . 10
84 nn0ex 10183 . . . . . . . . . . . 12
8584mptex 5925 . . . . . . . . . . 11
8685a1i 11 . . . . . . . . . 10
87 oveq2 6048 . . . . . . . . . . . . 13
88 eqid 2404 . . . . . . . . . . . . 13
89 ovex 6065 . . . . . . . . . . . . 13
9087, 88, 89fvmpt 5765 . . . . . . . . . . . 12
9190adantl 453 . . . . . . . . . . 11
92 nnrecre 9992 . . . . . . . . . . . 12
9392adantl 453 . . . . . . . . . . 11
9491, 93eqeltrd 2478 . . . . . . . . . 10
95 nnnn0 10184 . . . . . . . . . . . . 13
9695adantl 453 . . . . . . . . . . . 12
9796, 75syl 16 . . . . . . . . . . 11
9895, 55sylan2 461 . . . . . . . . . . . 12
9998nnrecred 10001 . . . . . . . . . . 11
10097, 99eqeltrd 2478 . . . . . . . . . 10
101 nnre 9963 . . . . . . . . . . . . . 14
102101adantl 453 . . . . . . . . . . . . 13
10323, 96, 32sylancr 645 . . . . . . . . . . . . . 14
104103nn0red 10231 . . . . . . . . . . . . 13
105 peano2re 9195 . . . . . . . . . . . . . 14
106104, 105syl 16 . . . . . . . . . . . . 13
107 nn0addge1 10222 . . . . . . . . . . . . . . 15
108102, 96, 107syl2anc 643 . . . . . . . . . . . . . 14
109102recnd 9070 . . . . . . . . . . . . . . 15
1101092timesd 10166 . . . . . . . . . . . . . 14
111108, 110breqtrrd 4198 . . . . . . . . . . . . 13
112104lep1d 9898 . . . . . . . . . . . . 13
113102, 104, 106, 111, 112letrd 9183 . . . . . . . . . . . 12
114 nngt0 9985 . . . . . . . . . . . . . 14
115114adantl 453 . . . . . . . . . . . . 13
11698nnred 9971 . . . . . . . . . . . . 13
11798nngt0d 9999 . . . . . . . . . . . . 13
118 lerec 9848 . . . . . . . . . . . . 13
119102, 115, 116, 117, 118syl22anc 1185 . . . . . . . . . . . 12
120113, 119mpbid 202 . . . . . . . . . . 11
121120, 97, 913brtr4d 4202 . . . . . . . . . 10
12298nnrpd 10603 . . . . . . . . . . . . 13
123122rpreccld 10614 . . . . . . . . . . . 12
124123rpge0d 10608 . . . . . . . . . . 11
125124, 97breqtrrd 4198 . . . . . . . . . 10
12678, 80, 83, 86, 94, 100, 121, 125climsqz2 12390 . . . . . . . . 9
127 neg1cn 10023 . . . . . . . . . . . . 13
128127a1i 11 . . . . . . . . . . . 12
129 expcl 11354 . . . . . . . . . . . 12
130128, 129sylan 458 . . . . . . . . . . 11
13155nncnd 9972 . . . . . . . . . . 11
13255nnne0d 10000 . . . . . . . . . . 11
133130, 131, 132divrecd 9749 . . . . . . . . . 10
134 oveq2 6048 . . . . . . . . . . . . 13
135134, 72oveq12d 6058 . . . . . . . . . . . 12
136 eqid 2404 . . . . . . . . . . . 12
137 ovex 6065 . . . . . . . . . . . 12
138135, 136, 137fvmpt 5765 . . . . . . . . . . 11
139138adantl 453 . . . . . . . . . 10
14076oveq2d 6056 . . . . . . . . . 10
141133, 139, 1403eqtr4d 2446 . . . . . . . . 9
1421, 3, 31, 77, 126, 141iseralt 12433 . . . . . . . 8
143 climdm 12303 . . . . . . . 8
144142, 143sylib 189 . . . . . . 7
145 fvex 5701 . . . . . . . 8
146136, 20, 145leibpilem2 20734 . . . . . . 7
147144, 146sylib 189 . . . . . 6
148 seqex 11280 . . . . . . 7
149148, 145breldm 5033 . . . . . 6
150147, 149syl 16 . . . . 5
1511, 3, 4, 22, 150isumclim2 12497 . . . 4
152 eqid 2404 . . . . . . . 8
15321, 150, 152abelth2 20311 . . . . . . 7
154 nnrp 10577 . . . . . . . . . . . . 13
155154adantl 453 . . . . . . . . . . . 12
156155rpreccld 10614 . . . . . . . . . . 11
157156rpred 10604 . . . . . . . . . 10
158156rpge0d 10608 . . . . . . . . . 10
159 nnge1 9982 . . . . . . . . . . . . 13
160159adantl 453 . . . . . . . . . . . 12
161 nnre 9963 . . . . . . . . . . . . . . 15
162161adantl 453 . . . . . . . . . . . . . 14
163162recnd 9070 . . . . . . . . . . . . 13
164163mulid1d 9061 . . . . . . . . . . . 12
165160, 164breqtrrd 4198 . . . . . . . . . . 11
1668a1i 11 . . . . . . . . . . . 12
167 nngt0 9985 . . . . . . . . . . . . 13
168167adantl 453 . . . . . . . . . . . 12
169 ledivmul 9839 . . . . . . . . . . . 12
170166, 166, 162, 168, 169syl112anc 1188 . . . . . . . . . . 11
171165, 170mpbird 224 . . . . . . . . . 10
172 0re 9047 . . . . . . . . . . 11
173172, 8elicc2i 10932 . . . . . . . . . 10
174157, 158, 171, 173syl3anbrc 1138 . . . . . . . . 9
175 iirev 18907 . . . . . . . . 9
176174, 175syl 16 . . . . . . . 8
177 eqid 2404 . . . . . . . 8
178176, 177fmptd 5852 . . . . . . 7
17981a1i 11 . . . . . . . . 9
180 nnex 9962 . . . . . . . . . . 11
181180mptex 5925 . . . . . . . . . 10
182181a1i 11 . . . . . . . . 9
18394recnd 9070 . . . . . . . . 9
18487oveq2d 6056 . . . . . . . . . . . 12
185 ovex 6065 . . . . . . . . . . . 12
186184, 177, 185fvmpt 5765 . . . . . . . . . . 11
18790oveq2d 6056 . . . . . . . . . . 11
188186, 187eqtr4d 2439 . . . . . . . . . 10
189188adantl 453 . . . . . . . . 9
19078, 80, 83, 179, 182, 183, 189climsubc2 12387 . . . . . . . 8
19181subid1i 9328 . . . . . . . 8
192190, 191syl6breq 4211 . . . . . . 7
193 1elunit 10972 . . . . . . . 8
194193a1i 11 . . . . . . 7
19578, 80, 153, 178, 192, 194climcncf 18883 . . . . . 6
196 eqidd 2405 . . . . . . . 8
197 eqidd 2405 . . . . . . . 8
198 oveq1 6047 . . . . . . . . . 10
199198oveq2d 6056 . . . . . . . . 9
200199sumeq2sdv 12453 . . . . . . . 8
201176, 196, 197, 200fmptco 5860 . . . . . . 7
2022a1i 11 . . . . . . . . 9
20311adantll 695 . . . . . . . . . . . . . . . . . . . . . 22
2049, 203, 12sylancr 645 . . . . . . . . . . . . . . . . . . . . 21
205204recnd 9070 . . . . . . . . . . . . . . . . . . . 20
206205adantllr 700 . . . . . . . . . . . . . . . . . . 19
207 resubcl 9321 . . . . . . . . . . . . . . . . . . . . . . 23
2088, 157, 207sylancr 645 . . . . . . . . . . . . . . . . . . . . . 22
209208ad2antrr 707 . . . . . . . . . . . . . . . . . . . . 21
210 simplr 732 . . . . . . . . . . . . . . . . . . . . 21
211209, 210reexpcld 11495 . . . . . . . . . . . . . . . . . . . 20
212211recnd 9070 . . . . . . . . . . . . . . . . . . 19
213 nn0cn 10187 . . . . . . . . . . . . . . . . . . . 20
214213ad2antlr 708 . . . . . . . . . . . . . . . . . . 19
21514adantll 695 . . . . . . . . . . . . . . . . . . . 20
216215nnne0d 10000 . . . . . . . . . . . . . . . . . . 19
217206, 212, 214, 216div12d 9782 . . . . . . . . . . . . . . . . . 18
21816adantll 695 . . . . . . . . . . . . . . . . . . 19
219212, 218mulcomd 9065 . . . . . . . . . . . . . . . . . 18
220217, 219eqtrd 2436 . . . . . . . . . . . . . . . . 17
2217, 220sylan2b 462 . . . . . . . . . . . . . . . 16
222221ifeq2da 3725 . . . . . . . . . . . . . . 15
223208recnd 9070 . . . . . . . . . . . . . . . . . 18
224 expcl 11354 . . . . . . . . . . . . . . . . . 18
225223, 224sylan 458 . . . . . . . . . . . . . . . . 17
226225mul02d 9220 . . . . . . . . . . . . . . . 16
227226ifeq1d 3713 . . . . . . . . . . . . . . 15
228222, 227eqtr4d 2439 . . . . . . . . . . . . . 14
229 oveq1 6047 . . . . . . . . . . . . . . 15
230 oveq1 6047 . . . . . . . . . . . . . . 15
231229, 230ifsb 3708 . . . . . . . . . . . . . 14
232228, 231syl6eqr 2454 . . . . . . . . . . . . 13
233 simpr 448 . . . . . . . . . . . . . 14
234 c0ex 9041 . . . . . . . . . . . . . . 15
235 ovex 6065 . . . . . . . . . . . . . . 15
236234, 235ifex 3757 . . . . . . . . . . . . . 14
237 eqid 2404 . . . . . . . . . . . . . . 15
238237fvmpt2 5771 . . . . . . . . . . . . . 14
239233, 236, 238sylancl 644 . . . . . . . . . . . . 13
240 ovex 6065 . . . . . . . . . . . . . . . 16
241234, 240ifex 3757 . . . . . . . . . . . . . . 15
24220fvmpt2 5771 . . . . . . . . . . . . . . 15
243233, 241, 242sylancl 644 . . . . . . . . . . . . . 14
244243oveq1d 6055 . . . . . . . . . . . . 13
245232, 239, 2443eqtr4d 2446 . . . . . . . . . . . 12
246245ralrimiva 2749 . . . . . . . . . . 11
247 nfv 1626 . . . . . . . . . . . 12
248 nffvmpt1 5695 . . . . . . . . . . . . 13
249 nffvmpt1 5695 . . . . . . . . . . . . . 14
250 nfcv 2540 . . . . . . . . . . . . . 14
251 nfcv 2540 . . . . . . . . . . . . . 14
252249, 250, 251nfov 6063 . . . . . . . . . . . . 13
253248, 252nfeq 2547 . . . . . . . . . . . 12
254 fveq2 5687 . . . . . . . . . . . . 13
255 fveq2 5687 . . . . . . . . . . . . . 14
256 oveq2 6048 . . . . . . . . . . . . . 14
257255, 256oveq12d 6058 . . . . . . . . . . . . 13
258254, 257eqeq12d 2418 . . . . . . . . . . . 12
259247, 253, 258cbvral 2888 . . . . . . . . . . 11
260246, 259sylib 189 . . . . . . . . . 10
261260r19.21bi 2764 . . . . . . . . 9
2625a1i 11 . . . . . . . . . . . . 13
263211, 215nndivred 10004 . . . . . . . . . . . . . . . 16
264263recnd 9070 . . . . . . . . . . . . . . 15
265206, 264mulcld 9064 . . . . . . . . . . . . . 14
2667, 265sylan2b 462 . . . . . . . . . . . . 13
267262, 266ifclda 3726 . . . . . . . . . . . 12
268267, 237fmptd 5852 . . . . . . . . . . 11
269268ffvelrnda 5829 . . . . . . . . . 10
270261, 269eqeltrrd 2479 . . . . . . . . 9
271 0nn0 10192 . . . . . . . . . . . 12
272271a1i 11 . . . . . . . . . . 11
273 0p1e1 10049 . . . . . . . . . . . . 13
274 seqeq1 11281 . . . . . . . . . . . . 13
275273, 274ax-mp 8 . . . . . . . . . . . 12
27679a1i 11 . . . . . . . . . . . . . 14
277 elnnuz 10478 . . . . . . . . . . . . . . 15
278 nnne0 9988 . . . . . . . . . . . . . . . . . . . . . . . 24
279278neneqd 2583 . . . . . . . . . . . . . . . . . . . . . . 23
280 biorf 395 . . . . . . . . . . . . . . . . . . . . . . 23
281279, 280syl 16 . . . . . . . . . . . . . . . . . . . . . 22
282281bicomd 193 . . . . . . . . . . . . . . . . . . . . 21
283282ifbid 3717 . . . . . . . . . . . . . . . . . . . 20
28495, 236, 238sylancl 644 . . . . . . . . . . . . . . . . . . . 20
285234, 235ifex 3757 . . . . . . . . . . . . . . . . . . . . 21
286 eqid 2404 . . . . . . . . . . . . . . . . . . . . . 22
287286fvmpt2 5771 . . . . . . . . . . . . . . . . . . . . 21
288285, 287mpan2 653 . . . . . . . . . . . . . . . . . . . 20
289283, 284, 2883eqtr4d 2446 . . . . . . . . . . . . . . . . . . 19
290289rgen 2731 . . . . . . . . . . . . . . . . . 18
291290a1i 11 . . . . . . . . . . . . . . . . 17
292 nfv 1626 . . . . . . . . . . . . . . . . . 18
293 nffvmpt1 5695 . . . . . . . . . . . . . . . . . . 19
294248, 293nfeq 2547 . . . . . . . . . . . . . . . . . 18
295 fveq2 5687 . . . . . . . . . . . . . . . . . . 19
296254, 295eqeq12d 2418 . . . . . . . . . . . . . . . . . 18
297292, 294, 296cbvral 2888 . . . . . . . . . . . . . . . . 17
298291, 297sylib 189 . . . . . . . . . . . . . . . 16
299298r19.21bi 2764 . . . . . . . . . . . . . . 15
300277, 299sylan2br 463 . . . . . . . . . . . . . 14
301276, 300seqfeq 11303 . . . . . . . . . . . . 13
302157, 166, 171abssubge0d 12189 . . . . . . . . . . . . . . 15
303 ltsubrp 10599 . . . . . . . . . . . . . . . 16
3048, 156, 303sylancr 645 . . . . . . . . . . . . . . 15
305302, 304eqbrtrd 4192 . . . . . . . . . . . . . 14
306286atantayl2 20731 . . . . . . . . . . . . . 14 arctan
307223, 305, 306syl2anc 643 . . . . . . . . . . . . 13 arctan
308301, 307eqbrtrd 4192 . . . . . . . . . . . 12 arctan
309275, 308syl5eqbr 4205 . . . . . . . . . . 11 arctan
3101, 272, 269, 309clim2ser2 12404 . . . . . . . . . 10 arctan
311 seq1 11291 . . . . . . . . . . . . . 14
3122, 311ax-mp 8 . . . . . . . . . . . . 13
313 iftrue 3705 . . . . . . . . . . . . . . . 16
314313orcs 384 . . . . . . . . . . . . . . 15
315314, 237, 234fvmpt 5765 . . . . . . . . . . . . . 14
316271, 315ax-mp 8 . . . . . . . . . . . . 13
317312, 316eqtri 2424 . . . . . . . . . . . 12
318317oveq2i 6051 . . . . . . . . . . 11 arctan arctan
319 atanrecl 20704 . . . . . . . . . . . . . 14 arctan
320208, 319syl 16 . . . . . . . . . . . . 13 arctan
321320recnd 9070 . . . . . . . . . . . 12 arctan
322321addid1d 9222 . . . . . . . . . . 11 arctan arctan
323318, 322syl5eq 2448 . . . . . . . . . 10 arctan arctan
324310, 323breqtrd 4196 . . . . . . . . 9 arctan
3251, 202, 261, 270, 324isumclim 12496 . . . . . . . 8