Metamath Proof Explorer

Theorem basellem8

Description: Lemma for basel . The function F of partial sums of the inverse squares is bounded below by J and above by K , obtained by summing the inequality cot ^ 2 x <_ 1 / x ^ 2 <_ csc ^ 2 x = cot ^ 2 x + 1 over the M roots of the polynomial P , and applying the identity basellem5 . (Contributed by Mario Carneiro, 29-Jul-2014)

Ref Expression
Hypotheses basel.g 
|- G = ( n e. NN |-> ( 1 / ( ( 2 x. n ) + 1 ) ) )
basel.f 
|- F = seq 1 ( + , ( n e. NN |-> ( n ^ -u 2 ) ) )
basel.h 
|- H = ( ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) oF x. ( ( NN X. { 1 } ) oF - G ) )
basel.j 
|- J = ( H oF x. ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) )
basel.k 
|- K = ( H oF x. ( ( NN X. { 1 } ) oF + G ) )
basellem8.n 
|- N = ( ( 2 x. M ) + 1 )
Assertion basellem8 
|- ( M e. NN -> ( ( J ` M ) <_ ( F ` M ) /\ ( F ` M ) <_ ( K ` M ) ) )

Proof

Step Hyp Ref Expression
1 basel.g 
 |-  G = ( n e. NN |-> ( 1 / ( ( 2 x. n ) + 1 ) ) )
2 basel.f 
 |-  F = seq 1 ( + , ( n e. NN |-> ( n ^ -u 2 ) ) )
3 basel.h 
 |-  H = ( ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) oF x. ( ( NN X. { 1 } ) oF - G ) )
4 basel.j 
 |-  J = ( H oF x. ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) )
5 basel.k 
 |-  K = ( H oF x. ( ( NN X. { 1 } ) oF + G ) )
6 basellem8.n 
 |-  N = ( ( 2 x. M ) + 1 )
7 fzfid 
 |-  ( M e. NN -> ( 1 ... M ) e. Fin )
8 pire 
 |-  _pi e. RR
9 2nn 
 |-  2 e. NN
10 nnmulcl 
 |-  ( ( 2 e. NN /\ M e. NN ) -> ( 2 x. M ) e. NN )
11 9 10 mpan 
 |-  ( M e. NN -> ( 2 x. M ) e. NN )
12 11 peano2nnd 
 |-  ( M e. NN -> ( ( 2 x. M ) + 1 ) e. NN )
13 6 12 eqeltrid 
 |-  ( M e. NN -> N e. NN )
14 nndivre 
 |-  ( ( _pi e. RR /\ N e. NN ) -> ( _pi / N ) e. RR )
15 8 13 14 sylancr 
 |-  ( M e. NN -> ( _pi / N ) e. RR )
16 15 resqcld 
 |-  ( M e. NN -> ( ( _pi / N ) ^ 2 ) e. RR )
17 16 adantr 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( _pi / N ) ^ 2 ) e. RR )
18 6 basellem1 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( k x. _pi ) / N ) e. ( 0 (,) ( _pi / 2 ) ) )
19 tanrpcl 
 |-  ( ( ( k x. _pi ) / N ) e. ( 0 (,) ( _pi / 2 ) ) -> ( tan ` ( ( k x. _pi ) / N ) ) e. RR+ )
20 18 19 syl 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( tan ` ( ( k x. _pi ) / N ) ) e. RR+ )
21 20 rpred 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( tan ` ( ( k x. _pi ) / N ) ) e. RR )
22 20 rpne0d 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( tan ` ( ( k x. _pi ) / N ) ) =/= 0 )
23 2z 
 |-  2 e. ZZ
24 znegcl 
 |-  ( 2 e. ZZ -> -u 2 e. ZZ )
25 23 24 ax-mp 
 |-  -u 2 e. ZZ
26 25 a1i 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> -u 2 e. ZZ )
27 21 22 26 reexpclzd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) e. RR )
28 17 27 remulcld 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( _pi / N ) ^ 2 ) x. ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) ) e. RR )
29 elfznn 
 |-  ( k e. ( 1 ... M ) -> k e. NN )
30 29 adantl 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> k e. NN )
31 30 nnred 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> k e. RR )
32 30 nnne0d 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> k =/= 0 )
33 31 32 26 reexpclzd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( k ^ -u 2 ) e. RR )
34 20 rpcnd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( tan ` ( ( k x. _pi ) / N ) ) e. CC )
35 2nn0 
 |-  2 e. NN0
36 expneg 
 |-  ( ( ( tan ` ( ( k x. _pi ) / N ) ) e. CC /\ 2 e. NN0 ) -> ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) = ( 1 / ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) )
37 34 35 36 sylancl 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) = ( 1 / ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) )
38 37 oveq2d 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( _pi / N ) ^ 2 ) x. ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) ) = ( ( ( _pi / N ) ^ 2 ) x. ( 1 / ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) ) )
39 15 recnd 
 |-  ( M e. NN -> ( _pi / N ) e. CC )
40 39 sqcld 
 |-  ( M e. NN -> ( ( _pi / N ) ^ 2 ) e. CC )
