Metamath Proof Explorer


Theorem leibpilem2

Description: The Leibniz formula for _pi . (Contributed by Mario Carneiro, 7-Apr-2015)

Ref Expression
Hypotheses leibpi.1
|- F = ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) )
leibpilem2.2
|- G = ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) )
leibpilem2.3
|- A e. _V
Assertion leibpilem2
|- ( seq 0 ( + , F ) ~~> A <-> seq 0 ( + , G ) ~~> A )

Proof

Step Hyp Ref Expression
1 leibpi.1
 |-  F = ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) )
2 leibpilem2.2
 |-  G = ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) )
3 leibpilem2.3
 |-  A e. _V
4 2cn
 |-  2 e. CC
5 nn0cn
 |-  ( n e. NN0 -> n e. CC )
6 mulcl
 |-  ( ( 2 e. CC /\ n e. CC ) -> ( 2 x. n ) e. CC )
7 4 5 6 sylancr
 |-  ( n e. NN0 -> ( 2 x. n ) e. CC )
8 ax-1cn
 |-  1 e. CC
9 pncan
 |-  ( ( ( 2 x. n ) e. CC /\ 1 e. CC ) -> ( ( ( 2 x. n ) + 1 ) - 1 ) = ( 2 x. n ) )
10 7 8 9 sylancl
 |-  ( n e. NN0 -> ( ( ( 2 x. n ) + 1 ) - 1 ) = ( 2 x. n ) )
11 10 oveq1d
 |-  ( n e. NN0 -> ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) = ( ( 2 x. n ) / 2 ) )
12 2ne0
 |-  2 =/= 0
13 divcan3
 |-  ( ( n e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( 2 x. n ) / 2 ) = n )
14 4 12 13 mp3an23
 |-  ( n e. CC -> ( ( 2 x. n ) / 2 ) = n )
15 5 14 syl
 |-  ( n e. NN0 -> ( ( 2 x. n ) / 2 ) = n )
16 11 15 eqtrd
 |-  ( n e. NN0 -> ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) = n )
17 16 oveq2d
 |-  ( n e. NN0 -> ( -u 1 ^ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) = ( -u 1 ^ n ) )
18 17 oveq1d
 |-  ( n e. NN0 -> ( ( -u 1 ^ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) / ( ( 2 x. n ) + 1 ) ) = ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) )
19 18 mpteq2ia
 |-  ( n e. NN0 |-> ( ( -u 1 ^ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) / ( ( 2 x. n ) + 1 ) ) ) = ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) )
20 1 19 eqtr4i
 |-  F = ( n e. NN0 |-> ( ( -u 1 ^ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) / ( ( 2 x. n ) + 1 ) ) )
21 seqeq3
 |-  ( F = ( n e. NN0 |-> ( ( -u 1 ^ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) / ( ( 2 x. n ) + 1 ) ) ) -> seq 0 ( + , F ) = seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) / ( ( 2 x. n ) + 1 ) ) ) ) )
22 20 21 ax-mp
 |-  seq 0 ( + , F ) = seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) / ( ( 2 x. n ) + 1 ) ) ) )
23 22 breq1i
 |-  ( seq 0 ( + , F ) ~~> A <-> seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) / ( ( 2 x. n ) + 1 ) ) ) ) ~~> A )
24 neg1rr
 |-  -u 1 e. RR
25 reexpcl
 |-  ( ( -u 1 e. RR /\ n e. NN0 ) -> ( -u 1 ^ n ) e. RR )
26 24 25 mpan
 |-  ( n e. NN0 -> ( -u 1 ^ n ) e. RR )
27 2nn0
 |-  2 e. NN0
28 nn0mulcl
 |-  ( ( 2 e. NN0 /\ n e. NN0 ) -> ( 2 x. n ) e. NN0 )
29 27 28 mpan
 |-  ( n e. NN0 -> ( 2 x. n ) e. NN0 )
30 nn0p1nn
 |-  ( ( 2 x. n ) e. NN0 -> ( ( 2 x. n ) + 1 ) e. NN )
