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 x. M ) + 1 )
basel.p 
|- P = ( t e. CC |-> sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( t ^ j ) ) )
basel.t 
|- T = ( n e. ( 1 ... M ) |-> ( ( tan ` ( ( n x. _pi ) / N ) ) ^ -u 2 ) )
Assertion basellem5 
|- ( M e. NN -> sum_ k e. ( 1 ... M ) ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) = ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / 6 ) )

Proof

Step Hyp Ref Expression
1 basel.n 
 |-  N = ( ( 2 x. M ) + 1 )
2 basel.p 
 |-  P = ( t e. CC |-> sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( t ^ j ) ) )
3 basel.t 
 |-  T = ( n e. ( 1 ... M ) |-> ( ( tan ` ( ( n x. _pi ) / N ) ) ^ -u 2 ) )
4 eqid 
 |-  ( coeff ` P ) = ( coeff ` P )
5 eqid 
 |-  ( deg ` P ) = ( deg ` P )
6 eqid 
 |-  ( `' P " { 0 } ) = ( `' P " { 0 } )
7 1 2 basellem2 
 |-  ( M e. NN -> ( P e. ( Poly ` CC ) /\ ( deg ` P ) = M /\ ( coeff ` P ) = ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ) )
8 7 simp1d 
 |-  ( M e. NN -> P e. ( Poly ` CC ) )
9 7 simp2d 
 |-  ( M e. NN -> ( deg ` P ) = M )
10 nnnn0 
 |-  ( M e. NN -> M e. NN0 )
11 hashfz1 
 |-  ( M e. NN0 -> ( # ` ( 1 ... M ) ) = M )
12 10 11 syl 
 |-  ( M e. NN -> ( # ` ( 1 ... M ) ) = M )
13 fzfid 
 |-  ( M e. NN -> ( 1 ... M ) e. Fin )
14 1 2 3 basellem4 
 |-  ( M e. NN -> T : ( 1 ... M ) -1-1-onto-> ( `' P " { 0 } ) )
15 13 14 hasheqf1od 
 |-  ( M e. NN -> ( # ` ( 1 ... M ) ) = ( # ` ( `' P " { 0 } ) ) )
16 9 12 15 3eqtr2rd 
 |-  ( M e. NN -> ( # ` ( `' P " { 0 } ) ) = ( deg ` P ) )
17 id 
 |-  ( M e. NN -> M e. NN )
18 9 17 eqeltrd 
 |-  ( M e. NN -> ( deg ` P ) e. NN )
19 4 5 6 8 16 18 vieta1 
 |-  ( M e. NN -> sum_ x e. ( `' P " { 0 } ) x = -u ( ( ( coeff ` P ) ` ( ( deg ` P ) - 1 ) ) / ( ( coeff ` P ) ` ( deg ` P ) ) ) )
20 id 
 |-  ( x = ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) -> x = ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) )
21 oveq1 
 |-  ( n = k -> ( n x. _pi ) = ( k x. _pi ) )
22 21 fvoveq1d 
 |-  ( n = k -> ( tan ` ( ( n x. _pi ) / N ) ) = ( tan ` ( ( k x. _pi ) / N ) ) )
23 22 oveq1d 
 |-  ( n = k -> ( ( tan ` ( ( n x. _pi ) / N ) ) ^ -u 2 ) = ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) )
24 ovex 
 |-  ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) e. _V
25 23 3 24 fvmpt 
 |-  ( k e. ( 1 ... M ) -> ( T ` k ) = ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) )
26 25 adantl 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( T ` k ) = ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) )
27 cnvimass 
 |-  ( `' P " { 0 } ) C_ dom P
28 plyf 
 |-  ( P e. ( Poly ` CC ) -> P : CC --> CC )
29 fdm 
 |-  ( P : CC --> CC -> dom P = CC )
30 8 28 29 3syl 
 |-  ( M e. NN -> dom P = CC )
31 27 30 sseqtrid 
 |-  ( M e. NN -> ( `' P " { 0 } ) C_ CC )
32 31 sselda 
 |-  ( ( M e. NN /\ x e. ( `' P " { 0 } ) ) -> x e. CC )
33 20 13 14 26 32 fsumf1o 
 |-  ( M e. NN -> sum_ x e. ( `' P " { 0 } ) x = sum_ k e. ( 1 ... M ) ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) )
34 7 simp3d 
 |-  ( M e. NN -> ( coeff ` P ) = ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) )
35 9 oveq1d 
 |-  ( M e. NN -> ( ( deg ` P ) - 1 ) = ( M - 1 ) )
36 34 35 fveq12d 
 |-  ( M e. NN -> ( ( coeff ` P ) ` ( ( deg ` P ) - 1 ) ) = ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` ( M - 1 ) ) )
37 nnm1nn0 
 |-  ( M e. NN -> ( M - 1 ) e. NN0 )
38 oveq2 
 |-  ( n = ( M - 1 ) -> ( 2 x. n ) = ( 2 x. ( M - 1 ) ) )
39 38 oveq2d 
 |-  ( n = ( M - 1 ) -> ( N _C ( 2 x. n ) ) = ( N _C ( 2 x. ( M - 1 ) ) ) )
40 oveq2 
 |-  ( n = ( M - 1 ) -> ( M - n ) = ( M - ( M - 1 ) ) )
41 40 oveq2d 
 |-  ( n = ( M - 1 ) -> ( -u 1 ^ ( M - n ) ) = ( -u 1 ^ ( M - ( M - 1 ) ) ) )
42 39 41 oveq12d 
 |-  ( n = ( M - 1 ) -> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) = ( ( N _C ( 2 x. ( M - 1 ) ) ) x. ( -u 1 ^ ( M - ( M - 1 ) ) ) ) )
43 eqid 
 |-  ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) = ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) )
44 ovex 
 |-  ( ( N _C ( 2 x. ( M - 1 ) ) ) x. ( -u 1 ^ ( M - ( M - 1 ) ) ) ) e. _V
45 42 43 44 fvmpt 
 |-  ( ( M - 1 ) e. NN0 -> ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` ( M - 1 ) ) = ( ( N _C ( 2 x. ( M - 1 ) ) ) x. ( -u 1 ^ ( M - ( M - 1 ) ) ) ) )
46 37 45 syl 
 |-  ( M e. NN -> ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` ( M - 1 ) ) = ( ( N _C ( 2 x. ( M - 1 ) ) ) x. ( -u 1 ^ ( M - ( M - 1 ) ) ) ) )
47 nncn 
 |-  ( M e. NN -> M e. CC )
48 ax-1cn 
 |-  1 e. CC
49 nncan 
 |-  ( ( M e. CC /\ 1 e. CC ) -> ( M - ( M - 1 ) ) = 1 )
50 47 48 49 sylancl 
 |-  ( M e. NN -> ( M - ( M - 1 ) ) = 1 )
51 50 oveq2d 
 |-  ( M e. NN -> ( -u 1 ^ ( M - ( M - 1 ) ) ) = ( -u 1 ^ 1 ) )
52 neg1cn 
 |-  -u 1 e. CC
53 exp1 
 |-  ( -u 1 e. CC -> ( -u 1 ^ 1 ) = -u 1 )
54 52 53 ax-mp 
 |-  ( -u 1 ^ 1 ) = -u 1
55 51 54 eqtrdi 
 |-  ( M e. NN -> ( -u 1 ^ ( M - ( M - 1 ) ) ) = -u 1 )
56 55 oveq2d 
 |-  ( M e. NN -> ( ( N _C ( 2 x. ( M - 1 ) ) ) x. ( -u 1 ^ ( M - ( M - 1 ) ) ) ) = ( ( N _C ( 2 x. ( M - 1 ) ) ) x. -u 1 ) )
57 2nn 
 |-  2 e. NN
58 nnmulcl 
 |-  ( ( 2 e. NN /\ M e. NN ) -> ( 2 x. M ) e. NN )
59 57 58 mpan 
 |-  ( M e. NN -> ( 2 x. M ) e. NN )
60 59 peano2nnd 
 |-  ( M e. NN -> ( ( 2 x. M ) + 1 ) e. NN )
61 1 60 eqeltrid 
 |-  ( M e. NN -> N e. NN )
62 61 nnnn0d 
 |-  ( M e. NN -> N e. NN0 )
63 2z 
 |-  2 e. ZZ
64 nnz 
 |-  ( M e. NN -> M e. ZZ )
65 peano2zm 
 |-  ( M e. ZZ -> ( M - 1 ) e. ZZ )
66 64 65 syl 
 |-  ( M e. NN -> ( M - 1 ) e. ZZ )
67 zmulcl 
 |-  ( ( 2 e. ZZ /\ ( M - 1 ) e. ZZ ) -> ( 2 x. ( M - 1 ) ) e. ZZ )
68 63 66 67 sylancr 
 |-  ( M e. NN -> ( 2 x. ( M - 1 ) ) e. ZZ )
69 bccl 
 |-  ( ( N e. NN0 /\ ( 2 x. ( M - 1 ) ) e. ZZ ) -> ( N _C ( 2 x. ( M - 1 ) ) ) e. NN0 )
70 62 68 69 syl2anc 
 |-  ( M e. NN -> ( N _C ( 2 x. ( M - 1 ) ) ) e. NN0 )
71 70 nn0cnd 
 |-  ( M e. NN -> ( N _C ( 2 x. ( M - 1 ) ) ) e. CC )
72 mulcom 
 |-  ( ( ( N _C ( 2 x. ( M - 1 ) ) ) e. CC /\ -u 1 e. CC ) -> ( ( N _C ( 2 x. ( M - 1 ) ) ) x. -u 1 ) = ( -u 1 x. ( N _C ( 2 x. ( M - 1 ) ) ) ) )
73 71 52 72 sylancl 
 |-  ( M e. NN -> ( ( N _C ( 2 x. ( M - 1 ) ) ) x. -u 1 ) = ( -u 1 x. ( N _C ( 2 x. ( M - 1 ) ) ) ) )
74 71 mulm1d 
 |-  ( M e. NN -> ( -u 1 x. ( N _C ( 2 x. ( M - 1 ) ) ) ) = -u ( N _C ( 2 x. ( M - 1 ) ) ) )
75 56 73 74 3eqtrd 
 |-  ( M e. NN -> ( ( N _C ( 2 x. ( M - 1 ) ) ) x. ( -u 1 ^ ( M - ( M - 1 ) ) ) ) = -u ( N _C ( 2 x. ( M - 1 ) ) ) )
76 36 46 75 3eqtrd 
 |-  ( M e. NN -> ( ( coeff ` P ) ` ( ( deg ` P ) - 1 ) ) = -u ( N _C ( 2 x. ( M - 1 ) ) ) )
77 71 negcld 
 |-  ( M e. NN -> -u ( N _C ( 2 x. ( M - 1 ) ) ) e. CC )
78 76 77 eqeltrd 
 |-  ( M e. NN -> ( ( coeff ` P ) ` ( ( deg ` P ) - 1 ) ) e. CC )
79 34 9 fveq12d 
 |-  ( M e. NN -> ( ( coeff ` P ) ` ( deg ` P ) ) = ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` M ) )
80 oveq2 
 |-  ( n = M -> ( 2 x. n ) = ( 2 x. M ) )
81 80 oveq2d 
 |-  ( n = M -> ( N _C ( 2 x. n ) ) = ( N _C ( 2 x. M ) ) )
82 oveq2 
 |-  ( n = M -> ( M - n ) = ( M - M ) )
83 82 oveq2d 
 |-  ( n = M -> ( -u 1 ^ ( M - n ) ) = ( -u 1 ^ ( M - M ) ) )
84 81 83 oveq12d 
 |-  ( n = M -> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) = ( ( N _C ( 2 x. M ) ) x. ( -u 1 ^ ( M - M ) ) ) )
85 ovex 
 |-  ( ( N _C ( 2 x. M ) ) x. ( -u 1 ^ ( M - M ) ) ) e. _V
86 84 43 85 fvmpt 
 |-  ( M e. NN0 -> ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` M ) = ( ( N _C ( 2 x. M ) ) x. ( -u 1 ^ ( M - M ) ) ) )
87 10 86 syl 
 |-  ( M e. NN -> ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` M ) = ( ( N _C ( 2 x. M ) ) x. ( -u 1 ^ ( M - M ) ) ) )
88 47 subidd 
 |-  ( M e. NN -> ( M - M ) = 0 )
89 88 oveq2d 
 |-  ( M e. NN -> ( -u 1 ^ ( M - M ) ) = ( -u 1 ^ 0 ) )
90 exp0 
 |-  ( -u 1 e. CC -> ( -u 1 ^ 0 ) = 1 )
91 52 90 ax-mp 
 |-  ( -u 1 ^ 0 ) = 1
92 89 91 eqtrdi 
 |-  ( M e. NN -> ( -u 1 ^ ( M - M ) ) = 1 )
93 92 oveq2d 
 |-  ( M e. NN -> ( ( N _C ( 2 x. M ) ) x. ( -u 1 ^ ( M - M ) ) ) = ( ( N _C ( 2 x. M ) ) x. 1 ) )
94 fz1ssfz0 
 |-  ( 1 ... N ) C_ ( 0 ... N )
95 59 nnred 
 |-  ( M e. NN -> ( 2 x. M ) e. RR )
96 95 lep1d 
 |-  ( M e. NN -> ( 2 x. M ) <_ ( ( 2 x. M ) + 1 ) )
97 96 1 breqtrrdi 
 |-  ( M e. NN -> ( 2 x. M ) <_ N )
98 nnuz 
 |-  NN = ( ZZ>= ` 1 )
99 59 98 eleqtrdi 
 |-  ( M e. NN -> ( 2 x. M ) e. ( ZZ>= ` 1 ) )
100 61 nnzd 
 |-  ( M e. NN -> N e. ZZ )
101 elfz5 
 |-  ( ( ( 2 x. M ) e. ( ZZ>= ` 1 ) /\ N e. ZZ ) -> ( ( 2 x. M ) e. ( 1 ... N ) <-> ( 2 x. M ) <_ N ) )
102 99 100 101 syl2anc 
 |-  ( M e. NN -> ( ( 2 x. M ) e. ( 1 ... N ) <-> ( 2 x. M ) <_ N ) )
103 97 102 mpbird 
 |-  ( M e. NN -> ( 2 x. M ) e. ( 1 ... N ) )
104 94 103 sselid 
 |-  ( M e. NN -> ( 2 x. M ) e. ( 0 ... N ) )
105 bccl2 
 |-  ( ( 2 x. M ) e. ( 0 ... N ) -> ( N _C ( 2 x. M ) ) e. NN )
106 104 105 syl 
 |-  ( M e. NN -> ( N _C ( 2 x. M ) ) e. NN )
107 106 nncnd 
 |-  ( M e. NN -> ( N _C ( 2 x. M ) ) e. CC )
108 107 mulid1d 
 |-  ( M e. NN -> ( ( N _C ( 2 x. M ) ) x. 1 ) = ( N _C ( 2 x. M ) ) )
109 93 108 eqtrd 
 |-  ( M e. NN -> ( ( N _C ( 2 x. M ) ) x. ( -u 1 ^ ( M - M ) ) ) = ( N _C ( 2 x. M ) ) )
110 79 87 109 3eqtrd 
 |-  ( M e. NN -> ( ( coeff ` P ) ` ( deg ` P ) ) = ( N _C ( 2 x. M ) ) )
111 110 107 eqeltrd 
 |-  ( M e. NN -> ( ( coeff ` P ) ` ( deg ` P ) ) e. CC )
112 106 nnne0d 
 |-  ( M e. NN -> ( N _C ( 2 x. M ) ) =/= 0 )
113 110 112 eqnetrd 
 |-  ( M e. NN -> ( ( coeff ` P ) ` ( deg ` P ) ) =/= 0 )
114 78 111 113 divnegd 
 |-  ( M e. NN -> -u ( ( ( coeff ` P ) ` ( ( deg ` P ) - 1 ) ) / ( ( coeff ` P ) ` ( deg ` P ) ) ) = ( -u ( ( coeff ` P ) ` ( ( deg ` P ) - 1 ) ) / ( ( coeff ` P ) ` ( deg ` P ) ) ) )
115 76 negeqd 
 |-  ( M e. NN -> -u ( ( coeff ` P ) ` ( ( deg ` P ) - 1 ) ) = -u -u ( N _C ( 2 x. ( M - 1 ) ) ) )
116 71 negnegd 
 |-  ( M e. NN -> -u -u ( N _C ( 2 x. ( M - 1 ) ) ) = ( N _C ( 2 x. ( M - 1 ) ) ) )
117 115 116 eqtrd 
 |-  ( M e. NN -> -u ( ( coeff ` P ) ` ( ( deg ` P ) - 1 ) ) = ( N _C ( 2 x. ( M - 1 ) ) ) )
118 117 110 oveq12d 
 |-  ( M e. NN -> ( -u ( ( coeff ` P ) ` ( ( deg ` P ) - 1 ) ) / ( ( coeff ` P ) ` ( deg ` P ) ) ) = ( ( N _C ( 2 x. ( M - 1 ) ) ) / ( N _C ( 2 x. M ) ) ) )
119 bcm1k 
 |-  ( ( 2 x. M ) e. ( 1 ... N ) -> ( N _C ( 2 x. M ) ) = ( ( N _C ( ( 2 x. M ) - 1 ) ) x. ( ( N - ( ( 2 x. M ) - 1 ) ) / ( 2 x. M ) ) ) )
120 103 119 syl 
 |-  ( M e. NN -> ( N _C ( 2 x. M ) ) = ( ( N _C ( ( 2 x. M ) - 1 ) ) x. ( ( N - ( ( 2 x. M ) - 1 ) ) / ( 2 x. M ) ) ) )
121 59 nncnd 
 |-  ( M e. NN -> ( 2 x. M ) e. CC )
122 1cnd 
 |-  ( M e. NN -> 1 e. CC )
123 121 122 122 pnncand 
 |-  ( M e. NN -> ( ( ( 2 x. M ) + 1 ) - ( ( 2 x. M ) - 1 ) ) = ( 1 + 1 ) )
124 1 oveq1i 
 |-  ( N - ( ( 2 x. M ) - 1 ) ) = ( ( ( 2 x. M ) + 1 ) - ( ( 2 x. M ) - 1 ) )
125 df-2 
 |-  2 = ( 1 + 1 )
126 123 124 125 3eqtr4g 
 |-  ( M e. NN -> ( N - ( ( 2 x. M ) - 1 ) ) = 2 )
127 2nn0 
 |-  2 e. NN0
128 126 127 eqeltrdi 
 |-  ( M e. NN -> ( N - ( ( 2 x. M ) - 1 ) ) e. NN0 )
129 nnm1nn0 
 |-  ( ( 2 x. M ) e. NN -> ( ( 2 x. M ) - 1 ) e. NN0 )
130 59 129 syl 
 |-  ( M e. NN -> ( ( 2 x. M ) - 1 ) e. NN0 )
131 nn0sub 
 |-  ( ( ( ( 2 x. M ) - 1 ) e. NN0 /\ N e. NN0 ) -> ( ( ( 2 x. M ) - 1 ) <_ N <-> ( N - ( ( 2 x. M ) - 1 ) ) e. NN0 ) )
132 130 62 131 syl2anc 
 |-  ( M e. NN -> ( ( ( 2 x. M ) - 1 ) <_ N <-> ( N - ( ( 2 x. M ) - 1 ) ) e. NN0 ) )
133 128 132 mpbird 
 |-  ( M e. NN -> ( ( 2 x. M ) - 1 ) <_ N )
134 47 2timesd 
 |-  ( M e. NN -> ( 2 x. M ) = ( M + M ) )
135 134 oveq1d 
 |-  ( M e. NN -> ( ( 2 x. M ) - 1 ) = ( ( M + M ) - 1 ) )
136 47 47 122 addsubd 
 |-  ( M e. NN -> ( ( M + M ) - 1 ) = ( ( M - 1 ) + M ) )
137 135 136 eqtrd 
 |-  ( M e. NN -> ( ( 2 x. M ) - 1 ) = ( ( M - 1 ) + M ) )
138 nn0nnaddcl 
 |-  ( ( ( M - 1 ) e. NN0 /\ M e. NN ) -> ( ( M - 1 ) + M ) e. NN )
139 37 138 mpancom 
 |-  ( M e. NN -> ( ( M - 1 ) + M ) e. NN )
140 137 139 eqeltrd 
 |-  ( M e. NN -> ( ( 2 x. M ) - 1 ) e. NN )
141 140 98 eleqtrdi 
 |-  ( M e. NN -> ( ( 2 x. M ) - 1 ) e. ( ZZ>= ` 1 ) )
142 elfz5 
 |-  ( ( ( ( 2 x. M ) - 1 ) e. ( ZZ>= ` 1 ) /\ N e. ZZ ) -> ( ( ( 2 x. M ) - 1 ) e. ( 1 ... N ) <-> ( ( 2 x. M ) - 1 ) <_ N ) )
143 141 100 142 syl2anc 
 |-  ( M e. NN -> ( ( ( 2 x. M ) - 1 ) e. ( 1 ... N ) <-> ( ( 2 x. M ) - 1 ) <_ N ) )
144 133 143 mpbird 
 |-  ( M e. NN -> ( ( 2 x. M ) - 1 ) e. ( 1 ... N ) )
145 bcm1k 
 |-  ( ( ( 2 x. M ) - 1 ) e. ( 1 ... N ) -> ( N _C ( ( 2 x. M ) - 1 ) ) = ( ( N _C ( ( ( 2 x. M ) - 1 ) - 1 ) ) x. ( ( N - ( ( ( 2 x. M ) - 1 ) - 1 ) ) / ( ( 2 x. M ) - 1 ) ) ) )
146 144 145 syl 
 |-  ( M e. NN -> ( N _C ( ( 2 x. M ) - 1 ) ) = ( ( N _C ( ( ( 2 x. M ) - 1 ) - 1 ) ) x. ( ( N - ( ( ( 2 x. M ) - 1 ) - 1 ) ) / ( ( 2 x. M ) - 1 ) ) ) )
147 48 2timesi 
 |-  ( 2 x. 1 ) = ( 1 + 1 )
148 147 eqcomi 
 |-  ( 1 + 1 ) = ( 2 x. 1 )
149 148 oveq2i 
 |-  ( ( 2 x. M ) - ( 1 + 1 ) ) = ( ( 2 x. M ) - ( 2 x. 1 ) )
150 121 122 122 subsub4d 
 |-  ( M e. NN -> ( ( ( 2 x. M ) - 1 ) - 1 ) = ( ( 2 x. M ) - ( 1 + 1 ) ) )
151 2cnd 
 |-  ( M e. NN -> 2 e. CC )
152 151 47 122 subdid 
 |-  ( M e. NN -> ( 2 x. ( M - 1 ) ) = ( ( 2 x. M ) - ( 2 x. 1 ) ) )
153 149 150 152 3eqtr4a 
 |-  ( M e. NN -> ( ( ( 2 x. M ) - 1 ) - 1 ) = ( 2 x. ( M - 1 ) ) )
154 153 oveq2d 
 |-  ( M e. NN -> ( N _C ( ( ( 2 x. M ) - 1 ) - 1 ) ) = ( N _C ( 2 x. ( M - 1 ) ) ) )
155 61 nncnd 
 |-  ( M e. NN -> N e. CC )
156 140 nncnd 
 |-  ( M e. NN -> ( ( 2 x. M ) - 1 ) e. CC )
157 155 156 122 subsubd 
 |-  ( M e. NN -> ( N - ( ( ( 2 x. M ) - 1 ) - 1 ) ) = ( ( N - ( ( 2 x. M ) - 1 ) ) + 1 ) )
158 126 oveq1d 
 |-  ( M e. NN -> ( ( N - ( ( 2 x. M ) - 1 ) ) + 1 ) = ( 2 + 1 ) )
159 df-3 
 |-  3 = ( 2 + 1 )
160 158 159 eqtr4di 
 |-  ( M e. NN -> ( ( N - ( ( 2 x. M ) - 1 ) ) + 1 ) = 3 )
161 157 160 eqtrd 
 |-  ( M e. NN -> ( N - ( ( ( 2 x. M ) - 1 ) - 1 ) ) = 3 )
162 161 oveq1d 
 |-  ( M e. NN -> ( ( N - ( ( ( 2 x. M ) - 1 ) - 1 ) ) / ( ( 2 x. M ) - 1 ) ) = ( 3 / ( ( 2 x. M ) - 1 ) ) )
163 154 162 oveq12d 
 |-  ( M e. NN -> ( ( N _C ( ( ( 2 x. M ) - 1 ) - 1 ) ) x. ( ( N - ( ( ( 2 x. M ) - 1 ) - 1 ) ) / ( ( 2 x. M ) - 1 ) ) ) = ( ( N _C ( 2 x. ( M - 1 ) ) ) x. ( 3 / ( ( 2 x. M ) - 1 ) ) ) )
164 146 163 eqtrd 
 |-  ( M e. NN -> ( N _C ( ( 2 x. M ) - 1 ) ) = ( ( N _C ( 2 x. ( M - 1 ) ) ) x. ( 3 / ( ( 2 x. M ) - 1 ) ) ) )
165 126 oveq1d 
 |-  ( M e. NN -> ( ( N - ( ( 2 x. M ) - 1 ) ) / ( 2 x. M ) ) = ( 2 / ( 2 x. M ) ) )
166 164 165 oveq12d 
 |-  ( M e. NN -> ( ( N _C ( ( 2 x. M ) - 1 ) ) x. ( ( N - ( ( 2 x. M ) - 1 ) ) / ( 2 x. M ) ) ) = ( ( ( N _C ( 2 x. ( M - 1 ) ) ) x. ( 3 / ( ( 2 x. M ) - 1 ) ) ) x. ( 2 / ( 2 x. M ) ) ) )
167 3re 
 |-  3 e. RR
168 nndivre 
 |-  ( ( 3 e. RR /\ ( ( 2 x. M ) - 1 ) e. NN ) -> ( 3 / ( ( 2 x. M ) - 1 ) ) e. RR )
169 167 140 168 sylancr 
 |-  ( M e. NN -> ( 3 / ( ( 2 x. M ) - 1 ) ) e. RR )
170 169 recnd 
 |-  ( M e. NN -> ( 3 / ( ( 2 x. M ) - 1 ) ) e. CC )
171 2re 
 |-  2 e. RR
172 nndivre 
 |-  ( ( 2 e. RR /\ ( 2 x. M ) e. NN ) -> ( 2 / ( 2 x. M ) ) e. RR )
173 171 59 172 sylancr 
 |-  ( M e. NN -> ( 2 / ( 2 x. M ) ) e. RR )
174 173 recnd 
 |-  ( M e. NN -> ( 2 / ( 2 x. M ) ) e. CC )
175 71 170 174 mulassd 
 |-  ( M e. NN -> ( ( ( N _C ( 2 x. ( M - 1 ) ) ) x. ( 3 / ( ( 2 x. M ) - 1 ) ) ) x. ( 2 / ( 2 x. M ) ) ) = ( ( N _C ( 2 x. ( M - 1 ) ) ) x. ( ( 3 / ( ( 2 x. M ) - 1 ) ) x. ( 2 / ( 2 x. M ) ) ) ) )
176 120 166 175 3eqtrd 
 |-  ( M e. NN -> ( N _C ( 2 x. M ) ) = ( ( N _C ( 2 x. ( M - 1 ) ) ) x. ( ( 3 / ( ( 2 x. M ) - 1 ) ) x. ( 2 / ( 2 x. M ) ) ) ) )
177 3cn 
 |-  3 e. CC
178 177 a1i 
 |-  ( M e. NN -> 3 e. CC )
179 140 nnne0d 
 |-  ( M e. NN -> ( ( 2 x. M ) - 1 ) =/= 0 )
180 59 nnne0d 
 |-  ( M e. NN -> ( 2 x. M ) =/= 0 )
181 178 156 151 121 179 180 divmuldivd 
 |-  ( M e. NN -> ( ( 3 / ( ( 2 x. M ) - 1 ) ) x. ( 2 / ( 2 x. M ) ) ) = ( ( 3 x. 2 ) / ( ( ( 2 x. M ) - 1 ) x. ( 2 x. M ) ) ) )
182 3t2e6 
 |-  ( 3 x. 2 ) = 6
183 182 a1i 
 |-  ( M e. NN -> ( 3 x. 2 ) = 6 )
184 156 121 mulcomd 
 |-  ( M e. NN -> ( ( ( 2 x. M ) - 1 ) x. ( 2 x. M ) ) = ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) )
185 183 184 oveq12d 
 |-  ( M e. NN -> ( ( 3 x. 2 ) / ( ( ( 2 x. M ) - 1 ) x. ( 2 x. M ) ) ) = ( 6 / ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) ) )
186 181 185 eqtrd 
 |-  ( M e. NN -> ( ( 3 / ( ( 2 x. M ) - 1 ) ) x. ( 2 / ( 2 x. M ) ) ) = ( 6 / ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) ) )
187 186 oveq2d 
 |-  ( M e. NN -> ( ( N _C ( 2 x. ( M - 1 ) ) ) x. ( ( 3 / ( ( 2 x. M ) - 1 ) ) x. ( 2 / ( 2 x. M ) ) ) ) = ( ( N _C ( 2 x. ( M - 1 ) ) ) x. ( 6 / ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) ) ) )
188 176 187 eqtrd 
 |-  ( M e. NN -> ( N _C ( 2 x. M ) ) = ( ( N _C ( 2 x. ( M - 1 ) ) ) x. ( 6 / ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) ) ) )
189 188 oveq1d 
 |-  ( M e. NN -> ( ( N _C ( 2 x. M ) ) / ( N _C ( 2 x. ( M - 1 ) ) ) ) = ( ( ( N _C ( 2 x. ( M - 1 ) ) ) x. ( 6 / ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) ) ) / ( N _C ( 2 x. ( M - 1 ) ) ) ) )
190 6re 
 |-  6 e. RR
191 59 140 nnmulcld 
 |-  ( M e. NN -> ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) e. NN )
192 nndivre 
 |-  ( ( 6 e. RR /\ ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) e. NN ) -> ( 6 / ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) ) e. RR )
193 190 191 192 sylancr 
 |-  ( M e. NN -> ( 6 / ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) ) e. RR )
194 193 recnd 
 |-  ( M e. NN -> ( 6 / ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) ) e. CC )
