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

Theorem leibpisum 22466
 Description: The Leibniz formula for . This version of leibpi 22465 looks nicer but does not assert that the series is convergent so is not as practically useful. (Contributed by Mario Carneiro, 7-Apr-2015.)
Assertion
Ref Expression
leibpisum

Proof of Theorem leibpisum
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 nn0uz 11001 . . 3
2 0zd 10764 . . 3
3 oveq2 6203 . . . . . 6
4 oveq2 6203 . . . . . . 7
54oveq1d 6210 . . . . . 6
63, 5oveq12d 6213 . . . . 5
7 eqid 2452 . . . . 5
8 ovex 6220 . . . . 5
96, 7, 8fvmpt 5878 . . . 4
11 neg1rr 10532 . . . . . . 7
12 reexpcl 11994 . . . . . . 7
1311, 12mpan 670 . . . . . 6
14 2nn0 10702 . . . . . . . 8
15 nn0mulcl 10722 . . . . . . . 8
1614, 15mpan 670 . . . . . . 7
17 nn0p1nn 10725 . . . . . . 7
1816, 17syl 16 . . . . . 6
1913, 18nndivred 10476 . . . . 5
2019recnd 9518 . . . 4