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