195 nnm1nn0 
 |-  ( ( ( 2 x. M ) - 1 ) e. NN -> ( ( ( 2 x. M ) - 1 ) - 1 ) e. NN0 )
196 140 195 syl 
 |-  ( M e. NN -> ( ( ( 2 x. M ) - 1 ) - 1 ) e. NN0 )
197 153 196 eqeltrrd 
 |-  ( M e. NN -> ( 2 x. ( M - 1 ) ) e. NN0 )
198 197 nn0red 
 |-  ( M e. NN -> ( 2 x. ( M - 1 ) ) e. RR )
199 140 nnred 
 |-  ( M e. NN -> ( ( 2 x. M ) - 1 ) e. RR )
200 61 nnred 
 |-  ( M e. NN -> N e. RR )
201 199 ltm1d 
 |-  ( M e. NN -> ( ( ( 2 x. M ) - 1 ) - 1 ) < ( ( 2 x. M ) - 1 ) )
202 153 201 eqbrtrrd 
 |-  ( M e. NN -> ( 2 x. ( M - 1 ) ) < ( ( 2 x. M ) - 1 ) )
203 198 199 202 ltled 
 |-  ( M e. NN -> ( 2 x. ( M - 1 ) ) <_ ( ( 2 x. M ) - 1 ) )
