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 )