Metamath Proof Explorer

Theorem basellem9

Description: Lemma for basel . Since by basellem8 F is bounded by two expressions that tend to _pi ^ 2 / 6 , F must also go to _pi ^ 2 / 6 by the squeeze theorem climsqz . But the series F is exactly the partial sums of k ^ -u 2 , so it follows that this is also the value of the infinite sum sum_ k e. NN ( k ^ -u 2 ) . (Contributed by Mario Carneiro, 28-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 ) )
Assertion basellem9 
|- sum_ k e. NN ( k ^ -u 2 ) = ( ( _pi ^ 2 ) / 6 )

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 nnuz 
 |-  NN = ( ZZ>= ` 1 )
7 1zzd 
 |-  ( T. -> 1 e. ZZ )
8 oveq1 
 |-  ( n = k -> ( n ^ -u 2 ) = ( k ^ -u 2 ) )
9 eqid 
 |-  ( n e. NN |-> ( n ^ -u 2 ) ) = ( n e. NN |-> ( n ^ -u 2 ) )
10 ovex 
 |-  ( k ^ -u 2 ) e. _V
11 8 9 10 fvmpt 
 |-  ( k e. NN -> ( ( n e. NN |-> ( n ^ -u 2 ) ) ` k ) = ( k ^ -u 2 ) )
12 11 adantl 
 |-  ( ( T. /\ k e. NN ) -> ( ( n e. NN |-> ( n ^ -u 2 ) ) ` k ) = ( k ^ -u 2 ) )
13 nnre 
 |-  ( n e. NN -> n e. RR )
14 nnne0 
 |-  ( n e. NN -> n =/= 0 )
15 2z 
 |-  2 e. ZZ
16 znegcl 
 |-  ( 2 e. ZZ -> -u 2 e. ZZ )
17 15 16 ax-mp 
 |-  -u 2 e. ZZ
18 17 a1i 
 |-  ( n e. NN -> -u 2 e. ZZ )
19 13 14 18 reexpclzd 
 |-  ( n e. NN -> ( n ^ -u 2 ) e. RR )
20 19 adantl 
 |-  ( ( T. /\ n e. NN ) -> ( n ^ -u 2 ) e. RR )
21 20 9 fmptd 
 |-  ( T. -> ( n e. NN |-> ( n ^ -u 2 ) ) : NN --> RR )
22 21 ffvelcdmda 
 |-  ( ( T. /\ k e. NN ) -> ( ( n e. NN |-> ( n ^ -u 2 ) ) ` k ) e. RR )
23 12 22 eqeltrrd 
 |-  ( ( T. /\ k e. NN ) -> ( k ^ -u 2 ) e. RR )
24 23 recnd 
 |-  ( ( T. /\ k e. NN ) -> ( k ^ -u 2 ) e. CC )
25 6 7 22 serfre 
 |-  ( T. -> seq 1 ( + , ( n e. NN |-> ( n ^ -u 2 ) ) ) : NN --> RR )
26 2 feq1i 
 |-  ( F : NN --> RR <-> seq 1 ( + , ( n e. NN |-> ( n ^ -u 2 ) ) ) : NN --> RR )
27 25 26 sylibr 
 |-  ( T. -> F : NN --> RR )
28 27 ffvelcdmda 
 |-  ( ( T. /\ n e. NN ) -> ( F ` n ) e. RR )
29 28 recnd 
 |-  ( ( T. /\ n e. NN ) -> ( F ` n ) e. CC )
30 remulcl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x x. y ) e. RR )
31 30 adantl 
 |-  ( ( T. /\ ( x e. RR /\ y e. RR ) ) -> ( x x. y ) e. RR )
32 ovex 
 |-  ( ( _pi ^ 2 ) / 6 ) e. _V
33 32 fconst 
 |-  ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) : NN --> { ( ( _pi ^ 2 ) / 6 ) }
34 pire 
 |-  _pi e. RR
35 34 resqcli 
 |-  ( _pi ^ 2 ) e. RR
36 6re 
 |-  6 e. RR
37 6nn 
 |-  6 e. NN
38 37 nnne0i 
 |-  6 =/= 0
39 35 36 38 redivcli 
 |-  ( ( _pi ^ 2 ) / 6 ) e. RR
40 39 a1i 
 |-  ( T. -> ( ( _pi ^ 2 ) / 6 ) e. RR )
41 40 snssd 
 |-  ( T. -> { ( ( _pi ^ 2 ) / 6 ) } C_ RR )