31 29 30 syl
 |-  ( n e. NN0 -> ( ( 2 x. n ) + 1 ) e. NN )
32 26 31 nndivred
 |-  ( n e. NN0 -> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) e. RR )
33 32 recnd
 |-  ( n e. NN0 -> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) e. CC )
34 18 33 eqeltrd
 |-  ( n e. NN0 -> ( ( -u 1 ^ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) / ( ( 2 x. n ) + 1 ) ) e. CC )
35 34 adantl
 |-  ( ( T. /\ n e. NN0 ) -> ( ( -u 1 ^ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) / ( ( 2 x. n ) + 1 ) ) e. CC )
36 oveq1
 |-  ( k = ( ( 2 x. n ) + 1 ) -> ( k - 1 ) = ( ( ( 2 x. n ) + 1 ) - 1 ) )
37 36 oveq1d
 |-  ( k = ( ( 2 x. n ) + 1 ) -> ( ( k - 1 ) / 2 ) = ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) )
38 37 oveq2d
 |-  ( k = ( ( 2 x. n ) + 1 ) -> ( -u 1 ^ ( ( k - 1 ) / 2 ) ) = ( -u 1 ^ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) )
39 id
 |-  ( k = ( ( 2 x. n ) + 1 ) -> k = ( ( 2 x. n ) + 1 ) )
40 38 39 oveq12d
 |-  ( k = ( ( 2 x. n ) + 1 ) -> ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) = ( ( -u 1 ^ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) / ( ( 2 x. n ) + 1 ) ) )
41 35 40 iserodd
 |-  ( T. -> ( seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) / ( ( 2 x. n ) + 1 ) ) ) ) ~~> A <-> seq 1 ( + , ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ) ~~> A ) )
42 41 mptru
 |-  ( seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) / ( ( 2 x. n ) + 1 ) ) ) ) ~~> A <-> seq 1 ( + , ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ) ~~> A )
43 addid2
 |-  ( n e. CC -> ( 0 + n ) = n )
44 43 adantl
 |-  ( ( T. /\ n e. CC ) -> ( 0 + n ) = n )
45 0cnd
 |-  ( T. -> 0 e. CC )
46 1eluzge0
 |-  1 e. ( ZZ>= ` 0 )
47 46 a1i
 |-  ( T. -> 1 e. ( ZZ>= ` 0 ) )
48 1nn0
 |-  1 e. NN0
49 0cnd
 |-  ( ( k e. NN0 /\ ( k = 0 \/ 2 || k ) ) -> 0 e. CC )
50 ioran
 |-  ( -. ( k = 0 \/ 2 || k ) <-> ( -. k = 0 /\ -. 2 || k ) )
51 leibpilem1
 |-  ( ( k e. NN0 /\ ( -. k = 0 /\ -. 2 || k ) ) -> ( k e. NN /\ ( ( k - 1 ) / 2 ) e. NN0 ) )
52 51 simprd
 |-  ( ( k e. NN0 /\ ( -. k = 0 /\ -. 2 || k ) ) -> ( ( k - 1 ) / 2 ) e. NN0 )
53 reexpcl
 |-  ( ( -u 1 e. RR /\ ( ( k - 1 ) / 2 ) e. NN0 ) -> ( -u 1 ^ ( ( k - 1 ) / 2 ) ) e. RR )
54 24 52 53 sylancr
 |-  ( ( k e. NN0 /\ ( -. k = 0 /\ -. 2 || k ) ) -> ( -u 1 ^ ( ( k - 1 ) / 2 ) ) e. RR )
55 51 simpld
 |-  ( ( k e. NN0 /\ ( -. k = 0 /\ -. 2 || k ) ) -> k e. NN )
56 54 55 nndivred
 |-  ( ( k e. NN0 /\ ( -. k = 0 /\ -. 2 || k ) ) -> ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) e. RR )
57 56 recnd
 |-  ( ( k e. NN0 /\ ( -. k = 0 /\ -. 2 || k ) ) -> ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) e. CC )
