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

Theorem leibpisum 20775
 Description: The Leibniz formula for . This version of leibpi 20774 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 10512 . . 3
2 0z 10285 . . . 4
32a1i 11 . . 3
4 oveq2 6081 . . . . . 6
5 oveq2 6081 . . . . . . 7
65oveq1d 6088 . . . . . 6
74, 6oveq12d 6091 . . . . 5
8 eqid 2435 . . . . 5
9 ovex 6098 . . . . 5
107, 8, 9fvmpt 5798 . . . 4
12 1re 9082 . . . . . . . 8
1312renegcli 9354 . . . . . . 7
14 reexpcl 11390 . . . . . . 7
1513, 14mpan 652 . . . . . 6
16 2nn0 10230 . . . . . . . 8
17 nn0mulcl 10248 . . . . . . . 8
1816, 17mpan 652 . . . . . . 7
19 nn0p1nn 10251 . . . . . . 7
2018, 19syl 16 . . . . . 6
2115, 20nndivred 10040 . . . . 5
2221recnd 9106 . . . 4