42 fss 
 |-  ( ( ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) : NN --> { ( ( _pi ^ 2 ) / 6 ) } /\ { ( ( _pi ^ 2 ) / 6 ) } C_ RR ) -> ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) : NN --> RR )
43 33 41 42 sylancr 
 |-  ( T. -> ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) : NN --> RR )
44 resubcl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x - y ) e. RR )
45 44 adantl 
 |-  ( ( T. /\ ( x e. RR /\ y e. RR ) ) -> ( x - y ) e. RR )
46 1ex 
 |-  1 e. _V
47 46 fconst 
 |-  ( NN X. { 1 } ) : NN --> { 1 }
48 1red 
 |-  ( T. -> 1 e. RR )
49 48 snssd 
 |-  ( T. -> { 1 } C_ RR )
50 fss 
 |-  ( ( ( NN X. { 1 } ) : NN --> { 1 } /\ { 1 } C_ RR ) -> ( NN X. { 1 } ) : NN --> RR )
51 47 49 50 sylancr 
 |-  ( T. -> ( NN X. { 1 } ) : NN --> RR )
52 2nn 
 |-  2 e. NN
53 52 a1i 
 |-  ( T. -> 2 e. NN )
54 nnmulcl 
 |-  ( ( 2 e. NN /\ n e. NN ) -> ( 2 x. n ) e. NN )
55 53 54 sylan 
 |-  ( ( T. /\ n e. NN ) -> ( 2 x. n ) e. NN )
56 55 peano2nnd 
 |-  ( ( T. /\ n e. NN ) -> ( ( 2 x. n ) + 1 ) e. NN )
57 56 nnrecred 
 |-  ( ( T. /\ n e. NN ) -> ( 1 / ( ( 2 x. n ) + 1 ) ) e. RR )
58 57 1 fmptd 
 |-  ( T. -> G : NN --> RR )
59 nnex 
 |-  NN e. _V
60 59 a1i 
 |-  ( T. -> NN e. _V )
61 inidm 
 |-  ( NN i^i NN ) = NN
62 45 51 58 60 60 61 off 
 |-  ( T. -> ( ( NN X. { 1 } ) oF - G ) : NN --> RR )
63 31 43 62 60 60 61 off 
 |-  ( T. -> ( ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) oF x. ( ( NN X. { 1 } ) oF - G ) ) : NN --> RR )
64 3 feq1i 
 |-  ( H : NN --> RR <-> ( ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) oF x. ( ( NN X. { 1 } ) oF - G ) ) : NN --> RR )
65 63 64 sylibr 
 |-  ( T. -> H : NN --> RR )
66 readdcl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + y ) e. RR )
67 66 adantl 
 |-  ( ( T. /\ ( x e. RR /\ y e. RR ) ) -> ( x + y ) e. RR )
68 negex 
 |-  -u 2 e. _V
69 68 fconst 
 |-  ( NN X. { -u 2 } ) : NN --> { -u 2 }
70 17 zrei 
 |-  -u 2 e. RR
71 70 a1i 
 |-  ( T. -> -u 2 e. RR )
72 71 snssd 
 |-  ( T. -> { -u 2 } C_ RR )
73 fss 
 |-  ( ( ( NN X. { -u 2 } ) : NN --> { -u 2 } /\ { -u 2 } C_ RR ) -> ( NN X. { -u 2 } ) : NN --> RR )
74 69 72 73 sylancr 
 |-  ( T. -> ( NN X. { -u 2 } ) : NN --> RR )
75 31 74 58 60 60 61 off 
 |-  ( T. -> ( ( NN X. { -u 2 } ) oF x. G ) : NN --> RR )
76 67 51 75 60 60 61 off 
 |-  ( T. -> ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) : NN --> RR )
77 31 65 76 60 60 61 off 
 |-  ( T. -> ( H oF x. ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ) : NN --> RR )
78 4 feq1i 
 |-  ( J : NN --> RR <-> ( H oF x. ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ) : NN --> RR )
79 77 78 sylibr 
 |-  ( T. -> J : NN --> RR )
80 79 ffvelcdmda 
 |-  ( ( T. /\ n e. NN ) -> ( J ` n ) e. RR )
81 80 recnd 
 |-  ( ( T. /\ n e. NN ) -> ( J ` n ) e. CC )