41 40 adantr 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( _pi / N ) ^ 2 ) e. CC )
42 rpexpcl 
 |-  ( ( ( tan ` ( ( k x. _pi ) / N ) ) e. RR+ /\ 2 e. ZZ ) -> ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) e. RR+ )
43 20 23 42 sylancl 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) e. RR+ )
44 43 rpcnd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) e. CC )
45 43 rpne0d 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) =/= 0 )
46 41 44 45 divrecd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( _pi / N ) ^ 2 ) / ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) = ( ( ( _pi / N ) ^ 2 ) x. ( 1 / ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) ) )
47 38 46 eqtr4d 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( _pi / N ) ^ 2 ) x. ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) ) = ( ( ( _pi / N ) ^ 2 ) / ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) )
48 30 nnrpd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> k e. RR+ )
49 rpexpcl 
 |-  ( ( k e. RR+ /\ -u 2 e. ZZ ) -> ( k ^ -u 2 ) e. RR+ )
50 48 25 49 sylancl 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( k ^ -u 2 ) e. RR+ )
51 30 nncnd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> k e. CC )
52 51 32 26 expnegd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( k ^ -u -u 2 ) = ( 1 / ( k ^ -u 2 ) ) )
53 2cn 
 |-  2 e. CC
54 53 negnegi 
 |-  -u -u 2 = 2
55 54 oveq2i 
 |-  ( k ^ -u -u 2 ) = ( k ^ 2 )
56 52 55 eqtr3di 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( 1 / ( k ^ -u 2 ) ) = ( k ^ 2 ) )
57 56 oveq1d 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( 1 / ( k ^ -u 2 ) ) x. ( ( _pi / N ) ^ 2 ) ) = ( ( k ^ 2 ) x. ( ( _pi / N ) ^ 2 ) ) )
58 nncn 
 |-  ( k e. NN -> k e. CC )
59 nnne0 
 |-  ( k e. NN -> k =/= 0 )
60 25 a1i 
 |-  ( k e. NN -> -u 2 e. ZZ )
61 58 59 60 expclzd 
 |-  ( k e. NN -> ( k ^ -u 2 ) e. CC )
62 30 61 syl 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( k ^ -u 2 ) e. CC )
63 51 32 26 expne0d 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( k ^ -u 2 ) =/= 0 )
64 41 62 63 divrec2d 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( _pi / N ) ^ 2 ) / ( k ^ -u 2 ) ) = ( ( 1 / ( k ^ -u 2 ) ) x. ( ( _pi / N ) ^ 2 ) ) )
65 picn 
 |-  _pi e. CC
66 65 a1i 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> _pi e. CC )
67 13 nncnd 
 |-  ( M e. NN -> N e. CC )
68 67 adantr 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> N e. CC )
69 13 nnne0d 
 |-  ( M e. NN -> N =/= 0 )
70 69 adantr 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> N =/= 0 )
71 51 66 68 70 divassd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( k x. _pi ) / N ) = ( k x. ( _pi / N ) ) )
72 71 oveq1d 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( k x. _pi ) / N ) ^ 2 ) = ( ( k x. ( _pi / N ) ) ^ 2 ) )
73 39 adantr 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( _pi / N ) e. CC )
74 51 73 sqmuld 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( k x. ( _pi / N ) ) ^ 2 ) = ( ( k ^ 2 ) x. ( ( _pi / N ) ^ 2 ) ) )
75 72 74 eqtrd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( k x. _pi ) / N ) ^ 2 ) = ( ( k ^ 2 ) x. ( ( _pi / N ) ^ 2 ) ) )
76 57 64 75 3eqtr4d 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( _pi / N ) ^ 2 ) / ( k ^ -u 2 ) ) = ( ( ( k x. _pi ) / N ) ^ 2 ) )
77 elioore 
 |-  ( ( ( k x. _pi ) / N ) e. ( 0 (,) ( _pi / 2 ) ) -> ( ( k x. _pi ) / N ) e. RR )
78 18 77 syl 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( k x. _pi ) / N ) e. RR )
79 78 resqcld 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( k x. _pi ) / N ) ^ 2 ) e. RR )
80 43 rpred 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) e. RR )
81 tangtx 
 |-  ( ( ( k x. _pi ) / N ) e. ( 0 (,) ( _pi / 2 ) ) -> ( ( k x. _pi ) / N ) < ( tan ` ( ( k x. _pi ) / N ) ) )
82 18 81 syl 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( k x. _pi ) / N ) < ( tan ` ( ( k x. _pi ) / N ) ) )
83 eliooord 
 |-  ( ( ( k x. _pi ) / N ) e. ( 0 (,) ( _pi / 2 ) ) -> ( 0 < ( ( k x. _pi ) / N ) /\ ( ( k x. _pi ) / N ) < ( _pi / 2 ) ) )
84 18 83 syl 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( 0 < ( ( k x. _pi ) / N ) /\ ( ( k x. _pi ) / N ) < ( _pi / 2 ) ) )
85 84 simpld 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> 0 < ( ( k x. _pi ) / N ) )
86 78 85 elrpd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( k x. _pi ) / N ) e. RR+ )
87 86 rpge0d 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> 0 <_ ( ( k x. _pi ) / N ) )
88 20 rpge0d 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> 0 <_ ( tan ` ( ( k x. _pi ) / N ) ) )
89 78 21 87 88 lt2sqd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( k x. _pi ) / N ) < ( tan ` ( ( k x. _pi ) / N ) ) <-> ( ( ( k x. _pi ) / N ) ^ 2 ) < ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) )
90 82 89 mpbid 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( k x. _pi ) / N ) ^ 2 ) < ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) )
91 79 80 90 ltled 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( k x. _pi ) / N ) ^ 2 ) <_ ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) )
92 76 91 eqbrtrd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( _pi / N ) ^ 2 ) / ( k ^ -u 2 ) ) <_ ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) )
93 17 50 43 92 lediv23d 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( _pi / N ) ^ 2 ) / ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) <_ ( k ^ -u 2 ) )
94 47 93 eqbrtrd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( _pi / N ) ^ 2 ) x. ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) ) <_ ( k ^ -u 2 ) )
95 7 28 33 94 fsumle 
 |-  ( M e. NN -> sum_ k e. ( 1 ... M ) ( ( ( _pi / N ) ^ 2 ) x. ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) ) <_ sum_ k e. ( 1 ... M ) ( k ^ -u 2 ) )
96 oveq2 
 |-  ( n = M -> ( 2 x. n ) = ( 2 x. M ) )
97 96 oveq1d 
 |-  ( n = M -> ( ( 2 x. n ) + 1 ) = ( ( 2 x. M ) + 1 ) )
98 97 6 eqtr4di 
 |-  ( n = M -> ( ( 2 x. n ) + 1 ) = N )
99 98 oveq2d 
 |-  ( n = M -> ( 1 / ( ( 2 x. n ) + 1 ) ) = ( 1 / N ) )
100 99 oveq2d 
 |-  ( n = M -> ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) = ( 1 - ( 1 / N ) ) )
101 100 oveq2d 
 |-  ( n = M -> ( ( ( _pi ^ 2 ) / 6 ) x. ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) = ( ( ( _pi ^ 2 ) / 6 ) x. ( 1 - ( 1 / N ) ) ) )
102 99 oveq2d 
 |-  ( n = M -> ( -u 2 x. ( 1 / ( ( 2 x. n ) + 1 ) ) ) = ( -u 2 x. ( 1 / N ) ) )
103 102 oveq2d 
 |-  ( n = M -> ( 1 + ( -u 2 x. ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) = ( 1 + ( -u 2 x. ( 1 / N ) ) ) )
104 101 103 oveq12d 
 |-  ( n = M -> ( ( ( ( _pi ^ 2 ) / 6 ) x. ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) x. ( 1 + ( -u 2 x. ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) ) = ( ( ( ( _pi ^ 2 ) / 6 ) x. ( 1 - ( 1 / N ) ) ) x. ( 1 + ( -u 2 x. ( 1 / N ) ) ) ) )
105 nnex 
 |-  NN e. _V
106 105 a1i 
 |-  ( T. -> NN e. _V )
107 ovexd 
 |-  ( ( T. /\ n e. NN ) -> ( ( ( _pi ^ 2 ) / 6 ) x. ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) e. _V )
108 ovexd 
 |-  ( ( T. /\ n e. NN ) -> ( 1 + ( -u 2 x. ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) e. _V )
109 8 resqcli 
 |-  ( _pi ^ 2 ) e. RR
110 6re 
 |-  6 e. RR
111 6nn 
 |-  6 e. NN
112 111 nnne0i 
 |-  6 =/= 0
113 109 110 112 redivcli 
 |-  ( ( _pi ^ 2 ) / 6 ) e. RR
114 113 a1i 
 |-  ( ( T. /\ n e. NN ) -> ( ( _pi ^ 2 ) / 6 ) e. RR )
115 ovexd 
 |-  ( ( T. /\ n e. NN ) -> ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) e. _V )
116 fconstmpt 
 |-  ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) = ( n e. NN |-> ( ( _pi ^ 2 ) / 6 ) )
117 116 a1i 
 |-  ( T. -> ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) = ( n e. NN |-> ( ( _pi ^ 2 ) / 6 ) ) )
118 1zzd 
 |-  ( ( T. /\ n e. NN ) -> 1 e. ZZ )
119 ovexd 
 |-  ( ( T. /\ n e. NN ) -> ( 1 / ( ( 2 x. n ) + 1 ) ) e. _V )
120 fconstmpt 
 |-  ( NN X. { 1 } ) = ( n e. NN |-> 1 )
121 120 a1i 
 |-  ( T. -> ( NN X. { 1 } ) = ( n e. NN |-> 1 ) )
122 1 a1i 
 |-  ( T. -> G = ( n e. NN |-> ( 1 / ( ( 2 x. n ) + 1 ) ) ) )
123 106 118 119 121 122 offval2 
 |-  ( T. -> ( ( NN X. { 1 } ) oF - G ) = ( n e. NN |-> ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) )
124 106 114 115 117 123 offval2 
 |-  ( T. -> ( ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) oF x. ( ( NN X. { 1 } ) oF - G ) ) = ( n e. NN |-> ( ( ( _pi ^ 2 ) / 6 ) x. ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) ) )
125 3 124 eqtrid 
 |-  ( T. -> H = ( n e. NN |-> ( ( ( _pi ^ 2 ) / 6 ) x. ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) ) )
126 ovexd 
 |-  ( ( T. /\ n e. NN ) -> ( -u 2 x. ( 1 / ( ( 2 x. n ) + 1 ) ) ) e. _V )
127 53 negcli 
 |-  -u 2 e. CC
128 127 a1i 
 |-  ( ( T. /\ n e. NN ) -> -u 2 e. CC )
129 fconstmpt 
 |-  ( NN X. { -u 2 } ) = ( n e. NN |-> -u 2 )
130 129 a1i 
 |-  ( T. -> ( NN X. { -u 2 } ) = ( n e. NN |-> -u 2 ) )
131 106 128 119 130 122 offval2 
 |-  ( T. -> ( ( NN X. { -u 2 } ) oF x. G ) = ( n e. NN |-> ( -u 2 x. ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) )
132 106 118 126 121 131 offval2 
 |-  ( T. -> ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) = ( n e. NN |-> ( 1 + ( -u 2 x. ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) ) )
133 106 107 108 125 132 offval2 
 |-  ( T. -> ( H oF x. ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ) = ( n e. NN |-> ( ( ( ( _pi ^ 2 ) / 6 ) x. ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) x. ( 1 + ( -u 2 x. ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) ) ) )
134 133 mptru 
 |-  ( H oF x. ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ) = ( n e. NN |-> ( ( ( ( _pi ^ 2 ) / 6 ) x. ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) x. ( 1 + ( -u 2 x. ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) ) )
135 4 134 eqtri 
 |-  J = ( n e. NN |-> ( ( ( ( _pi ^ 2 ) / 6 ) x. ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) x. ( 1 + ( -u 2 x. ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) ) )
136 ovex 
 |-  ( ( ( ( _pi ^ 2 ) / 6 ) x. ( 1 - ( 1 / N ) ) ) x. ( 1 + ( -u 2 x. ( 1 / N ) ) ) ) e. _V
137 104 135 136 fvmpt 
 |-  ( M e. NN -> ( J ` M ) = ( ( ( ( _pi ^ 2 ) / 6 ) x. ( 1 - ( 1 / N ) ) ) x. ( 1 + ( -u 2 x. ( 1 / N ) ) ) ) )