58 50 57 sylan2b
 |-  ( ( k e. NN0 /\ -. ( k = 0 \/ 2 || k ) ) -> ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) e. CC )
59 49 58 ifclda
 |-  ( k e. NN0 -> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) e. CC )
60 2 59 fmpti
 |-  G : NN0 --> CC
61 60 ffvelrni
 |-  ( 1 e. NN0 -> ( G ` 1 ) e. CC )
62 48 61 mp1i
 |-  ( T. -> ( G ` 1 ) e. CC )
63 simpr
 |-  ( ( T. /\ n e. ( 0 ... ( 1 - 1 ) ) ) -> n e. ( 0 ... ( 1 - 1 ) ) )
64 1m1e0
 |-  ( 1 - 1 ) = 0
65 64 oveq2i
 |-  ( 0 ... ( 1 - 1 ) ) = ( 0 ... 0 )
66 63 65 eleqtrdi
 |-  ( ( T. /\ n e. ( 0 ... ( 1 - 1 ) ) ) -> n e. ( 0 ... 0 ) )
67 elfz1eq
 |-  ( n e. ( 0 ... 0 ) -> n = 0 )
68 66 67 syl
 |-  ( ( T. /\ n e. ( 0 ... ( 1 - 1 ) ) ) -> n = 0 )
69 68 fveq2d
 |-  ( ( T. /\ n e. ( 0 ... ( 1 - 1 ) ) ) -> ( G ` n ) = ( G ` 0 ) )
70 0nn0
 |-  0 e. NN0
71 iftrue
 |-  ( ( k = 0 \/ 2 || k ) -> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) = 0 )
72 71 orcs
 |-  ( k = 0 -> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) = 0 )
73 c0ex
 |-  0 e. _V