82 29 81 npcand 
 |-  ( ( T. /\ n e. NN ) -> ( ( ( F ` n ) - ( J ` n ) ) + ( J ` n ) ) = ( F ` n ) )
83 82 mpteq2dva 
 |-  ( T. -> ( n e. NN |-> ( ( ( F ` n ) - ( J ` n ) ) + ( J ` n ) ) ) = ( n e. NN |-> ( F ` n ) ) )
84 ovexd 
 |-  ( ( T. /\ n e. NN ) -> ( ( F ` n ) - ( J ` n ) ) e. _V )
85 27 feqmptd 
 |-  ( T. -> F = ( n e. NN |-> ( F ` n ) ) )
86 79 feqmptd 
 |-  ( T. -> J = ( n e. NN |-> ( J ` n ) ) )
87 60 28 80 85 86 offval2 
 |-  ( T. -> ( F oF - J ) = ( n e. NN |-> ( ( F ` n ) - ( J ` n ) ) ) )
88 60 84 80 87 86 offval2 
 |-  ( T. -> ( ( F oF - J ) oF + J ) = ( n e. NN |-> ( ( ( F ` n ) - ( J ` n ) ) + ( J ` n ) ) ) )
89 83 88 85 3eqtr4d 
 |-  ( T. -> ( ( F oF - J ) oF + J ) = F )
90 67 51 58 60 60 61 off 
 |-  ( T. -> ( ( NN X. { 1 } ) oF + G ) : NN --> RR )
91 recn 
 |-  ( x e. RR -> x e. CC )
92 recn 
 |-  ( y e. RR -> y e. CC )
93 recn 
 |-  ( z e. RR -> z e. CC )
94 subdi 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( x x. ( y - z ) ) = ( ( x x. y ) - ( x x. z ) ) )
95 91 92 93 94 syl3an 
 |-  ( ( x e. RR /\ y e. RR /\ z e. RR ) -> ( x x. ( y - z ) ) = ( ( x x. y ) - ( x x. z ) ) )
96 95 adantl 
 |-  ( ( T. /\ ( x e. RR /\ y e. RR /\ z e. RR ) ) -> ( x x. ( y - z ) ) = ( ( x x. y ) - ( x x. z ) ) )
97 60 65 90 76 96 caofdi 
 |-  ( T. -> ( H oF x. ( ( ( NN X. { 1 } ) oF + G ) oF - ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ) ) = ( ( H oF x. ( ( NN X. { 1 } ) oF + G ) ) oF - ( H oF x. ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ) ) )
98 5 4 oveq12i 
 |-  ( K oF - J ) = ( ( H oF x. ( ( NN X. { 1 } ) oF + G ) ) oF - ( H oF x. ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ) )
99 97 98 eqtr4di 
 |-  ( T. -> ( H oF x. ( ( ( NN X. { 1 } ) oF + G ) oF - ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ) ) = ( K oF - J ) )
100 39 recni 
 |-  ( ( _pi ^ 2 ) / 6 ) e. CC
101 6 eqimss2i 
 |-  ( ZZ>= ` 1 ) C_ NN
102 101 59 climconst2 
 |-  ( ( ( ( _pi ^ 2 ) / 6 ) e. CC /\ 1 e. ZZ ) -> ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) ~~> ( ( _pi ^ 2 ) / 6 ) )
103 100 7 102 sylancr 
 |-  ( T. -> ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) ~~> ( ( _pi ^ 2 ) / 6 ) )
104 ovexd 
 |-  ( T. -> ( ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) oF x. ( ( NN X. { 1 } ) oF - G ) ) e. _V )
105 ax-resscn 
 |-  RR C_ CC
106 fss 
 |-  ( ( ( NN X. { 1 } ) : NN --> RR /\ RR C_ CC ) -> ( NN X. { 1 } ) : NN --> CC )
107 51 105 106 sylancl 
 |-  ( T. -> ( NN X. { 1 } ) : NN --> CC )
108 fss 
 |-  ( ( G : NN --> RR /\ RR C_ CC ) -> G : NN --> CC )
109 58 105 108 sylancl 
 |-  ( T. -> G : NN --> CC )
110 ofnegsub 
 |-  ( ( NN e. _V /\ ( NN X. { 1 } ) : NN --> CC /\ G : NN --> CC ) -> ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 1 } ) oF x. G ) ) = ( ( NN X. { 1 } ) oF - G ) )
111 59 107 109 110 mp3an2i 
 |-  ( T. -> ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 1 } ) oF x. G ) ) = ( ( NN X. { 1 } ) oF - G ) )