138 113 recni 
 |-  ( ( _pi ^ 2 ) / 6 ) e. CC
139 138 a1i 
 |-  ( M e. NN -> ( ( _pi ^ 2 ) / 6 ) e. CC )
140 11 nncnd 
 |-  ( M e. NN -> ( 2 x. M ) e. CC )
141 140 67 69 divcld 
 |-  ( M e. NN -> ( ( 2 x. M ) / N ) e. CC )
142 ax-1cn 
 |-  1 e. CC
143 subcl 
 |-  ( ( ( 2 x. M ) e. CC /\ 1 e. CC ) -> ( ( 2 x. M ) - 1 ) e. CC )
144 140 142 143 sylancl 
 |-  ( M e. NN -> ( ( 2 x. M ) - 1 ) e. CC )
145 144 67 69 divcld 
 |-  ( M e. NN -> ( ( ( 2 x. M ) - 1 ) / N ) e. CC )
146 139 141 145 mulassd 
 |-  ( M e. NN -> ( ( ( ( _pi ^ 2 ) / 6 ) x. ( ( 2 x. M ) / N ) ) x. ( ( ( 2 x. M ) - 1 ) / N ) ) = ( ( ( _pi ^ 2 ) / 6 ) x. ( ( ( 2 x. M ) / N ) x. ( ( ( 2 x. M ) - 1 ) / N ) ) ) )
147 1cnd 
 |-  ( M e. NN -> 1 e. CC )
148 67 147 67 69 divsubdird 
 |-  ( M e. NN -> ( ( N - 1 ) / N ) = ( ( N / N ) - ( 1 / N ) ) )
149 6 oveq1i 
 |-  ( N - 1 ) = ( ( ( 2 x. M ) + 1 ) - 1 )
150 pncan 
 |-  ( ( ( 2 x. M ) e. CC /\ 1 e. CC ) -> ( ( ( 2 x. M ) + 1 ) - 1 ) = ( 2 x. M ) )
151 140 142 150 sylancl 
 |-  ( M e. NN -> ( ( ( 2 x. M ) + 1 ) - 1 ) = ( 2 x. M ) )
152 149 151 eqtrid 
 |-  ( M e. NN -> ( N - 1 ) = ( 2 x. M ) )
153 152 oveq1d 
 |-  ( M e. NN -> ( ( N - 1 ) / N ) = ( ( 2 x. M ) / N ) )
154 67 69 dividd 
 |-  ( M e. NN -> ( N / N ) = 1 )
155 154 oveq1d 
 |-  ( M e. NN -> ( ( N / N ) - ( 1 / N ) ) = ( 1 - ( 1 / N ) ) )
156 148 153 155 3eqtr3rd 
 |-  ( M e. NN -> ( 1 - ( 1 / N ) ) = ( ( 2 x. M ) / N ) )
157 156 oveq2d 
 |-  ( M e. NN -> ( ( ( _pi ^ 2 ) / 6 ) x. ( 1 - ( 1 / N ) ) ) = ( ( ( _pi ^ 2 ) / 6 ) x. ( ( 2 x. M ) / N ) ) )
158 127 a1i 
 |-  ( M e. NN -> -u 2 e. CC )
159 67 158 67 69 divdird 
 |-  ( M e. NN -> ( ( N + -u 2 ) / N ) = ( ( N / N ) + ( -u 2 / N ) ) )
160 negsub 
 |-  ( ( N e. CC /\ 2 e. CC ) -> ( N + -u 2 ) = ( N - 2 ) )
161 67 53 160 sylancl 
 |-  ( M e. NN -> ( N + -u 2 ) = ( N - 2 ) )
162 df-2 
 |-  2 = ( 1 + 1 )
163 6 162 oveq12i 
 |-  ( N - 2 ) = ( ( ( 2 x. M ) + 1 ) - ( 1 + 1 ) )
164 140 147 147 pnpcan2d 
 |-  ( M e. NN -> ( ( ( 2 x. M ) + 1 ) - ( 1 + 1 ) ) = ( ( 2 x. M ) - 1 ) )
165 163 164 eqtrid 
 |-  ( M e. NN -> ( N - 2 ) = ( ( 2 x. M ) - 1 ) )