204 198 199 200 203 133 letrd 
 |-  ( M e. NN -> ( 2 x. ( M - 1 ) ) <_ N )
205 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
206 197 205 eleqtrdi 
 |-  ( M e. NN -> ( 2 x. ( M - 1 ) ) e. ( ZZ>= ` 0 ) )
207 elfz5 
 |-  ( ( ( 2 x. ( M - 1 ) ) e. ( ZZ>= ` 0 ) /\ N e. ZZ ) -> ( ( 2 x. ( M - 1 ) ) e. ( 0 ... N ) <-> ( 2 x. ( M - 1 ) ) <_ N ) )
208 206 100 207 syl2anc 
 |-  ( M e. NN -> ( ( 2 x. ( M - 1 ) ) e. ( 0 ... N ) <-> ( 2 x. ( M - 1 ) ) <_ N ) )
209 204 208 mpbird 
 |-  ( M e. NN -> ( 2 x. ( M - 1 ) ) e. ( 0 ... N ) )
210 bccl2 
 |-  ( ( 2 x. ( M - 1 ) ) e. ( 0 ... N ) -> ( N _C ( 2 x. ( M - 1 ) ) ) e. NN )
211 209 210 syl 
 |-  ( M e. NN -> ( N _C ( 2 x. ( M - 1 ) ) ) e. NN )