112 neg1cn 
 |-  -u 1 e. CC
113 1 112 basellem7 
 |-  ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 1 } ) oF x. G ) ) ~~> 1
114 111 113 eqbrtrrdi 
 |-  ( T. -> ( ( NN X. { 1 } ) oF - G ) ~~> 1 )
115 43 ffvelcdmda 
 |-  ( ( T. /\ k e. NN ) -> ( ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) ` k ) e. RR )
116 115 recnd 
 |-  ( ( T. /\ k e. NN ) -> ( ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) ` k ) e. CC )
117 62 ffvelcdmda 
 |-  ( ( T. /\ k e. NN ) -> ( ( ( NN X. { 1 } ) oF - G ) ` k ) e. RR )
118 117 recnd 
 |-  ( ( T. /\ k e. NN ) -> ( ( ( NN X. { 1 } ) oF - G ) ` k ) e. CC )
119 43 ffnd 
 |-  ( T. -> ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) Fn NN )
120 fnconstg 
 |-  ( 1 e. ZZ -> ( NN X. { 1 } ) Fn NN )
121 7 120 syl 
 |-  ( T. -> ( NN X. { 1 } ) Fn NN )
122 58 ffnd 
 |-  ( T. -> G Fn NN )
123 121 122 60 60 61 offn 
 |-  ( T. -> ( ( NN X. { 1 } ) oF - G ) Fn NN )
124 eqidd 
 |-  ( ( T. /\ k e. NN ) -> ( ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) ` k ) = ( ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) ` k ) )
125 eqidd 
 |-  ( ( T. /\ k e. NN ) -> ( ( ( NN X. { 1 } ) oF - G ) ` k ) = ( ( ( NN X. { 1 } ) oF - G ) ` k ) )
126 119 123 60 60 61 124 125 ofval 
 |-  ( ( T. /\ k e. NN ) -> ( ( ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) oF x. ( ( NN X. { 1 } ) oF - G ) ) ` k ) = ( ( ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) ` k ) x. ( ( ( NN X. { 1 } ) oF - G ) ` k ) ) )
127 6 7 103 104 114 116 118 126 climmul 
 |-  ( T. -> ( ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) oF x. ( ( NN X. { 1 } ) oF - G ) ) ~~> ( ( ( _pi ^ 2 ) / 6 ) x. 1 ) )
128 100 mulridi 
 |-  ( ( ( _pi ^ 2 ) / 6 ) x. 1 ) = ( ( _pi ^ 2 ) / 6 )
129 127 128 breqtrdi 
 |-  ( T. -> ( ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) oF x. ( ( NN X. { 1 } ) oF - G ) ) ~~> ( ( _pi ^ 2 ) / 6 ) )
130 3 129 eqbrtrid 
 |-  ( T. -> H ~~> ( ( _pi ^ 2 ) / 6 ) )
131 ovexd 
 |-  ( T. -> ( H oF x. ( ( ( NN X. { 1 } ) oF + G ) oF - ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ) ) e. _V )
132 3cn 
 |-  3 e. CC
133 101 59 climconst2 
 |-  ( ( 3 e. CC /\ 1 e. ZZ ) -> ( NN X. { 3 } ) ~~> 3 )
134 132 7 133 sylancr 
 |-  ( T. -> ( NN X. { 3 } ) ~~> 3 )
135 ovexd 
 |-  ( T. -> ( ( NN X. { 3 } ) oF x. G ) e. _V )
136 1 basellem6 
 |-  G ~~> 0
137 136 a1i 
 |-  ( T. -> G ~~> 0 )
138 3ex 
 |-  3 e. _V
139 138 fconst 
 |-  ( NN X. { 3 } ) : NN --> { 3 }
140 3re 
 |-  3 e. RR
141 140 a1i 
 |-  ( T. -> 3 e. RR )
142 141 snssd 
 |-  ( T. -> { 3 } C_ RR )
143 fss 
 |-  ( ( ( NN X. { 3 } ) : NN --> { 3 } /\ { 3 } C_ RR ) -> ( NN X. { 3 } ) : NN --> RR )
144 139 142 143 sylancr 
 |-  ( T. -> ( NN X. { 3 } ) : NN --> RR )
145 144 ffvelcdmda 
 |-  ( ( T. /\ k e. NN ) -> ( ( NN X. { 3 } ) ` k ) e. RR )