166 161 165 eqtrd 
 |-  ( M e. NN -> ( N + -u 2 ) = ( ( 2 x. M ) - 1 ) )
167 166 oveq1d 
 |-  ( M e. NN -> ( ( N + -u 2 ) / N ) = ( ( ( 2 x. M ) - 1 ) / N ) )
168 158 67 69 divrecd 
 |-  ( M e. NN -> ( -u 2 / N ) = ( -u 2 x. ( 1 / N ) ) )
169 154 168 oveq12d 
 |-  ( M e. NN -> ( ( N / N ) + ( -u 2 / N ) ) = ( 1 + ( -u 2 x. ( 1 / N ) ) ) )
170 159 167 169 3eqtr3rd 
 |-  ( M e. NN -> ( 1 + ( -u 2 x. ( 1 / N ) ) ) = ( ( ( 2 x. M ) - 1 ) / N ) )
171 157 170 oveq12d 
 |-  ( M e. NN -> ( ( ( ( _pi ^ 2 ) / 6 ) x. ( 1 - ( 1 / N ) ) ) x. ( 1 + ( -u 2 x. ( 1 / N ) ) ) ) = ( ( ( ( _pi ^ 2 ) / 6 ) x. ( ( 2 x. M ) / N ) ) x. ( ( ( 2 x. M ) - 1 ) / N ) ) )
172 13 nnsqcld 
 |-  ( M e. NN -> ( N ^ 2 ) e. NN )
173 172 nncnd 
 |-  ( M e. NN -> ( N ^ 2 ) e. CC )
174 6cn 
 |-  6 e. CC
175 174 a1i 
 |-  ( M e. NN -> 6 e. CC )
176 173 175 mulcomd 
 |-  ( M e. NN -> ( ( N ^ 2 ) x. 6 ) = ( 6 x. ( N ^ 2 ) ) )
177 176 oveq2d 
 |-  ( M e. NN -> ( ( ( _pi ^ 2 ) x. ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) ) / ( ( N ^ 2 ) x. 6 ) ) = ( ( ( _pi ^ 2 ) x. ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) ) / ( 6 x. ( N ^ 2 ) ) ) )
178 109 recni 
 |-  ( _pi ^ 2 ) e. CC
179 178 a1i 
 |-  ( M e. NN -> ( _pi ^ 2 ) e. CC )
180 140 144 mulcld 
 |-  ( M e. NN -> ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) e. CC )
181 172 nnne0d 
 |-  ( M e. NN -> ( N ^ 2 ) =/= 0 )
182 173 181 jca 
 |-  ( M e. NN -> ( ( N ^ 2 ) e. CC /\ ( N ^ 2 ) =/= 0 ) )
183 174 112 pm3.2i 
 |-  ( 6 e. CC /\ 6 =/= 0 )
184 183 a1i 
 |-  ( M e. NN -> ( 6 e. CC /\ 6 =/= 0 ) )
185 divmuldiv 
 |-  ( ( ( ( _pi ^ 2 ) e. CC /\ ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) e. CC ) /\ ( ( ( N ^ 2 ) e. CC /\ ( N ^ 2 ) =/= 0 ) /\ ( 6 e. CC /\ 6 =/= 0 ) ) ) -> ( ( ( _pi ^ 2 ) / ( N ^ 2 ) ) x. ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / 6 ) ) = ( ( ( _pi ^ 2 ) x. ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) ) / ( ( N ^ 2 ) x. 6 ) ) )
186 179 180 182 184 185 syl22anc 
 |-  ( M e. NN -> ( ( ( _pi ^ 2 ) / ( N ^ 2 ) ) x. ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / 6 ) ) = ( ( ( _pi ^ 2 ) x. ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) ) / ( ( N ^ 2 ) x. 6 ) ) )
187 divmuldiv 
 |-  ( ( ( ( _pi ^ 2 ) e. CC /\ ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) e. CC ) /\ ( ( 6 e. CC /\ 6 =/= 0 ) /\ ( ( N ^ 2 ) e. CC /\ ( N ^ 2 ) =/= 0 ) ) ) -> ( ( ( _pi ^ 2 ) / 6 ) x. ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / ( N ^ 2 ) ) ) = ( ( ( _pi ^ 2 ) x. ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) ) / ( 6 x. ( N ^ 2 ) ) ) )
188 179 180 184 182 187 syl22anc 
 |-  ( M e. NN -> ( ( ( _pi ^ 2 ) / 6 ) x. ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / ( N ^ 2 ) ) ) = ( ( ( _pi ^ 2 ) x. ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) ) / ( 6 x. ( N ^ 2 ) ) ) )
189 177 186 188 3eqtr4d 
 |-  ( M e. NN -> ( ( ( _pi ^ 2 ) / ( N ^ 2 ) ) x. ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / 6 ) ) = ( ( ( _pi ^ 2 ) / 6 ) x. ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / ( N ^ 2 ) ) ) )
190 65 a1i 
 |-  ( M e. NN -> _pi e. CC )
191 190 67 69 sqdivd 
 |-  ( M e. NN -> ( ( _pi / N ) ^ 2 ) = ( ( _pi ^ 2 ) / ( N ^ 2 ) ) )
192 191 oveq1d 
 |-  ( M e. NN -> ( ( ( _pi / N ) ^ 2 ) x. ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / 6 ) ) = ( ( ( _pi ^ 2 ) / ( N ^ 2 ) ) x. ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / 6 ) ) )
193 140 67 144 67 69 69 divmuldivd 
 |-  ( M e. NN -> ( ( ( 2 x. M ) / N ) x. ( ( ( 2 x. M ) - 1 ) / N ) ) = ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / ( N x. N ) ) )
194 67 sqvald 
 |-  ( M e. NN -> ( N ^ 2 ) = ( N x. N ) )
195 194 oveq2d 
 |-  ( M e. NN -> ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / ( N ^ 2 ) ) = ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / ( N x. N ) ) )
196 193 195 eqtr4d 
 |-  ( M e. NN -> ( ( ( 2 x. M ) / N ) x. ( ( ( 2 x. M ) - 1 ) / N ) ) = ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / ( N ^ 2 ) ) )
197 196 oveq2d 
 |-  ( M e. NN -> ( ( ( _pi ^ 2 ) / 6 ) x. ( ( ( 2 x. M ) / N ) x. ( ( ( 2 x. M ) - 1 ) / N ) ) ) = ( ( ( _pi ^ 2 ) / 6 ) x. ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / ( N ^ 2 ) ) ) )
198 189 192 197 3eqtr4d 
 |-  ( M e. NN -> ( ( ( _pi / N ) ^ 2 ) x. ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / 6 ) ) = ( ( ( _pi ^ 2 ) / 6 ) x. ( ( ( 2 x. M ) / N ) x. ( ( ( 2 x. M ) - 1 ) / N ) ) ) )
199 146 171 198 3eqtr4d 
 |-  ( M e. NN -> ( ( ( ( _pi ^ 2 ) / 6 ) x. ( 1 - ( 1 / N ) ) ) x. ( 1 + ( -u 2 x. ( 1 / N ) ) ) ) = ( ( ( _pi / N ) ^ 2 ) x. ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / 6 ) ) )
