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 0 1 n 2 n + 1
leibpilem2.2 G = k 0 if k = 0 2 k 0 1 k 1 2 k
leibpilem2.3 A V
Assertion leibpilem2 seq 0 + F A seq 0 + G A

Proof

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