146 145 recnd 
 |-  ( ( T. /\ k e. NN ) -> ( ( NN X. { 3 } ) ` k ) e. CC )
147 58 ffvelcdmda 
 |-  ( ( T. /\ k e. NN ) -> ( G ` k ) e. RR )
148 147 recnd 
 |-  ( ( T. /\ k e. NN ) -> ( G ` k ) e. CC )
149 144 ffnd 
 |-  ( T. -> ( NN X. { 3 } ) Fn NN )
150 eqidd 
 |-  ( ( T. /\ k e. NN ) -> ( ( NN X. { 3 } ) ` k ) = ( ( NN X. { 3 } ) ` k ) )
151 eqidd 
 |-  ( ( T. /\ k e. NN ) -> ( G ` k ) = ( G ` k ) )
152 149 122 60 60 61 150 151 ofval 
 |-  ( ( T. /\ k e. NN ) -> ( ( ( NN X. { 3 } ) oF x. G ) ` k ) = ( ( ( NN X. { 3 } ) ` k ) x. ( G ` k ) ) )
153 6 7 134 135 137 146 148 152 climmul 
 |-  ( T. -> ( ( NN X. { 3 } ) oF x. G ) ~~> ( 3 x. 0 ) )
154 132 mul01i 
 |-  ( 3 x. 0 ) = 0
155 153 154 breqtrdi 
 |-  ( T. -> ( ( NN X. { 3 } ) oF x. G ) ~~> 0 )
156 65 ffvelcdmda 
 |-  ( ( T. /\ k e. NN ) -> ( H ` k ) e. RR )
157 156 recnd 
 |-  ( ( T. /\ k e. NN ) -> ( H ` k ) e. CC )
158 31 144 58 60 60 61 off 
 |-  ( T. -> ( ( NN X. { 3 } ) oF x. G ) : NN --> RR )
159 158 ffvelcdmda 
 |-  ( ( T. /\ k e. NN ) -> ( ( ( NN X. { 3 } ) oF x. G ) ` k ) e. RR )
160 159 recnd 
 |-  ( ( T. /\ k e. NN ) -> ( ( ( NN X. { 3 } ) oF x. G ) ` k ) e. CC )
161 65 ffnd 
 |-  ( T. -> H Fn NN )
162 45 90 76 60 60 61 off 
 |-  ( T. -> ( ( ( NN X. { 1 } ) oF + G ) oF - ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ) : NN --> RR )
163 162 ffnd 
 |-  ( T. -> ( ( ( NN X. { 1 } ) oF + G ) oF - ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ) Fn NN )
164 eqidd 
 |-  ( ( T. /\ k e. NN ) -> ( H ` k ) = ( H ` k ) )
165 148 mullidd 
 |-  ( ( T. /\ k e. NN ) -> ( 1 x. ( G ` k ) ) = ( G ` k ) )
166 2cn 
 |-  2 e. CC
167 mulneg1 
 |-  ( ( 2 e. CC /\ ( G ` k ) e. CC ) -> ( -u 2 x. ( G ` k ) ) = -u ( 2 x. ( G ` k ) ) )
168 166 148 167 sylancr 
 |-  ( ( T. /\ k e. NN ) -> ( -u 2 x. ( G ` k ) ) = -u ( 2 x. ( G ` k ) ) )
169 168 negeqd 
 |-  ( ( T. /\ k e. NN ) -> -u ( -u 2 x. ( G ` k ) ) = -u -u ( 2 x. ( G ` k ) ) )
170 mulcl 
 |-  ( ( 2 e. CC /\ ( G ` k ) e. CC ) -> ( 2 x. ( G ` k ) ) e. CC )
171 166 148 170 sylancr 
 |-  ( ( T. /\ k e. NN ) -> ( 2 x. ( G ` k ) ) e. CC )
172 171 negnegd 
 |-  ( ( T. /\ k e. NN ) -> -u -u ( 2 x. ( G ` k ) ) = ( 2 x. ( G ` k ) ) )
173 169 172 eqtr2d 
 |-  ( ( T. /\ k e. NN ) -> ( 2 x. ( G ` k ) ) = -u ( -u 2 x. ( G ` k ) ) )
174 165 173 oveq12d 
 |-  ( ( T. /\ k e. NN ) -> ( ( 1 x. ( G ` k ) ) + ( 2 x. ( G ` k ) ) ) = ( ( G ` k ) + -u ( -u 2 x. ( G ` k ) ) ) )