200 eqid 
 |-  ( x e. CC |-> sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( x ^ j ) ) ) = ( x e. CC |-> sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( x ^ j ) ) )
201 eqid 
 |-  ( n e. ( 1 ... M ) |-> ( ( tan ` ( ( n x. _pi ) / N ) ) ^ -u 2 ) ) = ( n e. ( 1 ... M ) |-> ( ( tan ` ( ( n x. _pi ) / N ) ) ^ -u 2 ) )
202 6 200 201 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 ) )
203 202 oveq2d 
 |-  ( M e. NN -> ( ( ( _pi / N ) ^ 2 ) x. sum_ k e. ( 1 ... M ) ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) ) = ( ( ( _pi / N ) ^ 2 ) x. ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / 6 ) ) )
204 199 203 eqtr4d 
 |-  ( M e. NN -> ( ( ( ( _pi ^ 2 ) / 6 ) x. ( 1 - ( 1 / N ) ) ) x. ( 1 + ( -u 2 x. ( 1 / N ) ) ) ) = ( ( ( _pi / N ) ^ 2 ) x. sum_ k e. ( 1 ... M ) ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) ) )
205 27 recnd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) e. CC )
206 7 40 205 fsummulc2 
 |-  ( M e. NN -> ( ( ( _pi / N ) ^ 2 ) x. sum_ k e. ( 1 ... M ) ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) ) = sum_ k e. ( 1 ... M ) ( ( ( _pi / N ) ^ 2 ) x. ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) ) )
207 137 204 206 3eqtrd 
 |-  ( M e. NN -> ( J ` M ) = sum_ k e. ( 1 ... M ) ( ( ( _pi / N ) ^ 2 ) x. ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) ) )
208 2 fveq1i 
 |-  ( F ` M ) = ( seq 1 ( + , ( n e. NN |-> ( n ^ -u 2 ) ) ) ` M )
209 oveq1 
 |-  ( n = k -> ( n ^ -u 2 ) = ( k ^ -u 2 ) )
210 eqid 
 |-  ( n e. NN |-> ( n ^ -u 2 ) ) = ( n e. NN |-> ( n ^ -u 2 ) )
211 ovex 
 |-  ( k ^ -u 2 ) e. _V
212 209 210 211 fvmpt 
 |-  ( k e. NN -> ( ( n e. NN |-> ( n ^ -u 2 ) ) ` k ) = ( k ^ -u 2 ) )
213 30 212 syl 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( n e. NN |-> ( n ^ -u 2 ) ) ` k ) = ( k ^ -u 2 ) )
214 id 
 |-  ( M e. NN -> M e. NN )
215 nnuz 
 |-  NN = ( ZZ>= ` 1 )
216 214 215 eleqtrdi 
 |-  ( M e. NN -> M e. ( ZZ>= ` 1 ) )
217 213 216 62 fsumser 
 |-  ( M e. NN -> sum_ k e. ( 1 ... M ) ( k ^ -u 2 ) = ( seq 1 ( + , ( n e. NN |-> ( n ^ -u 2 ) ) ) ` M ) )
218 208 217 eqtr4id 
 |-  ( M e. NN -> ( F ` M ) = sum_ k e. ( 1 ... M ) ( k ^ -u 2 ) )
219 95 207 218 3brtr4d 
 |-  ( M e. NN -> ( J ` M ) <_ ( F ` M ) )
220 78 resincld 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( sin ` ( ( k x. _pi ) / N ) ) e. RR )
221 sincosq1sgn 
 |-  ( ( ( k x. _pi ) / N ) e. ( 0 (,) ( _pi / 2 ) ) -> ( 0 < ( sin ` ( ( k x. _pi ) / N ) ) /\ 0 < ( cos ` ( ( k x. _pi ) / N ) ) ) )
222 18 221 syl 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( 0 < ( sin ` ( ( k x. _pi ) / N ) ) /\ 0 < ( cos ` ( ( k x. _pi ) / N ) ) ) )
223 222 simpld 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> 0 < ( sin ` ( ( k x. _pi ) / N ) ) )
224 223 gt0ne0d 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( sin ` ( ( k x. _pi ) / N ) ) =/= 0 )
225 220 224 26 reexpclzd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( sin ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) e. RR )
226 17 225 remulcld 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( _pi / N ) ^ 2 ) x. ( ( sin ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) ) e. RR )
227 sinltx 
 |-  ( ( ( k x. _pi ) / N ) e. RR+ -> ( sin ` ( ( k x. _pi ) / N ) ) < ( ( k x. _pi ) / N ) )
228 86 227 syl 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( sin ` ( ( k x. _pi ) / N ) ) < ( ( k x. _pi ) / N ) )
229 220 78 228 ltled 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( sin ` ( ( k x. _pi ) / N ) ) <_ ( ( k x. _pi ) / N ) )
230 0re 
 |-  0 e. RR
231 ltle 
 |-  ( ( 0 e. RR /\ ( sin ` ( ( k x. _pi ) / N ) ) e. RR ) -> ( 0 < ( sin ` ( ( k x. _pi ) / N ) ) -> 0 <_ ( sin ` ( ( k x. _pi ) / N ) ) ) )
232 230 220 231 sylancr 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( 0 < ( sin ` ( ( k x. _pi ) / N ) ) -> 0 <_ ( sin ` ( ( k x. _pi ) / N ) ) ) )
233 223 232 mpd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> 0 <_ ( sin ` ( ( k x. _pi ) / N ) ) )
234 220 78 233 87 le2sqd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( sin ` ( ( k x. _pi ) / N ) ) <_ ( ( k x. _pi ) / N ) <-> ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) <_ ( ( ( k x. _pi ) / N ) ^ 2 ) ) )
235 229 234 mpbid 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) <_ ( ( ( k x. _pi ) / N ) ^ 2 ) )
236 235 76 breqtrrd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) <_ ( ( ( _pi / N ) ^ 2 ) / ( k ^ -u 2 ) ) )
237 220 resqcld 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) e. RR )
238 237 17 50 lemuldiv2d 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( k ^ -u 2 ) x. ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) <_ ( ( _pi / N ) ^ 2 ) <-> ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) <_ ( ( ( _pi / N ) ^ 2 ) / ( k ^ -u 2 ) ) ) )
239 220 223 elrpd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( sin ` ( ( k x. _pi ) / N ) ) e. RR+ )
240 rpexpcl 
 |-  ( ( ( sin ` ( ( k x. _pi ) / N ) ) e. RR+ /\ 2 e. ZZ ) -> ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) e. RR+ )
241 239 23 240 sylancl 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) e. RR+ )
242 33 17 241 lemuldivd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( k ^ -u 2 ) x. ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) <_ ( ( _pi / N ) ^ 2 ) <-> ( k ^ -u 2 ) <_ ( ( ( _pi / N ) ^ 2 ) / ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) ) )
243 238 242 bitr3d 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) <_ ( ( ( _pi / N ) ^ 2 ) / ( k ^ -u 2 ) ) <-> ( k ^ -u 2 ) <_ ( ( ( _pi / N ) ^ 2 ) / ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) ) )
244 236 243 mpbid 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( k ^ -u 2 ) <_ ( ( ( _pi / N ) ^ 2 ) / ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) )
245 220 recnd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( sin ` ( ( k x. _pi ) / N ) ) e. CC )
246 expneg 
 |-  ( ( ( sin ` ( ( k x. _pi ) / N ) ) e. CC /\ 2 e. NN0 ) -> ( ( sin ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) = ( 1 / ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) )