212 211 nnne0d 
 |-  ( M e. NN -> ( N _C ( 2 x. ( M - 1 ) ) ) =/= 0 )
213 194 71 212 divcan3d 
 |-  ( M e. NN -> ( ( ( N _C ( 2 x. ( M - 1 ) ) ) x. ( 6 / ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) ) ) / ( N _C ( 2 x. ( M - 1 ) ) ) ) = ( 6 / ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) ) )
214 189 213 eqtrd 
 |-  ( M e. NN -> ( ( N _C ( 2 x. M ) ) / ( N _C ( 2 x. ( M - 1 ) ) ) ) = ( 6 / ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) ) )
215 214 oveq2d 
 |-  ( M e. NN -> ( 1 / ( ( N _C ( 2 x. M ) ) / ( N _C ( 2 x. ( M - 1 ) ) ) ) ) = ( 1 / ( 6 / ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) ) ) )
216 107 71 112 212 recdivd 
 |-  ( M e. NN -> ( 1 / ( ( N _C ( 2 x. M ) ) / ( N _C ( 2 x. ( M - 1 ) ) ) ) ) = ( ( N _C ( 2 x. ( M - 1 ) ) ) / ( N _C ( 2 x. M ) ) ) )
217 191 nncnd 
 |-  ( M e. NN -> ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) e. CC )