175 remulcl 
 |-  ( ( -u 2 e. RR /\ ( G ` k ) e. RR ) -> ( -u 2 x. ( G ` k ) ) e. RR )
176 70 147 175 sylancr 
 |-  ( ( T. /\ k e. NN ) -> ( -u 2 x. ( G ` k ) ) e. RR )
177 176 recnd 
 |-  ( ( T. /\ k e. NN ) -> ( -u 2 x. ( G ` k ) ) e. CC )
178 148 177 negsubd 
 |-  ( ( T. /\ k e. NN ) -> ( ( G ` k ) + -u ( -u 2 x. ( G ` k ) ) ) = ( ( G ` k ) - ( -u 2 x. ( G ` k ) ) ) )
179 174 178 eqtrd 
 |-  ( ( T. /\ k e. NN ) -> ( ( 1 x. ( G ` k ) ) + ( 2 x. ( G ` k ) ) ) = ( ( G ` k ) - ( -u 2 x. ( G ` k ) ) ) )
180 df-3 
 |-  3 = ( 2 + 1 )
181 ax-1cn 
 |-  1 e. CC
182 166 181 addcomi 
 |-  ( 2 + 1 ) = ( 1 + 2 )
183 180 182 eqtri 
 |-  3 = ( 1 + 2 )
184 183 oveq1i 
 |-  ( 3 x. ( G ` k ) ) = ( ( 1 + 2 ) x. ( G ` k ) )
185 1cnd 
 |-  ( ( T. /\ k e. NN ) -> 1 e. CC )
186 166 a1i 
 |-  ( ( T. /\ k e. NN ) -> 2 e. CC )
187 185 186 148 adddird 
 |-  ( ( T. /\ k e. NN ) -> ( ( 1 + 2 ) x. ( G ` k ) ) = ( ( 1 x. ( G ` k ) ) + ( 2 x. ( G ` k ) ) ) )
188 184 187 eqtrid 
 |-  ( ( T. /\ k e. NN ) -> ( 3 x. ( G ` k ) ) = ( ( 1 x. ( G ` k ) ) + ( 2 x. ( G ` k ) ) ) )
189 185 148 177 pnpcand 
 |-  ( ( T. /\ k e. NN ) -> ( ( 1 + ( G ` k ) ) - ( 1 + ( -u 2 x. ( G ` k ) ) ) ) = ( ( G ` k ) - ( -u 2 x. ( G ` k ) ) ) )