247 245 35 246 sylancl 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( sin ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) = ( 1 / ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) )
248 247 oveq2d 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( _pi / N ) ^ 2 ) x. ( ( sin ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) ) = ( ( ( _pi / N ) ^ 2 ) x. ( 1 / ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) ) )
249 237 recnd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) e. CC )
250 241 rpne0d 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) =/= 0 )
251 41 249 250 divrecd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( _pi / N ) ^ 2 ) / ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) = ( ( ( _pi / N ) ^ 2 ) x. ( 1 / ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) ) )
252 248 251 eqtr4d 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( _pi / N ) ^ 2 ) x. ( ( sin ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) ) = ( ( ( _pi / N ) ^ 2 ) / ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) )
253 244 252 breqtrrd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( k ^ -u 2 ) <_ ( ( ( _pi / N ) ^ 2 ) x. ( ( sin ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) ) )
254 7 33 226 253 fsumle 
 |-  ( M e. NN -> sum_ k e. ( 1 ... M ) ( k ^ -u 2 ) <_ sum_ k e. ( 1 ... M ) ( ( ( _pi / N ) ^ 2 ) x. ( ( sin ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) ) )
255 99 oveq2d 
 |-  ( n = M -> ( 1 + ( 1 / ( ( 2 x. n ) + 1 ) ) ) = ( 1 + ( 1 / N ) ) )
256 101 255 oveq12d 
 |-  ( n = M -> ( ( ( ( _pi ^ 2 ) / 6 ) x. ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) x. ( 1 + ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) = ( ( ( ( _pi ^ 2 ) / 6 ) x. ( 1 - ( 1 / N ) ) ) x. ( 1 + ( 1 / N ) ) ) )
257 ovexd 
 |-  ( ( T. /\ n e. NN ) -> ( 1 + ( 1 / ( ( 2 x. n ) + 1 ) ) ) e. _V )
258 106 118 119 121 122 offval2 
 |-  ( T. -> ( ( NN X. { 1 } ) oF + G ) = ( n e. NN |-> ( 1 + ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) )
259 106 107 257 125 258 offval2 
 |-  ( T. -> ( H oF x. ( ( NN X. { 1 } ) oF + G ) ) = ( n e. NN |-> ( ( ( ( _pi ^ 2 ) / 6 ) x. ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) x. ( 1 + ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) ) )
260 259 mptru 
 |-  ( H oF x. ( ( NN X. { 1 } ) oF + G ) ) = ( n e. NN |-> ( ( ( ( _pi ^ 2 ) / 6 ) x. ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) x. ( 1 + ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) )
261 5 260 eqtri 
 |-  K = ( n e. NN |-> ( ( ( ( _pi ^ 2 ) / 6 ) x. ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) x. ( 1 + ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) )
262 ovex 
 |-  ( ( ( ( _pi ^ 2 ) / 6 ) x. ( 1 - ( 1 / N ) ) ) x. ( 1 + ( 1 / N ) ) ) e. _V
263 256 261 262 fvmpt 
 |-  ( M e. NN -> ( K ` M ) = ( ( ( ( _pi ^ 2 ) / 6 ) x. ( 1 - ( 1 / N ) ) ) x. ( 1 + ( 1 / N ) ) ) )
264 peano2cn 
 |-  ( N e. CC -> ( N + 1 ) e. CC )
265 67 264 syl 
 |-  ( M e. NN -> ( N + 1 ) e. CC )
266 265 67 69 divcld 
 |-  ( M e. NN -> ( ( N + 1 ) / N ) e. CC )
267 139 141 266 mulassd 
 |-  ( M e. NN -> ( ( ( ( _pi ^ 2 ) / 6 ) x. ( ( 2 x. M ) / N ) ) x. ( ( N + 1 ) / N ) ) = ( ( ( _pi ^ 2 ) / 6 ) x. ( ( ( 2 x. M ) / N ) x. ( ( N + 1 ) / N ) ) ) )
268 67 147 67 69 divdird 
 |-  ( M e. NN -> ( ( N + 1 ) / N ) = ( ( N / N ) + ( 1 / N ) ) )
269 154 oveq1d 
 |-  ( M e. NN -> ( ( N / N ) + ( 1 / N ) ) = ( 1 + ( 1 / N ) ) )
270 268 269 eqtr2d 
 |-  ( M e. NN -> ( 1 + ( 1 / N ) ) = ( ( N + 1 ) / N ) )
271 157 270 oveq12d 
 |-  ( M e. NN -> ( ( ( ( _pi ^ 2 ) / 6 ) x. ( 1 - ( 1 / N ) ) ) x. ( 1 + ( 1 / N ) ) ) = ( ( ( ( _pi ^ 2 ) / 6 ) x. ( ( 2 x. M ) / N ) ) x. ( ( N + 1 ) / N ) ) )
272 176 oveq2d 
 |-  ( M e. NN -> ( ( ( _pi ^ 2 ) x. ( ( 2 x. M ) x. ( N + 1 ) ) ) / ( ( N ^ 2 ) x. 6 ) ) = ( ( ( _pi ^ 2 ) x. ( ( 2 x. M ) x. ( N + 1 ) ) ) / ( 6 x. ( N ^ 2 ) ) ) )
273 140 265 mulcld 
 |-  ( M e. NN -> ( ( 2 x. M ) x. ( N + 1 ) ) e. CC )
274 divmuldiv 
 |-  ( ( ( ( _pi ^ 2 ) e. CC /\ ( ( 2 x. M ) x. ( N + 1 ) ) e. CC ) /\ ( ( ( N ^ 2 ) e. CC /\ ( N ^ 2 ) =/= 0 ) /\ ( 6 e. CC /\ 6 =/= 0 ) ) ) -> ( ( ( _pi ^ 2 ) / ( N ^ 2 ) ) x. ( ( ( 2 x. M ) x. ( N + 1 ) ) / 6 ) ) = ( ( ( _pi ^ 2 ) x. ( ( 2 x. M ) x. ( N + 1 ) ) ) / ( ( N ^ 2 ) x. 6 ) ) )
275 179 273 182 184 274 syl22anc 
 |-  ( M e. NN -> ( ( ( _pi ^ 2 ) / ( N ^ 2 ) ) x. ( ( ( 2 x. M ) x. ( N + 1 ) ) / 6 ) ) = ( ( ( _pi ^ 2 ) x. ( ( 2 x. M ) x. ( N + 1 ) ) ) / ( ( N ^ 2 ) x. 6 ) ) )
276 divmuldiv 
 |-  ( ( ( ( _pi ^ 2 ) e. CC /\ ( ( 2 x. M ) x. ( N + 1 ) ) e. CC ) /\ ( ( 6 e. CC /\ 6 =/= 0 ) /\ ( ( N ^ 2 ) e. CC /\ ( N ^ 2 ) =/= 0 ) ) ) -> ( ( ( _pi ^ 2 ) / 6 ) x. ( ( ( 2 x. M ) x. ( N + 1 ) ) / ( N ^ 2 ) ) ) = ( ( ( _pi ^ 2 ) x. ( ( 2 x. M ) x. ( N + 1 ) ) ) / ( 6 x. ( N ^ 2 ) ) ) )
277 179 273 184 182 276 syl22anc 
 |-  ( M e. NN -> ( ( ( _pi ^ 2 ) / 6 ) x. ( ( ( 2 x. M ) x. ( N + 1 ) ) / ( N ^ 2 ) ) ) = ( ( ( _pi ^ 2 ) x. ( ( 2 x. M ) x. ( N + 1 ) ) ) / ( 6 x. ( N ^ 2 ) ) ) )
278 272 275 277 3eqtr4d 
 |-  ( M e. NN -> ( ( ( _pi ^ 2 ) / ( N ^ 2 ) ) x. ( ( ( 2 x. M ) x. ( N + 1 ) ) / 6 ) ) = ( ( ( _pi ^ 2 ) / 6 ) x. ( ( ( 2 x. M ) x. ( N + 1 ) ) / ( N ^ 2 ) ) ) )
279 78 recoscld 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( cos ` ( ( k x. _pi ) / N ) ) e. RR )
280 279 recnd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( cos ` ( ( k x. _pi ) / N ) ) e. CC )
281 280 sqcld 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( cos ` ( ( k x. _pi ) / N ) ) ^ 2 ) e. CC )
282 249 281 249 250 divdird 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) + ( ( cos ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) / ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) = ( ( ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) / ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) + ( ( ( cos ` ( ( k x. _pi ) / N ) ) ^ 2 ) / ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) ) )
283 78 recnd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( k x. _pi ) / N ) e. CC )
284 sincossq 
 |-  ( ( ( k x. _pi ) / N ) e. CC -> ( ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) + ( ( cos ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) = 1 )
285 283 284 syl 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) + ( ( cos ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) = 1 )
286 285 oveq1d 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) + ( ( cos ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) / ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) = ( 1 / ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) )
287 249 250 dividd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) / ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) = 1 )
288 222 simprd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> 0 < ( cos ` ( ( k x. _pi ) / N ) ) )
289 288 gt0ne0d 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( cos ` ( ( k x. _pi ) / N ) ) =/= 0 )
290 tanval 
 |-  ( ( ( ( k x. _pi ) / N ) e. CC /\ ( cos ` ( ( k x. _pi ) / N ) ) =/= 0 ) -> ( tan ` ( ( k x. _pi ) / N ) ) = ( ( sin ` ( ( k x. _pi ) / N ) ) / ( cos ` ( ( k x. _pi ) / N ) ) ) )
291 283 289 290 syl2anc 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( tan ` ( ( k x. _pi ) / N ) ) = ( ( sin ` ( ( k x. _pi ) / N ) ) / ( cos ` ( ( k x. _pi ) / N ) ) ) )
292 291 oveq1d 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) = ( ( ( sin ` ( ( k x. _pi ) / N ) ) / ( cos ` ( ( k x. _pi ) / N ) ) ) ^ 2 ) )
293 245 280 289 sqdivd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( sin ` ( ( k x. _pi ) / N ) ) / ( cos ` ( ( k x. _pi ) / N ) ) ) ^ 2 ) = ( ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) / ( ( cos ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) )
294 292 293 eqtrd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) = ( ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) / ( ( cos ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) )
295 294 oveq2d 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( 1 / ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) = ( 1 / ( ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) / ( ( cos ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) ) )
296 sqne0 
 |-  ( ( cos ` ( ( k x. _pi ) / N ) ) e. CC -> ( ( ( cos ` ( ( k x. _pi ) / N ) ) ^ 2 ) =/= 0 <-> ( cos ` ( ( k x. _pi ) / N ) ) =/= 0 ) )
297 280 296 syl 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( cos ` ( ( k x. _pi ) / N ) ) ^ 2 ) =/= 0 <-> ( cos ` ( ( k x. _pi ) / N ) ) =/= 0 ) )
298 289 297 mpbird 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( cos ` ( ( k x. _pi ) / N ) ) ^ 2 ) =/= 0 )
299 249 281 250 298 recdivd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( 1 / ( ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) / ( ( cos ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) ) = ( ( ( cos ` ( ( k x. _pi ) / N ) ) ^ 2 ) / ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) )
300 37 295 299 3eqtrrd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( cos ` ( ( k x. _pi ) / N ) ) ^ 2 ) / ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) = ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) )
301 287 300 oveq12d 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) / ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) + ( ( ( cos ` ( ( k x. _pi ) / N ) ) ^ 2 ) / ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) ) = ( 1 + ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) ) )
302 282 286 301 3eqtr3d 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( 1 / ( ( sin ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) = ( 1 + ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) ) )
303 addcom 
 |-  ( ( 1 e. CC /\ ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) e. CC ) -> ( 1 + ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) ) = ( ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) + 1 ) )
304 142 205 303 sylancr 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( 1 + ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) ) = ( ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) + 1 ) )
305 247 302 304 3eqtrd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( sin ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) = ( ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) + 1 ) )
306 305 sumeq2dv 
 |-  ( M e. NN -> sum_ k e. ( 1 ... M ) ( ( sin ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) = sum_ k e. ( 1 ... M ) ( ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) + 1 ) )
307 1cnd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> 1 e. CC )
308 7 205 307 fsumadd 
 |-  ( M e. NN -> sum_ k e. ( 1 ... M ) ( ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) + 1 ) = ( sum_ k e. ( 1 ... M ) ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) + sum_ k e. ( 1 ... M ) 1 ) )
309 fsumconst 
 |-  ( ( ( 1 ... M ) e. Fin /\ 1 e. CC ) -> sum_ k e. ( 1 ... M ) 1 = ( ( # ` ( 1 ... M ) ) x. 1 ) )
