Metamath Proof Explorer


Theorem basellem5

Description: Lemma for basel . Using vieta1 , we can calculate the sum of the roots of P as the quotient of the top two coefficients, and since the function T enumerates the roots, we are left with an equation that sums the cot ^ 2 function at the M different roots. (Contributed by Mario Carneiro, 29-Jul-2014)

Ref Expression
Hypotheses basel.n N=2 M+1
basel.p P=tj=0M(N2j)1Mjtj
basel.t T=n1MtannπN2
Assertion basellem5 Mk=1MtankπN2=2 M2 M16

Proof

Step Hyp Ref Expression
1 basel.n N=2 M+1
2 basel.p P=tj=0M(N2j)1Mjtj
3 basel.t T=n1MtannπN2
4 eqid coeffP=coeffP
5 eqid degP=degP
6 eqid P-10=P-10
7 1 2 basellem2 MPPolydegP=McoeffP=n0(N2n)1Mn
8 7 simp1d MPPoly
9 7 simp2d MdegP=M
10 nnnn0 MM0
11 hashfz1 M01M=M
12 10 11 syl M1M=M
13 fzfid M1MFin
14 1 2 3 basellem4 MT:1M1-1 ontoP-10
15 13 14 hasheqf1od M1M=P-10
16 9 12 15 3eqtr2rd MP-10=degP
17 id MM
18 9 17 eqeltrd MdegP
19 4 5 6 8 16 18 vieta1 MxP-10x=coeffPdegP1coeffPdegP
20 id x=tankπN2x=tankπN2
21 oveq1 n=knπ=kπ
22 21 fvoveq1d n=ktannπN=tankπN
23 22 oveq1d n=ktannπN2=tankπN2
24 ovex tankπN2V
25 23 3 24 fvmpt k1MTk=tankπN2
26 25 adantl Mk1MTk=tankπN2
27 cnvimass P-10domP
28 plyf PPolyP:
29 fdm P:domP=
30 8 28 29 3syl MdomP=
31 27 30 sseqtrid MP-10
32 31 sselda MxP-10x
33 20 13 14 26 32 fsumf1o MxP-10x=k=1MtankπN2
34 7 simp3d McoeffP=n0(N2n)1Mn
35 9 oveq1d MdegP1=M1
36 34 35 fveq12d McoeffPdegP1=n0(N2n)1MnM1
37 nnm1nn0 MM10
38 oveq2 n=M12n=2M1
39 38 oveq2d n=M1(N2n)=(N2M1)
40 oveq2 n=M1Mn=MM1
41 40 oveq2d n=M11Mn=1MM1
42 39 41 oveq12d n=M1(N2n)1Mn=(N2M1)1MM1
43 eqid n0(N2n)1Mn=n0(N2n)1Mn
44 ovex (N2M1)1MM1V
45 42 43 44 fvmpt M10n0(N2n)1MnM1=(N2M1)1MM1
46 37 45 syl Mn0(N2n)1MnM1=(N2M1)1MM1
47 nncn MM
48 ax-1cn 1
49 nncan M1MM1=1
50 47 48 49 sylancl MMM1=1
51 50 oveq2d M1MM1=11
52 neg1cn 1
53 exp1 111=1
54 52 53 ax-mp 11=1
55 51 54 eqtrdi M1MM1=1
56 55 oveq2d M(N2M1)1MM1=(N2M1)-1
57 2nn 2
58 nnmulcl 2M2 M
59 57 58 mpan M2 M
60 59 peano2nnd M2 M+1
61 1 60 eqeltrid MN
62 61 nnnn0d MN0
63 2z 2
64 nnz MM
65 peano2zm MM1
66 64 65 syl MM1
67 zmulcl 2M12M1
68 63 66 67 sylancr M2M1
69 bccl N02M1(N2M1)0
70 62 68 69 syl2anc M(N2M1)0
71 70 nn0cnd M(N2M1)
72 mulcom (N2M1)1(N2M1)-1=-1(N2M1)
73 71 52 72 sylancl M(N2M1)-1=-1(N2M1)
74 71 mulm1d M-1(N2M1)=(N2M1)
75 56 73 74 3eqtrd M(N2M1)1MM1=(N2M1)
76 36 46 75 3eqtrd McoeffPdegP1=(N2M1)
77 71 negcld M(N2M1)
78 76 77 eqeltrd McoeffPdegP1
79 34 9 fveq12d McoeffPdegP=n0(N2n)1MnM
80 oveq2 n=M2n=2 M
81 80 oveq2d n=M(N2n)=(N2 M)
82 oveq2 n=MMn=MM
83 82 oveq2d n=M1Mn=1MM
84 81 83 oveq12d n=M(N2n)1Mn=(N2 M)1MM
85 ovex (N2 M)1MMV
86 84 43 85 fvmpt M0n0(N2n)1MnM=(N2 M)1MM
87 10 86 syl Mn0(N2n)1MnM=(N2 M)1MM
88 47 subidd MMM=0
89 88 oveq2d M1MM=10
90 exp0 110=1
91 52 90 ax-mp 10=1
92 89 91 eqtrdi M1MM=1
93 92 oveq2d M(N2 M)1MM=(N2 M)1
94 fz1ssfz0 1N0N
95 59 nnred M2 M
96 95 lep1d M2 M2 M+1
97 96 1 breqtrrdi M2 MN
98 nnuz =1
99 59 98 eleqtrdi M2 M1
100 61 nnzd MN
101 elfz5 2 M1N2 M1N2 MN
102 99 100 101 syl2anc M2 M1N2 MN
103 97 102 mpbird M2 M1N
104 94 103 sselid M2 M0N
105 bccl2 2 M0N(N2 M)
106 104 105 syl M(N2 M)
107 106 nncnd M(N2 M)
108 107 mulid1d M(N2 M)1=(N2 M)
109 93 108 eqtrd M(N2 M)1MM=(N2 M)
110 79 87 109 3eqtrd McoeffPdegP=(N2 M)
111 110 107 eqeltrd McoeffPdegP
112 106 nnne0d M(N2 M)0
113 110 112 eqnetrd McoeffPdegP0
114 78 111 113 divnegd McoeffPdegP1coeffPdegP=coeffPdegP1coeffPdegP
115 76 negeqd McoeffPdegP1=(N2M1)
116 71 negnegd M(N2M1)=(N2M1)
117 115 116 eqtrd McoeffPdegP1=(N2M1)
118 117 110 oveq12d McoeffPdegP1coeffPdegP=(N2M1)(N2 M)
119 bcm1k 2 M1N(N2 M)=(N2 M1)N2 M12 M
120 103 119 syl M(N2 M)=(N2 M1)N2 M12 M
121 59 nncnd M2 M
122 1cnd M1
123 121 122 122 pnncand M2 M+1-2 M1=1+1
124 1 oveq1i N2 M1=2 M+1-2 M1
125 df-2 2=1+1
126 123 124 125 3eqtr4g MN2 M1=2
127 2nn0 20
128 126 127 eqeltrdi MN2 M10
129 nnm1nn0 2 M2 M10
130 59 129 syl M2 M10
131 nn0sub 2 M10N02 M1NN2 M10
132 130 62 131 syl2anc M2 M1NN2 M10
133 128 132 mpbird M2 M1N
134 47 2timesd M2 M=M+M
135 134 oveq1d M2 M1=M+M-1
136 47 47 122 addsubd MM+M-1=M-1+M
137 135 136 eqtrd M2 M1=M-1+M
138 nn0nnaddcl M10MM-1+M
139 37 138 mpancom MM-1+M
140 137 139 eqeltrd M2 M1
141 140 98 eleqtrdi M2 M11
142 elfz5 2 M11N2 M11N2 M1N
143 141 100 142 syl2anc M2 M11N2 M1N
144 133 143 mpbird M2 M11N
145 bcm1k 2 M11N(N2 M1)=(N2 M-1-1)N2 M-1-12 M1
146 144 145 syl M(N2 M1)=(N2 M-1-1)N2 M-1-12 M1
147 48 2timesi 21=1+1
148 147 eqcomi 1+1=21
149 148 oveq2i 2 M1+1=2 M21
150 121 122 122 subsub4d M2 M-1-1=2 M1+1
151 2cnd M2
152 151 47 122 subdid M2M1=2 M21
153 149 150 152 3eqtr4a M2 M-1-1=2M1
154 153 oveq2d M(N2 M-1-1)=(N2M1)
155 61 nncnd MN
156 140 nncnd M2 M1
157 155 156 122 subsubd MN2 M-1-1=N-2 M1+1
158 126 oveq1d MN-2 M1+1=2+1
159 df-3 3=2+1
160 158 159 eqtr4di MN-2 M1+1=3
161 157 160 eqtrd MN2 M-1-1=3
162 161 oveq1d MN2 M-1-12 M1=32 M1
163 154 162 oveq12d M(N2 M-1-1)N2 M-1-12 M1=(N2M1)32 M1
164 146 163 eqtrd M(N2 M1)=(N2M1)32 M1
165 126 oveq1d MN2 M12 M=22 M
166 164 165 oveq12d M(N2 M1)N2 M12 M=(N2M1)32 M122 M
167 3re 3
168 nndivre 32 M132 M1
169 167 140 168 sylancr M32 M1
170 169 recnd M32 M1
171 2re 2
172 nndivre 22 M22 M
173 171 59 172 sylancr M22 M
174 173 recnd M22 M
175 71 170 174 mulassd M(N2M1)32 M122 M=(N2M1)32 M122 M
176 120 166 175 3eqtrd M(N2 M)=(N2M1)32 M122 M
177 3cn 3
178 177 a1i M3
179 140 nnne0d M2 M10
180 59 nnne0d M2 M0
181 178 156 151 121 179 180 divmuldivd M32 M122 M=322 M12 M
182 3t2e6 32=6
183 182 a1i M32=6
184 156 121 mulcomd M2 M12 M=2 M2 M1
185 183 184 oveq12d M322 M12 M=62 M2 M1
186 181 185 eqtrd M32 M122 M=62 M2 M1
187 186 oveq2d M(N2M1)32 M122 M=(N2M1)62 M2 M1
188 176 187 eqtrd M(N2 M)=(N2M1)62 M2 M1
189 188 oveq1d M(N2 M)(N2M1)=(N2M1)62 M2 M1(N2M1)
190 6re 6
191 59 140 nnmulcld M2 M2 M1
192 nndivre 62 M2 M162 M2 M1
193 190 191 192 sylancr M62 M2 M1
194 193 recnd M62 M2 M1
195 nnm1nn0 2 M12 M-1-10
196 140 195 syl M2 M-1-10
197 153 196 eqeltrrd M2M10
198 197 nn0red M2M1
199 140 nnred M2 M1
200 61 nnred MN
201 199 ltm1d M2 M-1-1<2 M1
202 153 201 eqbrtrrd M2M1<2 M1
203 198 199 202 ltled M2M12 M1
204 198 199 200 203 133 letrd M2M1N
205 nn0uz 0=0
206 197 205 eleqtrdi M2M10
207 elfz5 2M10N2M10N2M1N
208 206 100 207 syl2anc M2M10N2M1N
209 204 208 mpbird M2M10N
210 bccl2 2M10N(N2M1)
211 209 210 syl M(N2M1)
212 211 nnne0d M(N2M1)0
213 194 71 212 divcan3d M(N2M1)62 M2 M1(N2M1)=62 M2 M1
214 189 213 eqtrd M(N2 M)(N2M1)=62 M2 M1
215 214 oveq2d M1(N2 M)(N2M1)=162 M2 M1
216 107 71 112 212 recdivd M1(N2 M)(N2M1)=(N2M1)(N2 M)
217 191 nncnd M2 M2 M1
218 191 nnne0d M2 M2 M10
219 6cn 6
220 6nn 6
221 220 nnne0i 60
222 recdiv 6602 M2 M12 M2 M10162 M2 M1=2 M2 M16
223 219 221 222 mpanl12 2 M2 M12 M2 M10162 M2 M1=2 M2 M16
224 217 218 223 syl2anc M162 M2 M1=2 M2 M16
225 215 216 224 3eqtr3d M(N2M1)(N2 M)=2 M2 M16
226 114 118 225 3eqtrd McoeffPdegP1coeffPdegP=2 M2 M16
227 19 33 226 3eqtr3d Mk=1MtankπN2=2 M2 M16