190 179 188 189 3eqtr4rd 
 |-  ( ( T. /\ k e. NN ) -> ( ( 1 + ( G ` k ) ) - ( 1 + ( -u 2 x. ( G ` k ) ) ) ) = ( 3 x. ( G ` k ) ) )
191 121 122 60 60 61 offn 
 |-  ( T. -> ( ( NN X. { 1 } ) oF + G ) Fn NN )
192 17 a1i 
 |-  ( T. -> -u 2 e. ZZ )
193 fnconstg 
 |-  ( -u 2 e. ZZ -> ( NN X. { -u 2 } ) Fn NN )
194 192 193 syl 
 |-  ( T. -> ( NN X. { -u 2 } ) Fn NN )
195 194 122 60 60 61 offn 
 |-  ( T. -> ( ( NN X. { -u 2 } ) oF x. G ) Fn NN )
196 121 195 60 60 61 offn 
 |-  ( T. -> ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) Fn NN )
197 60 48 122 151 ofc1 
 |-  ( ( T. /\ k e. NN ) -> ( ( ( NN X. { 1 } ) oF + G ) ` k ) = ( 1 + ( G ` k ) ) )
198 60 71 122 151 ofc1 
 |-  ( ( T. /\ k e. NN ) -> ( ( ( NN X. { -u 2 } ) oF x. G ) ` k ) = ( -u 2 x. ( G ` k ) ) )
199 60 48 195 198 ofc1 
 |-  ( ( T. /\ k e. NN ) -> ( ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ` k ) = ( 1 + ( -u 2 x. ( G ` k ) ) ) )
200 191 196 60 60 61 197 199 ofval 
 |-  ( ( T. /\ k e. NN ) -> ( ( ( ( NN X. { 1 } ) oF + G ) oF - ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ) ` k ) = ( ( 1 + ( G ` k ) ) - ( 1 + ( -u 2 x. ( G ` k ) ) ) ) )
201 60 141 122 151 ofc1 
 |-  ( ( T. /\ k e. NN ) -> ( ( ( NN X. { 3 } ) oF x. G ) ` k ) = ( 3 x. ( G ` k ) ) )
202 190 200 201 3eqtr4d 
 |-  ( ( T. /\ k e. NN ) -> ( ( ( ( NN X. { 1 } ) oF + G ) oF - ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ) ` k ) = ( ( ( NN X. { 3 } ) oF x. G ) ` k ) )
203 161 163 60 60 61 164 202 ofval 
 |-  ( ( T. /\ k e. NN ) -> ( ( H oF x. ( ( ( NN X. { 1 } ) oF + G ) oF - ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ) ) ` k ) = ( ( H ` k ) x. ( ( ( NN X. { 3 } ) oF x. G ) ` k ) ) )
204 6 7 130 131 155 157 160 203 climmul 
 |-  ( T. -> ( H oF x. ( ( ( NN X. { 1 } ) oF + G ) oF - ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ) ) ~~> ( ( ( _pi ^ 2 ) / 6 ) x. 0 ) )
205 100 mul01i 
 |-  ( ( ( _pi ^ 2 ) / 6 ) x. 0 ) = 0
206 204 205 breqtrdi 
 |-  ( T. -> ( H oF x. ( ( ( NN X. { 1 } ) oF + G ) oF - ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ) ) ~~> 0 )
207 99 206 eqbrtrrd 
 |-  ( T. -> ( K oF - J ) ~~> 0 )
208 ovexd 
 |-  ( T. -> ( F oF - J ) e. _V )
209 31 65 90 60 60 61 off 
 |-  ( T. -> ( H oF x. ( ( NN X. { 1 } ) oF + G ) ) : NN --> RR )
210 5 feq1i 
 |-  ( K : NN --> RR <-> ( H oF x. ( ( NN X. { 1 } ) oF + G ) ) : NN --> RR )
211 209 210 sylibr 
 |-  ( T. -> K : NN --> RR )
212 45 211 79 60 60 61 off 
 |-  ( T. -> ( K oF - J ) : NN --> RR )
213 212 ffvelcdmda 
 |-  ( ( T. /\ k e. NN ) -> ( ( K oF - J ) ` k ) e. RR )
214 45 27 79 60 60 61 off 
 |-  ( T. -> ( F oF - J ) : NN --> RR )
215 214 ffvelcdmda 
 |-  ( ( T. /\ k e. NN ) -> ( ( F oF - J ) ` k ) e. RR )
216 27 ffvelcdmda 
 |-  ( ( T. /\ k e. NN ) -> ( F ` k ) e. RR )
217 211 ffvelcdmda 
 |-  ( ( T. /\ k e. NN ) -> ( K ` k ) e. RR )
218 79 ffvelcdmda 
 |-  ( ( T. /\ k e. NN ) -> ( J ` k ) e. RR )
219 eqid 
 |-  ( ( 2 x. k ) + 1 ) = ( ( 2 x. k ) + 1 )
220 1 2 3 4 5 219 basellem8 
 |-  ( k e. NN -> ( ( J ` k ) <_ ( F ` k ) /\ ( F ` k ) <_ ( K ` k ) ) )
221 220 adantl 
 |-  ( ( T. /\ k e. NN ) -> ( ( J ` k ) <_ ( F ` k ) /\ ( F ` k ) <_ ( K ` k ) ) )
222 221 simprd 
 |-  ( ( T. /\ k e. NN ) -> ( F ` k ) <_ ( K ` k ) )
223 216 217 218 222 lesub1dd 
 |-  ( ( T. /\ k e. NN ) -> ( ( F ` k ) - ( J ` k ) ) <_ ( ( K ` k ) - ( J ` k ) ) )
224 27 ffnd 
 |-  ( T. -> F Fn NN )
225 79 ffnd 
 |-  ( T. -> J Fn NN )
226 eqidd 
 |-  ( ( T. /\ k e. NN ) -> ( F ` k ) = ( F ` k ) )
227 eqidd 
 |-  ( ( T. /\ k e. NN ) -> ( J ` k ) = ( J ` k ) )
228 224 225 60 60 61 226 227 ofval 
 |-  ( ( T. /\ k e. NN ) -> ( ( F oF - J ) ` k ) = ( ( F ` k ) - ( J ` k ) ) )
229 211 ffnd 
 |-  ( T. -> K Fn NN )
230 eqidd 
 |-  ( ( T. /\ k e. NN ) -> ( K ` k ) = ( K ` k ) )
231 229 225 60 60 61 230 227 ofval 
 |-  ( ( T. /\ k e. NN ) -> ( ( K oF - J ) ` k ) = ( ( K ` k ) - ( J ` k ) ) )
232 223 228 231 3brtr4d 
 |-  ( ( T. /\ k e. NN ) -> ( ( F oF - J ) ` k ) <_ ( ( K oF - J ) ` k ) )
233 221 simpld 
 |-  ( ( T. /\ k e. NN ) -> ( J ` k ) <_ ( F ` k ) )
234 216 218 subge0d 
 |-  ( ( T. /\ k e. NN ) -> ( 0 <_ ( ( F ` k ) - ( J ` k ) ) <-> ( J ` k ) <_ ( F ` k ) ) )
235 233 234 mpbird 
 |-  ( ( T. /\ k e. NN ) -> 0 <_ ( ( F ` k ) - ( J ` k ) ) )
236 235 228 breqtrrd 
 |-  ( ( T. /\ k e. NN ) -> 0 <_ ( ( F oF - J ) ` k ) )
237 6 7 207 208 213 215 232 236 climsqz2 
 |-  ( T. -> ( F oF - J ) ~~> 0 )
238 ovexd 
 |-  ( T. -> ( ( F oF - J ) oF + J ) e. _V )
239 ovexd 
 |-  ( T. -> ( H oF x. ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ) e. _V )
240 70 recni 
 |-  -u 2 e. CC
241 1 240 basellem7 
 |-  ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ~~> 1
242 241 a1i 
 |-  ( T. -> ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ~~> 1 )
243 76 ffvelcdmda 
 |-  ( ( T. /\ k e. NN ) -> ( ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ` k ) e. RR )
244 243 recnd 
 |-  ( ( T. /\ k e. NN ) -> ( ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ` k ) e. CC )
245 eqidd 
 |-  ( ( T. /\ k e. NN ) -> ( ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ` k ) = ( ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ` k ) )
246 161 196 60 60 61 164 245 ofval 
 |-  ( ( T. /\ k e. NN ) -> ( ( H oF x. ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ) ` k ) = ( ( H ` k ) x. ( ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ` k ) ) )
247 6 7 130 239 242 157 244 246 climmul 
 |-  ( T. -> ( H oF x. ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ) ~~> ( ( ( _pi ^ 2 ) / 6 ) x. 1 ) )
248 247 128 breqtrdi 
 |-  ( T. -> ( H oF x. ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) ) ~~> ( ( _pi ^ 2 ) / 6 ) )
249 4 248 eqbrtrid 
 |-  ( T. -> J ~~> ( ( _pi ^ 2 ) / 6 ) )
250 215 recnd 
 |-  ( ( T. /\ k e. NN ) -> ( ( F oF - J ) ` k ) e. CC )
251 218 recnd 
 |-  ( ( T. /\ k e. NN ) -> ( J ` k ) e. CC )
252 214 ffnd 
 |-  ( T. -> ( F oF - J ) Fn NN )
253 eqidd 
 |-  ( ( T. /\ k e. NN ) -> ( ( F oF - J ) ` k ) = ( ( F oF - J ) ` k ) )
254 252 225 60 60 61 253 227 ofval 
 |-  ( ( T. /\ k e. NN ) -> ( ( ( F oF - J ) oF + J ) ` k ) = ( ( ( F oF - J ) ` k ) + ( J ` k ) ) )
255 6 7 237 238 249 250 251 254 climadd 
 |-  ( T. -> ( ( F oF - J ) oF + J ) ~~> ( 0 + ( ( _pi ^ 2 ) / 6 ) ) )
256 89 255 eqbrtrrd 
 |-  ( T. -> F ~~> ( 0 + ( ( _pi ^ 2 ) / 6 ) ) )
257 100 addlidi 
 |-  ( 0 + ( ( _pi ^ 2 ) / 6 ) ) = ( ( _pi ^ 2 ) / 6 )
258 256 2 257 3brtr3g 
 |-  ( T. -> seq 1 ( + , ( n e. NN |-> ( n ^ -u 2 ) ) ) ~~> ( ( _pi ^ 2 ) / 6 ) )
259 6 7 12 24 258 isumclim 
 |-  ( T. -> sum_ k e. NN ( k ^ -u 2 ) = ( ( _pi ^ 2 ) / 6 ) )
260 259 mptru 
 |-  sum_ k e. NN ( k ^ -u 2 ) = ( ( _pi ^ 2 ) / 6 )