Metamath Proof Explorer

Theorem leibpisum

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

Ref Expression
Assertion leibpisum 
|- sum_ n e. NN0 ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) = ( _pi / 4 )

Proof

Step Hyp Ref Expression
1 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
2 0zd 
 |-  ( T. -> 0 e. ZZ )
3 oveq2 
 |-  ( k = n -> ( -u 1 ^ k ) = ( -u 1 ^ n ) )
4 oveq2 
 |-  ( k = n -> ( 2 x. k ) = ( 2 x. n ) )
5 4 oveq1d 
 |-  ( k = n -> ( ( 2 x. k ) + 1 ) = ( ( 2 x. n ) + 1 ) )
6 3 5 oveq12d 
 |-  ( k = n -> ( ( -u 1 ^ k ) / ( ( 2 x. k ) + 1 ) ) = ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) )
7 eqid 
 |-  ( k e. NN0 |-> ( ( -u 1 ^ k ) / ( ( 2 x. k ) + 1 ) ) ) = ( k e. NN0 |-> ( ( -u 1 ^ k ) / ( ( 2 x. k ) + 1 ) ) )
8 ovex 
 |-  ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) e. _V
9 6 7 8 fvmpt 
 |-  ( n e. NN0 -> ( ( k e. NN0 |-> ( ( -u 1 ^ k ) / ( ( 2 x. k ) + 1 ) ) ) ` n ) = ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) )
10 9 adantl 
 |-  ( ( T. /\ n e. NN0 ) -> ( ( k e. NN0 |-> ( ( -u 1 ^ k ) / ( ( 2 x. k ) + 1 ) ) ) ` n ) = ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) )
11 neg1rr 
 |-  -u 1 e. RR
12 reexpcl 
 |-  ( ( -u 1 e. RR /\ n e. NN0 ) -> ( -u 1 ^ n ) e. RR )
13 11 12 mpan 
 |-  ( n e. NN0 -> ( -u 1 ^ n ) e. RR )
14 2nn0 
 |-  2 e. NN0
15 nn0mulcl 
 |-  ( ( 2 e. NN0 /\ n e. NN0 ) -> ( 2 x. n ) e. NN0 )
16 14 15 mpan 
 |-  ( n e. NN0 -> ( 2 x. n ) e. NN0 )
17 nn0p1nn 
 |-  ( ( 2 x. n ) e. NN0 -> ( ( 2 x. n ) + 1 ) e. NN )
18 16 17 syl 
 |-  ( n e. NN0 -> ( ( 2 x. n ) + 1 ) e. NN )
19 13 18 nndivred 
 |-  ( n e. NN0 -> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) e. RR )
20 19 recnd 
 |-  ( n e. NN0 -> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) e. CC )
21 20 adantl 
 |-  ( ( T. /\ n e. NN0 ) -> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) e. CC )
22 7 leibpi 
 |-  seq 0 ( + , ( k e. NN0 |-> ( ( -u 1 ^ k ) / ( ( 2 x. k ) + 1 ) ) ) ) ~~> ( _pi / 4 )
23 22 a1i 
 |-  ( T. -> seq 0 ( + , ( k e. NN0 |-> ( ( -u 1 ^ k ) / ( ( 2 x. k ) + 1 ) ) ) ) ~~> ( _pi / 4 ) )
24 1 2 10 21 23 isumclim 
 |-  ( T. -> sum_ n e. NN0 ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) = ( _pi / 4 ) )
25 24 mptru 
 |-  sum_ n e. NN0 ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) = ( _pi / 4 )