218 191 nnne0d 
 |-  ( M e. NN -> ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) =/= 0 )
219 6cn 
 |-  6 e. CC
220 6nn 
 |-  6 e. NN
221 220 nnne0i 
 |-  6 =/= 0
222 recdiv 
 |-  ( ( ( 6 e. CC /\ 6 =/= 0 ) /\ ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) e. CC /\ ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) =/= 0 ) ) -> ( 1 / ( 6 / ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) ) ) = ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / 6 ) )
223 219 221 222 mpanl12 
 |-  ( ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) e. CC /\ ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) =/= 0 ) -> ( 1 / ( 6 / ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) ) ) = ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / 6 ) )
224 217 218 223 syl2anc 
 |-  ( M e. NN -> ( 1 / ( 6 / ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) ) ) = ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / 6 ) )
225 215 216 224 3eqtr3d 
 |-  ( M e. NN -> ( ( N _C ( 2 x. ( M - 1 ) ) ) / ( N _C ( 2 x. M ) ) ) = ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / 6 ) )
226 114 118 225 3eqtrd 
 |-  ( M e. NN -> -u ( ( ( coeff ` P ) ` ( ( deg ` P ) - 1 ) ) / ( ( coeff ` P ) ` ( deg ` P ) ) ) = ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / 6 ) )
227 19 33 226 3eqtr3d 
 |-  ( M e. NN -> sum_ k e. ( 1 ... M ) ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) = ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / 6 ) )