74 72 2 73 fvmpt
 |-  ( 0 e. NN0 -> ( G ` 0 ) = 0 )
75 70 74 ax-mp
 |-  ( G ` 0 ) = 0
76 69 75 eqtrdi
 |-  ( ( T. /\ n e. ( 0 ... ( 1 - 1 ) ) ) -> ( G ` n ) = 0 )
77 44 45 47 62 76 seqid
 |-  ( T. -> ( seq 0 ( + , G ) |` ( ZZ>= ` 1 ) ) = seq 1 ( + , G ) )
78 1zzd
 |-  ( T. -> 1 e. ZZ )
79 simpr
 |-  ( ( T. /\ n e. ( ZZ>= ` 1 ) ) -> n e. ( ZZ>= ` 1 ) )
80 nnuz
 |-  NN = ( ZZ>= ` 1 )
81 79 80 eleqtrrdi
 |-  ( ( T. /\ n e. ( ZZ>= ` 1 ) ) -> n e. NN )
82 nnne0
 |-  ( n e. NN -> n =/= 0 )
83 82 neneqd
 |-  ( n e. NN -> -. n = 0 )
84 biorf
 |-  ( -. n = 0 -> ( 2 || n <-> ( n = 0 \/ 2 || n ) ) )
85 83 84 syl
 |-  ( n e. NN -> ( 2 || n <-> ( n = 0 \/ 2 || n ) ) )
86 85 ifbid
 |-  ( n e. NN -> if ( 2 || n , 0 , ( ( -u 1 ^ ( ( n - 1 ) / 2 ) ) / n ) ) = if ( ( n = 0 \/ 2 || n ) , 0 , ( ( -u 1 ^ ( ( n - 1 ) / 2 ) ) / n ) ) )
87 breq2
 |-  ( k = n -> ( 2 || k <-> 2 || n ) )
88 oveq1
 |-  ( k = n -> ( k - 1 ) = ( n - 1 ) )
89 88 oveq1d
 |-  ( k = n -> ( ( k - 1 ) / 2 ) = ( ( n - 1 ) / 2 ) )
90 89 oveq2d
 |-  ( k = n -> ( -u 1 ^ ( ( k - 1 ) / 2 ) ) = ( -u 1 ^ ( ( n - 1 ) / 2 ) ) )
91 id
 |-  ( k = n -> k = n )
92 90 91 oveq12d
 |-  ( k = n -> ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) = ( ( -u 1 ^ ( ( n - 1 ) / 2 ) ) / n ) )
93 87 92 ifbieq2d
 |-  ( k = n -> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) = if ( 2 || n , 0 , ( ( -u 1 ^ ( ( n - 1 ) / 2 ) ) / n ) ) )
94 eqid
 |-  ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) = ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) )
95 ovex
 |-  ( ( -u 1 ^ ( ( n - 1 ) / 2 ) ) / n ) e. _V
96 73 95 ifex
 |-  if ( 2 || n , 0 , ( ( -u 1 ^ ( ( n - 1 ) / 2 ) ) / n ) ) e. _V
97 93 94 96 fvmpt
 |-  ( n e. NN -> ( ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` n ) = if ( 2 || n , 0 , ( ( -u 1 ^ ( ( n - 1 ) / 2 ) ) / n ) ) )
98 nnnn0
 |-  ( n e. NN -> n e. NN0 )
99 eqeq1
 |-  ( k = n -> ( k = 0 <-> n = 0 ) )
100 99 87 orbi12d
 |-  ( k = n -> ( ( k = 0 \/ 2 || k ) <-> ( n = 0 \/ 2 || n ) ) )
101 100 92 ifbieq2d
 |-  ( k = n -> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) = if ( ( n = 0 \/ 2 || n ) , 0 , ( ( -u 1 ^ ( ( n - 1 ) / 2 ) ) / n ) ) )
102 73 95 ifex
 |-  if ( ( n = 0 \/ 2 || n ) , 0 , ( ( -u 1 ^ ( ( n - 1 ) / 2 ) ) / n ) ) e. _V
103 101 2 102 fvmpt
 |-  ( n e. NN0 -> ( G ` n ) = if ( ( n = 0 \/ 2 || n ) , 0 , ( ( -u 1 ^ ( ( n - 1 ) / 2 ) ) / n ) ) )
104 98 103 syl
 |-  ( n e. NN -> ( G ` n ) = if ( ( n = 0 \/ 2 || n ) , 0 , ( ( -u 1 ^ ( ( n - 1 ) / 2 ) ) / n ) ) )
105 86 97 104 3eqtr4d
 |-  ( n e. NN -> ( ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` n ) = ( G ` n ) )
106 81 105 syl
 |-  ( ( T. /\ n e. ( ZZ>= ` 1 ) ) -> ( ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ` n ) = ( G ` n ) )
107 78 106 seqfeq
 |-  ( T. -> seq 1 ( + , ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ) = seq 1 ( + , G ) )
108 77 107 eqtr4d
 |-  ( T. -> ( seq 0 ( + , G ) |` ( ZZ>= ` 1 ) ) = seq 1 ( + , ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ) )
109 108 mptru
 |-  ( seq 0 ( + , G ) |` ( ZZ>= ` 1 ) ) = seq 1 ( + , ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) )
110 109 breq1i
 |-  ( ( seq 0 ( + , G ) |` ( ZZ>= ` 1 ) ) ~~> A <-> seq 1 ( + , ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ) ~~> A )
111 1z
 |-  1 e. ZZ
112 seqex
 |-  seq 0 ( + , G ) e. _V
113 climres
 |-  ( ( 1 e. ZZ /\ seq 0 ( + , G ) e. _V ) -> ( ( seq 0 ( + , G ) |` ( ZZ>= ` 1 ) ) ~~> A <-> seq 0 ( + , G ) ~~> A ) )
114 111 112 113 mp2an
 |-  ( ( seq 0 ( + , G ) |` ( ZZ>= ` 1 ) ) ~~> A <-> seq 0 ( + , G ) ~~> A )
115 110 114 bitr3i
 |-  ( seq 1 ( + , ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) ) ) ~~> A <-> seq 0 ( + , G ) ~~> A )
116 23 42 115 3bitri
 |-  ( seq 0 ( + , F ) ~~> A <-> seq 0 ( + , G ) ~~> A )