310 7 142 309 sylancl 
 |-  ( M e. NN -> sum_ k e. ( 1 ... M ) 1 = ( ( # ` ( 1 ... M ) ) x. 1 ) )
311 nnnn0 
 |-  ( M e. NN -> M e. NN0 )
312 hashfz1 
 |-  ( M e. NN0 -> ( # ` ( 1 ... M ) ) = M )
313 311 312 syl 
 |-  ( M e. NN -> ( # ` ( 1 ... M ) ) = M )
314 313 oveq1d 
 |-  ( M e. NN -> ( ( # ` ( 1 ... M ) ) x. 1 ) = ( M x. 1 ) )
315 nncn 
 |-  ( M e. NN -> M e. CC )
316 315 mulridd 
 |-  ( M e. NN -> ( M x. 1 ) = M )
317 310 314 316 3eqtrd 
 |-  ( M e. NN -> sum_ k e. ( 1 ... M ) 1 = M )
318 202 317 oveq12d 
 |-  ( M e. NN -> ( sum_ k e. ( 1 ... M ) ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) + sum_ k e. ( 1 ... M ) 1 ) = ( ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / 6 ) + M ) )
319 306 308 318 3eqtrd 
 |-  ( M e. NN -> sum_ k e. ( 1 ... M ) ( ( sin ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) = ( ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / 6 ) + M ) )
320 3cn 
 |-  3 e. CC
321 320 a1i 
 |-  ( M e. NN -> 3 e. CC )
322 140 144 321 adddid 
 |-  ( M e. NN -> ( ( 2 x. M ) x. ( ( ( 2 x. M ) - 1 ) + 3 ) ) = ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) + ( ( 2 x. M ) x. 3 ) ) )
323 3m1e2 
 |-  ( 3 - 1 ) = 2
324 323 162 eqtri 
 |-  ( 3 - 1 ) = ( 1 + 1 )
325 324 oveq2i 
 |-  ( ( 2 x. M ) + ( 3 - 1 ) ) = ( ( 2 x. M ) + ( 1 + 1 ) )
326 140 147 321 subadd23d 
 |-  ( M e. NN -> ( ( ( 2 x. M ) - 1 ) + 3 ) = ( ( 2 x. M ) + ( 3 - 1 ) ) )
327 140 147 147 addassd 
 |-  ( M e. NN -> ( ( ( 2 x. M ) + 1 ) + 1 ) = ( ( 2 x. M ) + ( 1 + 1 ) ) )
328 325 326 327 3eqtr4a 
 |-  ( M e. NN -> ( ( ( 2 x. M ) - 1 ) + 3 ) = ( ( ( 2 x. M ) + 1 ) + 1 ) )
329 6 oveq1i 
 |-  ( N + 1 ) = ( ( ( 2 x. M ) + 1 ) + 1 )
330 328 329 eqtr4di 
 |-  ( M e. NN -> ( ( ( 2 x. M ) - 1 ) + 3 ) = ( N + 1 ) )
331 330 oveq2d 
 |-  ( M e. NN -> ( ( 2 x. M ) x. ( ( ( 2 x. M ) - 1 ) + 3 ) ) = ( ( 2 x. M ) x. ( N + 1 ) ) )
332 2cnd 
 |-  ( M e. NN -> 2 e. CC )
333 332 315 321 mul32d 
 |-  ( M e. NN -> ( ( 2 x. M ) x. 3 ) = ( ( 2 x. 3 ) x. M ) )
334 2t3e6 
 |-  ( 2 x. 3 ) = 6
335 334 oveq1i 
 |-  ( ( 2 x. 3 ) x. M ) = ( 6 x. M )
336 333 335 eqtrdi 
 |-  ( M e. NN -> ( ( 2 x. M ) x. 3 ) = ( 6 x. M ) )
337 336 oveq2d 
 |-  ( M e. NN -> ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) + ( ( 2 x. M ) x. 3 ) ) = ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) + ( 6 x. M ) ) )
338 322 331 337 3eqtr3d 
 |-  ( M e. NN -> ( ( 2 x. M ) x. ( N + 1 ) ) = ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) + ( 6 x. M ) ) )
