Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  basellem3 Unicode version

Theorem basellem3 20818
 Description: Lemma for basel 20825. Using the binomial theorem and de Moivre's formula, we have the identity , so taking imaginary parts yields , where . (Contributed by Mario Carneiro, 30-Jul-2014.)
Hypotheses
Ref Expression
basel.n
basel.p
Assertion
Ref Expression
basellem3
Distinct variable groups:   ,,   ,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem basellem3
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tanrpcl 20365 . . . . . . . 8
21adantl 453 . . . . . . 7
32rpreccld 10614 . . . . . 6
43rpcnd 10606 . . . . 5
5 ax-icn 9005 . . . . . 6
65a1i 11 . . . . 5
7 basel.n . . . . . . 7
8 2nn 10089 . . . . . . . . 9
9 simpl 444 . . . . . . . . 9
10 nnmulcl 9979 . . . . . . . . 9
118, 9, 10sylancr 645 . . . . . . . 8
1211peano2nnd 9973 . . . . . . 7
137, 12syl5eqel 2488 . . . . . 6
1413nnnn0d 10230 . . . . 5
15 binom 12564 . . . . 5
164, 6, 14, 15syl3anc 1184 . . . 4
17 elioore 10902 . . . . . . . . . . 11
1817adantl 453 . . . . . . . . . 10
1918recoscld 12700 . . . . . . . . 9
2019recnd 9070 . . . . . . . 8
2118resincld 12699 . . . . . . . . . 10
2221recnd 9070 . . . . . . . . 9
23 mulcl 9030 . . . . . . . . 9
245, 22, 23sylancr 645 . . . . . . . 8
2520, 24addcld 9063 . . . . . . 7
26 sincosq1sgn 20359 . . . . . . . . . 10
2726adantl 453 . . . . . . . . 9
2827simpld 446 . . . . . . . 8
2928gt0ne0d 9547 . . . . . . 7
3025, 22, 29, 14expdivd 11492 . . . . . 6
3120, 24, 22, 29divdird 9784 . . . . . . . 8
3218recnd 9070 . . . . . . . . . . . 12
3327simprd 450 . . . . . . . . . . . . 13
3433gt0ne0d 9547 . . . . . . . . . . . 12
35 tanval 12684 . . . . . . . . . . . 12
3632, 34, 35syl2anc 643 . . . . . . . . . . 11
3736oveq2d 6056 . . . . . . . . . 10
3822, 20, 29, 34recdivd 9763 . . . . . . . . . 10
3937, 38eqtr2d 2437 . . . . . . . . 9
406, 22, 29divcan4d 9752 . . . . . . . . 9
4139, 40oveq12d 6058 . . . . . . . 8
4231, 41eqtrd 2436 . . . . . . 7
4342oveq1d 6055 . . . . . 6
4413nnzd 10330 . . . . . . . 8
45 demoivre 12756 . . . . . . . 8
4632, 44, 45syl2anc 643 . . . . . . 7
4746oveq1d 6055 . . . . . 6
4830, 43, 473eqtr3d 2444 . . . . 5
4913nnred 9971 . . . . . . . . 9
5049, 18remulcld 9072 . . . . . . . 8
5150recoscld 12700 . . . . . . 7
5251recnd 9070 . . . . . 6
5350resincld 12699 . . . . . . . 8
5453recnd 9070 . . . . . . 7
55 mulcl 9030 . . . . . . 7
565, 54, 55sylancr 645 . . . . . 6
5721, 28elrpd 10602 . . . . . . . 8
5857, 44rpexpcld 11501 . . . . . . 7
5958rpcnd 10606 . . . . . 6
6058rpne0d 10609 . . . . . 6
6152, 56, 59, 60divdird 9784 . . . . 5
626, 54, 59, 60divassd 9781 . . . . . 6
6362oveq2d 6056 . . . . 5
6448, 61, 633eqtrd 2440 . . . 4
6516, 64eqtr3d 2438 . . 3
6665fveq2d 5691 . 2
67 oveq2 6048 . . . . . . 7
68 oveq2 6048 . . . . . . . . 9
6968oveq2d 6056 . . . . . . . 8
70 oveq2 6048 . . . . . . . 8
7169, 70oveq12d 6058 . . . . . . 7
7267, 71oveq12d 6058 . . . . . 6
7372fveq2d 5691 . . . . 5
74 fzfid 11267 . . . . 5
75 2nn0 10194 . . . . . . . . . . . . 13
76 elfznn0 11039 . . . . . . . . . . . . . 14
7776adantl 453 . . . . . . . . . . . . 13
78 nn0mulcl 10212 . . . . . . . . . . . . 13
7975, 77, 78sylancr 645 . . . . . . . . . . . 12
8079nn0red 10231 . . . . . . . . . . 11
8111nnred 9971 . . . . . . . . . . . 12
8281adantr 452 . . . . . . . . . . 11
8349adantr 452 . . . . . . . . . . 11
84 elfzle2 11017 . . . . . . . . . . . . 13
8584adantl 453 . . . . . . . . . . . 12
8677nn0red 10231 . . . . . . . . . . . . 13
87 nnre 9963 . . . . . . . . . . . . . 14
8887ad2antrr 707 . . . . . . . . . . . . 13
89 2re 10025 . . . . . . . . . . . . . . 15
90 2pos 10038 . . . . . . . . . . . . . . 15
9189, 90pm3.2i 442 . . . . . . . . . . . . . 14
9291a1i 11 . . . . . . . . . . . . 13
93 lemul2 9819 . . . . . . . . . . . . 13
9486, 88, 92, 93syl3anc 1184 . . . . . . . . . . . 12
9585, 94mpbid 202 . . . . . . . . . . 11
9682lep1d 9898 . . . . . . . . . . . 12
9796, 7syl6breqr 4212 . . . . . . . . . . 11
9880, 82, 83, 95, 97letrd 9183 . . . . . . . . . 10
99 nn0uz 10476 . . . . . . . . . . . 12
10079, 99syl6eleq 2494 . . . . . . . . . . 11
10144adantr 452 . . . . . . . . . . 11
102 elfz5 11007 . . . . . . . . . . 11
103100, 101, 102syl2anc 643 . . . . . . . . . 10
10498, 103mpbird 224 . . . . . . . . 9
105 fznn0sub2 11042 . . . . . . . . 9
106104, 105syl 16 . . . . . . . 8
107106ex 424 . . . . . . 7
10813nncnd 9972 . . . . . . . . . . 11
109108adantr 452 . . . . . . . . . 10
110 2cn 10026 . . . . . . . . . . 11
111 elfzelz 11015 . . . . . . . . . . . . 13
112111zcnd 10332 . . . . . . . . . . . 12
113112ad2antrl 709 . . . . . . . . . . 11
114 mulcl 9030 . . . . . . . . . . 11
115110, 113, 114sylancr 645 . . . . . . . . . 10
116112ssriv 3312 . . . . . . . . . . . 12
117 simprr 734 . . . . . . . . . . . 12
118116, 117sseldi 3306 . . . . . . . . . . 11
119 mulcl 9030 . . . . . . . . . . 11
120110, 118, 119sylancr 645 . . . . . . . . . 10
121109, 115, 120subcanad 9410 . . . . . . . . 9
122 2ne0 10039 . . . . . . . . . . . 12
123110, 122pm3.2i 442 . . . . . . . . . . 11
124123a1i 11 . . . . . . . . . 10
125 mulcan 9615 . . . . . . . . . 10
126113, 118, 124, 125syl3anc 1184 . . . . . . . . 9
127121, 126bitrd 245 . . . . . . . 8
128127ex 424 . . . . . . 7
129107, 128dom2lem 7106 . . . . . 6
130 f1f1orn 5644 . . . . . 6
131129, 130syl 16 . . . . 5
132 oveq2 6048 . . . . . . . 8
133132oveq2d 6056 . . . . . . 7
134 eqid 2404 . . . . . . 7
135 ovex 6065 . . . . . . 7
136133, 134, 135fvmpt 5765 . . . . . 6
137136adantl 453 . . . . 5
138 f1f 5598 . . . . . . . . . . 11
139129, 138syl 16 . . . . . . . . . 10
140 frn 5556 . . . . . . . . . 10
141139, 140syl 16 . . . . . . . . 9
142141sselda 3308 . . . . . . . 8
143 bccl2 11569 . . . . . . . . . . 11
144143adantl 453 . . . . . . . . . 10
145144nncnd 9972 . . . . . . . . 9
1462rprecred 10615 . . . . . . . . . . . 12
147 fznn0sub 11041 . . . . . . . . . . . 12
148 reexpcl 11353 . . . . . . . . . . . 12
149146, 147, 148syl2an 464 . . . . . . . . . . 11
150149recnd 9070 . . . . . . . . . 10
151 elfznn0 11039 . . . . . . . . . . . 12
152151adantl 453 . . . . . . . . . . 11
153 expcl 11354 . . . . . . . . . . 11
1545, 152, 153sylancr 645 . . . . . . . . . 10
155150, 154mulcld 9064 . . . . . . . . 9
156145, 155mulcld 9064 . . . . . . . 8
157142, 156syldan 457 . . . . . . 7
158157imcld 11955 . . . . . 6
159158recnd 9070 . . . . 5
16073, 74, 131, 137, 159fsumf1o 12472 . . . 4
161 eldifi 3429 . . . . . . . 8
162144nnred 9971 . . . . . . . 8
163161, 162sylan2 461 . . . . . . 7
164161, 149sylan2 461 . . . . . . . 8
165 eldif 3290 . . . . . . . . 9
166 elfzelz 11015 . . . . . . . . . . . . . . 15
167166adantl 453 . . . . . . . . . . . . . 14
168 zeo 10311 . . . . . . . . . . . . . 14
169167, 168syl 16 . . . . . . . . . . . . 13
170 i2 11436 . . . . . . . . . . . . . . . . . 18
171170oveq1i 6050 . . . . . . . . . . . . . . . . 17
172 simprr 734 . . . . . . . . . . . . . . . . . . . 20
173151ad2antrl 709 . . . . . . . . . . . . . . . . . . . . 21
174 nn0re 10186 . . . . . . . . . . . . . . . . . . . . . 22
175 nn0ge0 10203 . . . . . . . . . . . . . . . . . . . . . 22
176 divge0 9835 . . . . . . . . . . . . . . . . . . . . . . 23
17789, 90, 176mpanr12 667 . . . . . . . . . . . . . . . . . . . . . 22
178174, 175, 177syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21
179173, 178syl 16 . . . . . . . . . . . . . . . . . . . 20
180 elnn0z 10250 . . . . . . . . . . . . . . . . . . . 20
181172, 179, 180sylanbrc 646 . . . . . . . . . . . . . . . . . . 19
182 expmul 11380 . . . . . . . . . . . . . . . . . . . 20
1835, 75, 182mp3an12 1269 . . . . . . . . . . . . . . . . . . 19
184181, 183syl 16 . . . . . . . . . . . . . . . . . 18
185173nn0cnd 10232 . . . . . . . . . . . . . . . . . . . 20
186 divcan2 9642 . . . . . . . . . . . . . . . . . . . . 21
187110, 122, 186mp3an23 1271 . . . . . . . . . . . . . . . . . . . 20
188185, 187syl 16 . . . . . . . . . . . . . . . . . . 19
189188oveq2d 6056 . . . . . . . . . . . . . . . . . 18
190184, 189eqtr3d 2438 . . . . . . . . . . . . . . . . 17
191171, 190syl5eqr 2450 . . . . . . . . . . . . . . . 16
192 1re 9046 . . . . . . . . . . . . . . . . . 18
193192renegcli 9318 . . . . . . . . . . . . . . . . 17
194 reexpcl 11353 . . . . . . . . . . . . . . . . 17
195193, 181, 194sylancr 645 . . . . . . . . . . . . . . . 16
196191, 195eqeltrrd 2479 . . . . . . . . . . . . . . 15
197196expr 599 . . . . . . . . . . . . . 14
198147ad2antrl 709 . . . . . . . . . . . . . . . . . . . 20
199 nn0re 10186 . . . . . . . . . . . . . . . . . . . . 21
200 nn0ge0 10203 . . . . . . . . . . . . . . . . . . . . 21
201 divge0 9835 . . . . . . . . . . . . . . . . . . . . . 22
20289, 90, 201mpanr12 667 . . . . . . . . . . . . . . . . . . . . 21
203199, 200, 202syl2anc 643 . . . . . . . . . . . . . . . . . . . 20
204198, 203syl 16 . . . . . . . . . . . . . . . . . . 19
205198nn0red 10231 . . . . . . . . . . . . . . . . . . . . . . 23
20649adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
207 peano2re 9195 . . . . . . . . . . . . . . . . . . . . . . . 24
208206, 207syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
209151ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . . . 25
210209, 175syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
211209nn0red 10231 . . . . . . . . . . . . . . . . . . . . . . . . 25
212206, 211subge02d 9574 . . . . . . . . . . . . . . . . . . . . . . . 24
213210, 212mpbid 202 . . . . . . . . . . . . . . . . . . . . . . 23
214206ltp1d 9897 . . . . . . . . . . . . . . . . . . . . . . 23
215205, 206, 208, 213, 214lelttrd 9184 . . . . . . . . . . . . . . . . . . . . . 22
216110mulid1i 9048 . . . . . . . . . . . . . . . . . . . . . . . . 25
217 df-2 10014 . . . . . . . . . . . . . . . . . . . . . . . . 25
218216, 217eqtr2i 2425 . . . . . . . . . . . . . . . . . . . . . . . 24
219218oveq2i 6051 . . . . . . . . . . . . . . . . . . . . . . 23
2207oveq1i 6050 . . . . . . . . . . . . . . . . . . . . . . . 24
22111nncnd 9972 . . . . . . . . . . . . . . . . . . . . . . . . . 26
222221adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25
223 ax-1cn 9004 . . . . . . . . . . . . . . . . . . . . . . . . . 26
224223a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25
225222, 224, 224addassd 9066 . . . . . . . . . . . . . . . . . . . . . . . 24
226220, 225syl5eq 2448 . . . . . . . . . . . . . . . . . . . . . . 23
227110a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24
228 nncn 9964 . . . . . . . . . . . . . . . . . . . . . . . . 25
229228ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . 24
230227, 229, 224adddid 9068 . . . . . . . . . . . . . . . . . . . . . . 23
231219, 226, 2303eqtr4a 2462 . . . . . . . . . . . . . . . . . . . . . 22
232215, 231breqtrd 4196 . . . . . . . . . . . . . . . . . . . . 21
233 nnz 10259 . . . . . . . . . . . . . . . . . . . . . . . . 25
234233ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . 24
235234peano2zd 10334 . . . . . . . . . . . . . . . . . . . . . . 23
236235zred 10331 . . . . . . . . . . . . . . . . . . . . . 22
23791a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
238 ltdivmul 9838 . . . . . . . . . . . . . . . . . . . . . 22
239205, 236, 237, 238syl3anc 1184 . . . . . . . . . . . . . . . . . . . . 21
240232, 239mpbird 224 . . . . . . . . . . . . . . . . . . . 20
241108adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26
242209nn0cnd 10232 . . . . . . . . . . . . . . . . . . . . . . . . . 26
243241, 242, 224pnpcan2d 9405 . . . . . . . . . . . . . . . . . . . . . . . . 25
244231oveq1d 6055 . . . . . . . . . . . . . . . . . . . . . . . . 25
245243, 244eqtr3d 2438 . . . . . . . . . . . . . . . . . . . . . . . 24
246245oveq1d 6055 . . . . . . . . . . . . . . . . . . . . . . 23
247235zcnd 10332 . . . . . . . . . . . . . . . . . . . . . . . . 25
248 mulcl 9030 . . . . . . . . . . . . . . . . . . . . . . . . 25
249110, 247, 248sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . 24
250 peano2cn 9194 . . . . . . . . . . . . . . . . . . . . . . . . 25
251242, 250syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
252123a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24
253 divsubdir 9666 . . . . . . . . . . . . . . . . . . . . . . . 24
254249, 251, 252, 253syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . 23
255122a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25
256247, 227, 255divcan3d 9751 . . . . . . . . . . . . . . . . . . . . . . . 24
257256oveq1d 6055 . . . . . . . . . . . . . . . . . . . . . . 23
258246, 254, 2573eqtrd 2440 . . . . . . . . . . . . . . . . . . . . . 22
259 simprr 734 . . . . . . . . . . . . . . . . . . . . . . 23
260235, 259zsubcld 10336 . . . . . . . . . . . . . . . . . . . . . 22
261258, 260eqeltrd 2478 . . . . . . . . . . . . . . . . . . . . 21
262 zleltp1 10282 . . . . . . . . . . . . . . . . . . . . 21
263261, 234, 262syl2anc 643 . . . . . . . . . . . . . . . . . . . 20
264240, 263mpbird 224 . . . . . . . . . . . . . . . . . . 19
265 0z 10249 . . . . . . . . . . . . . . . . . . . . 21
266265a1i 11 . . . . . . . . . . . . . . . . . . . 20
267 elfz 11005 . . . . . . . . . . . . . . . . . . . 20
268261, 266, 234, 267syl3anc 1184 . . . . . . . . . . . . . . . . . . 19
269204, 264, 268mpbir2and 889 . . . . . . . . . . . . . . . . . 18
270 oveq2 6048 . . . . . . . . . . . . . . . . . . . 20
271270oveq2d 6056 . . . . . . . . . . . . . . . . . . 19
272 ovex 6065 . . . . . . . . . . . . . . . . . . 19
273271, 134, 272fvmpt 5765 . . . . . . . . . . . . . . . . . 18
274269, 273syl 16 . . . . . . . . . . . . . . . . 17
275198nn0cnd 10232 . . . . . . . . . . . . . . . . . . 19
276275, 227, 255divcan2d 9748 . . . . . . . . . . . . . . . . . 18
277276oveq2d 6056 . . . . . . . . . . . . . . . . 17
278241, 242nncand 9372 . . . . . . . . . . . . . . . . 17
279274, 277, 2783eqtrd 2440 . . . . . . . . . . . . . . . 16
280 ffn 5550 . . . . . . . . . . . . . . . . . . 19
281139, 280syl 16 . . . . . . . . . . . . . . . . . 18
282281adantr 452 . . . . . . . . . . . . . . . . 17
283 fnfvelrn 5826 . . . . . . . . . . . . . . . . 17
284282, 269, 283syl2anc 643 . . . . . . . . . . . . . . . 16
285279, 284eqeltrrd 2479 . . . . . . . . . . . . . . 15
286285expr 599 . . . . . . . . . . . . . 14
287197, 286orim12d 812 . . . . . . . . . . . . 13
288169, 287mpd 15 . . . . . . . . . . . 12
289288orcomd 378 . . . . . . . . . . 11
290289ord 367 . . . . . . . . . 10
291290impr 603 . . . . . . . . 9
292165, 291sylan2b 462 . . . . . . . 8
293164, 292remulcld 9072 . . . . . . 7
294163, 293remulcld 9072 . . . . . 6
295294reim0d 11985 . . . . 5
296 fzfid 11267 . . . . 5
297141, 159, 295, 296fsumss 12474 . . . 4
29814adantr 452 . . . . . . . . . . . . . . 15
299 elfznn0 11039 . . . . . . . . . . . . . . . . . 18
300299adantl 453 . . . . . . . . . . . . . . . . 17
301 nn0mulcl 10212 . . . . . . . . . . . . . . . . 17
30275, 300, 301sylancr 645 . . . . . . . . . . . . . . . 16
303302nn0zd 10329 . . . . . . . . . . . . . . 15
304 bccl 11568 . . . . . . . . . . . . . . 15
305298, 303, 304syl2anc 643 . . . . . . . . . . . . . 14
306305nn0red 10231 . . . . . . . . . . . . 13
307 fznn0sub 11041 . . . . . . . . . . . . . . 15
308307adantl 453 . . . . . . . . . . . . . 14
309 reexpcl 11353 . . . . . . . . . . . . . 14
310193, 308, 309sylancr 645 . . . . . . . . . . . . 13
311306, 310remulcld 9072 . . . . . . . . . . . 12
312 2z 10268 . . . . . . . . . . . . . . . 16
313 znegcl 10269 . . . . . . . . . . . . . . . 16
314312, 313ax-mp 8 . . . . . . . . . . . . . . 15
315 rpexpcl 11355 . . . . . . . . . . . . . . 15
3162, 314, 315sylancl 644 . . . . . . . . . . . . . 14
317316rpred 10604 . . . . . . . . . . . . 13
318 reexpcl 11353 . . . . . . . . . . . . 13
319317, 299, 318syl2an 464 . . . . . . . . . . . 12
320311, 319remulcld 9072 . . . . . . . . . . 11
321320recnd 9070 . . . . . . . . . 10
322 mulcl 9030 . . . . . . . . . 10
3235, 321, 322sylancr 645 . . . . . . . . 9
324323addid2d 9223 . . . . . . . 8
325305nn0cnd 10232 . . . . . . . . . . 11
326310recnd 9070 . . . . . . . . . . 11
327319recnd 9070 . . . . . . . . . . 11
328325, 326, 327mulassd 9067 . . . . . . . . . 10
329328oveq2d 6056 . . . . . . . . 9
3305a1i 11 . . . . . . . . . 10
331326, 327mulcld 9064 . . . . . . . . . 10
332330, 325, 331mul12d 9231 . . . . . . . . 9
333329, 332eqtrd 2436 . . . . . . . 8
334 bccmpl 11555 . . . . . . . . . 10
335298, 303, 334syl2anc 643 . . . . . . . . 9
336108adantr 452 . . . . . . . . . . . . . 14
337302nn0cnd 10232 . . . . . . . . . . . . . 14
338336, 337nncand 9372 . . . . . . . . . . . . 13
339338oveq2d 6056 . . . . . . . . . . . 12
3402adantr 452 . . . . . . . . . . . . . . 15
341340rpcnd 10606 . . . . . . . . . . . . . 14
342 expneg 11344 . . . . . . . . . . . . . 14
343341, 302, 342syl2anc 643 . . . . . . . . . . . . 13
344300nn0cnd 10232 . . . . . . . . . . . . . . 15
345 mulneg1 9426 . . . . . . . . . . . . . . 15
346110, 344, 345sylancr