339 338 oveq1d 
 |-  ( M e. NN -> ( ( ( 2 x. M ) x. ( N + 1 ) ) / 6 ) = ( ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) + ( 6 x. M ) ) / 6 ) )
340 mulcl 
 |-  ( ( 6 e. CC /\ M e. CC ) -> ( 6 x. M ) e. CC )
341 174 315 340 sylancr 
 |-  ( M e. NN -> ( 6 x. M ) e. CC )
342 112 a1i 
 |-  ( M e. NN -> 6 =/= 0 )
343 180 341 175 342 divdird 
 |-  ( M e. NN -> ( ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) + ( 6 x. M ) ) / 6 ) = ( ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / 6 ) + ( ( 6 x. M ) / 6 ) ) )
344 315 175 342 divcan3d 
 |-  ( M e. NN -> ( ( 6 x. M ) / 6 ) = M )
345 344 oveq2d 
 |-  ( M e. NN -> ( ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / 6 ) + ( ( 6 x. M ) / 6 ) ) = ( ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / 6 ) + M ) )
346 339 343 345 3eqtrd 
 |-  ( M e. NN -> ( ( ( 2 x. M ) x. ( N + 1 ) ) / 6 ) = ( ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / 6 ) + M ) )
347 319 346 eqtr4d 
 |-  ( M e. NN -> sum_ k e. ( 1 ... M ) ( ( sin ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) = ( ( ( 2 x. M ) x. ( N + 1 ) ) / 6 ) )
348 191 347 oveq12d 
 |-  ( M e. NN -> ( ( ( _pi / N ) ^ 2 ) x. sum_ k e. ( 1 ... M ) ( ( sin ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) ) = ( ( ( _pi ^ 2 ) / ( N ^ 2 ) ) x. ( ( ( 2 x. M ) x. ( N + 1 ) ) / 6 ) ) )
349 140 67 265 67 69 69 divmuldivd 
 |-  ( M e. NN -> ( ( ( 2 x. M ) / N ) x. ( ( N + 1 ) / N ) ) = ( ( ( 2 x. M ) x. ( N + 1 ) ) / ( N x. N ) ) )
350 194 oveq2d 
 |-  ( M e. NN -> ( ( ( 2 x. M ) x. ( N + 1 ) ) / ( N ^ 2 ) ) = ( ( ( 2 x. M ) x. ( N + 1 ) ) / ( N x. N ) ) )
351 349 350 eqtr4d 
 |-  ( M e. NN -> ( ( ( 2 x. M ) / N ) x. ( ( N + 1 ) / N ) ) = ( ( ( 2 x. M ) x. ( N + 1 ) ) / ( N ^ 2 ) ) )
352 351 oveq2d 
 |-  ( M e. NN -> ( ( ( _pi ^ 2 ) / 6 ) x. ( ( ( 2 x. M ) / N ) x. ( ( N + 1 ) / N ) ) ) = ( ( ( _pi ^ 2 ) / 6 ) x. ( ( ( 2 x. M ) x. ( N + 1 ) ) / ( N ^ 2 ) ) ) )
353 278 348 352 3eqtr4d 
 |-  ( M e. NN -> ( ( ( _pi / N ) ^ 2 ) x. sum_ k e. ( 1 ... M ) ( ( sin ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) ) = ( ( ( _pi ^ 2 ) / 6 ) x. ( ( ( 2 x. M ) / N ) x. ( ( N + 1 ) / N ) ) ) )
354 267 271 353 3eqtr4d 
 |-  ( M e. NN -> ( ( ( ( _pi ^ 2 ) / 6 ) x. ( 1 - ( 1 / N ) ) ) x. ( 1 + ( 1 / N ) ) ) = ( ( ( _pi / N ) ^ 2 ) x. sum_ k e. ( 1 ... M ) ( ( sin ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) ) )
355 225 recnd 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( sin ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) e. CC )
356 7 40 355 fsummulc2 
 |-  ( M e. NN -> ( ( ( _pi / N ) ^ 2 ) x. sum_ k e. ( 1 ... M ) ( ( sin ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) ) = sum_ k e. ( 1 ... M ) ( ( ( _pi / N ) ^ 2 ) x. ( ( sin ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) ) )
357 263 354 356 3eqtrd 
 |-  ( M e. NN -> ( K ` M ) = sum_ k e. ( 1 ... M ) ( ( ( _pi / N ) ^ 2 ) x. ( ( sin ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) ) )
358 254 218 357 3brtr4d 
 |-  ( M e. NN -> ( F ` M ) <_ ( K ` M ) )
359 219 358 jca 
 |-  ( M e. NN -> ( ( J ` M ) <_ ( F ` M ) /\ ( F ` M ) <_ ( K ` M ) ) )