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

Theorem basellem9 20740
Description: Lemma for basel 20741. Since by basellem8 20739 
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 12363. 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.)
Hypotheses
Ref Expression
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 ) } )  o F  x.  (
( NN  X.  {
1 } )  o F  -  G ) )
basel.j  |-  J  =  ( H  o F  x.  ( ( NN 
X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G
) ) )
basel.k  |-  K  =  ( H  o F  x.  ( ( NN 
X.  { 1 } )  o F  +  G ) )
Assertion
Ref Expression
basellem9  |-  sum_ k  e.  NN  ( k ^ -u 2 )  =  ( ( pi ^ 2 )  /  6 )
Distinct variable groups:    k, n, F    k, G    k, H    k, J, n    k, K
Allowed substitution hints:    G( n)    H( n)    K( n)

Proof of Theorem basellem9
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 10455 . . 3  |-  NN  =  ( ZZ>= `  1 )
2 1z 10245 . . . 4  |-  1  e.  ZZ
32a1i 11 . . 3  |-  (  T. 
->  1  e.  ZZ )
4 oveq1 6029 . . . . 5  |-  ( n  =  k  ->  (
n ^ -u 2
)  =  ( k ^ -u 2 ) )
5 eqid 2389 . . . . 5  |-  ( n  e.  NN  |->  ( n ^ -u 2 ) )  =  ( n  e.  NN  |->  ( n ^ -u 2 ) )
6 ovex 6047 . . . . 5  |-  ( k ^ -u 2 )  e.  _V
74, 5, 6fvmpt 5747 . . . 4  |-  ( k  e.  NN  ->  (
( n  e.  NN  |->  ( n ^ -u 2
) ) `  k
)  =  ( k ^ -u 2 ) )
87adantl 453 . . 3  |-  ( (  T.  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( n ^ -u 2
) ) `  k
)  =  ( k ^ -u 2 ) )
9 nnre 9941 . . . . . . . . 9  |-  ( n  e.  NN  ->  n  e.  RR )
10 nnne0 9966 . . . . . . . . 9  |-  ( n  e.  NN  ->  n  =/=  0 )
11 2z 10246 . . . . . . . . . . 11  |-  2  e.  ZZ
12 znegcl 10247 . . . . . . . . . . 11  |-  ( 2  e.  ZZ  ->  -u 2  e.  ZZ )
1311, 12ax-mp 8 . . . . . . . . . 10  |-  -u 2  e.  ZZ
1413a1i 11 . . . . . . . . 9  |-  ( n  e.  NN  ->  -u 2  e.  ZZ )
159, 10, 14reexpclzd 11477 . . . . . . . 8  |-  ( n  e.  NN  ->  (
n ^ -u 2
)  e.  RR )
1615adantl 453 . . . . . . 7  |-  ( (  T.  /\  n  e.  NN )  ->  (
n ^ -u 2
)  e.  RR )
1716, 5fmptd 5834 . . . . . 6  |-  (  T. 
->  ( n  e.  NN  |->  ( n ^ -u 2
) ) : NN --> RR )
1817ffvelrnda 5811 . . . . 5  |-  ( (  T.  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( n ^ -u 2
) ) `  k
)  e.  RR )
198, 18eqeltrrd 2464 . . . 4  |-  ( (  T.  /\  k  e.  NN )  ->  (
k ^ -u 2
)  e.  RR )
2019recnd 9049 . . 3  |-  ( (  T.  /\  k  e.  NN )  ->  (
k ^ -u 2
)  e.  CC )
211, 3, 18serfre 11281 . . . . . . . . . . 11  |-  (  T. 
->  seq  1 (  +  ,  ( n  e.  NN  |->  ( n ^ -u 2 ) ) ) : NN --> RR )
22 basel.f . . . . . . . . . . . 12  |-  F  =  seq  1 (  +  ,  ( n  e.  NN  |->  ( n ^ -u 2 ) ) )
2322feq1i 5527 . . . . . . . . . . 11  |-  ( F : NN --> RR  <->  seq  1
(  +  ,  ( n  e.  NN  |->  ( n ^ -u 2
) ) ) : NN --> RR )
2421, 23sylibr 204 . . . . . . . . . 10  |-  (  T. 
->  F : NN --> RR )
2524ffvelrnda 5811 . . . . . . . . 9  |-  ( (  T.  /\  n  e.  NN )  ->  ( F `  n )  e.  RR )
2625recnd 9049 . . . . . . . 8  |-  ( (  T.  /\  n  e.  NN )  ->  ( F `  n )  e.  CC )
27 remulcl 9010 . . . . . . . . . . . . 13  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( x  x.  y
)  e.  RR )
2827adantl 453 . . . . . . . . . . . 12  |-  ( (  T.  /\  ( x  e.  RR  /\  y  e.  RR ) )  -> 
( x  x.  y
)  e.  RR )
29 ovex 6047 . . . . . . . . . . . . . . . 16  |-  ( ( pi ^ 2 )  /  6 )  e. 
_V
3029fconst 5571 . . . . . . . . . . . . . . 15  |-  ( NN 
X.  { ( ( pi ^ 2 )  /  6 ) } ) : NN --> { ( ( pi ^ 2 )  /  6 ) }
31 pire 20241 . . . . . . . . . . . . . . . . . . 19  |-  pi  e.  RR
3231resqcli 11396 . . . . . . . . . . . . . . . . . 18  |-  ( pi
^ 2 )  e.  RR
33 6re 10010 . . . . . . . . . . . . . . . . . 18  |-  6  e.  RR
34 6nn 10071 . . . . . . . . . . . . . . . . . . 19  |-  6  e.  NN
3534nnne0i 9968 . . . . . . . . . . . . . . . . . 18  |-  6  =/=  0
3632, 33, 35redivcli 9715 . . . . . . . . . . . . . . . . 17  |-  ( ( pi ^ 2 )  /  6 )  e.  RR
3736a1i 11 . . . . . . . . . . . . . . . 16  |-  (  T. 
->  ( ( pi ^
2 )  /  6
)  e.  RR )
3837snssd 3888 . . . . . . . . . . . . . . 15  |-  (  T. 
->  { ( ( pi
^ 2 )  / 
6 ) }  C_  RR )
39 fss 5541 . . . . . . . . . . . . . . 15  |-  ( ( ( NN  X.  {
( ( pi ^
2 )  /  6
) } ) : NN --> { ( ( pi ^ 2 )  /  6 ) }  /\  { ( ( pi ^ 2 )  /  6 ) } 
C_  RR )  -> 
( NN  X.  {
( ( pi ^
2 )  /  6
) } ) : NN --> RR )
4030, 38, 39sylancr 645 . . . . . . . . . . . . . 14  |-  (  T. 
->  ( NN  X.  {
( ( pi ^
2 )  /  6
) } ) : NN --> RR )
41 resubcl 9299 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( x  -  y
)  e.  RR )
4241adantl 453 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  ( x  e.  RR  /\  y  e.  RR ) )  -> 
( x  -  y
)  e.  RR )
43 1ex 9021 . . . . . . . . . . . . . . . . 17  |-  1  e.  _V
4443fconst 5571 . . . . . . . . . . . . . . . 16  |-  ( NN 
X.  { 1 } ) : NN --> { 1 }
45 1re 9025 . . . . . . . . . . . . . . . . . 18  |-  1  e.  RR
4645a1i 11 . . . . . . . . . . . . . . . . 17  |-  (  T. 
->  1  e.  RR )
4746snssd 3888 . . . . . . . . . . . . . . . 16  |-  (  T. 
->  { 1 }  C_  RR )
48 fss 5541 . . . . . . . . . . . . . . . 16  |-  ( ( ( NN  X.  {
1 } ) : NN --> { 1 }  /\  { 1 } 
C_  RR )  -> 
( NN  X.  {
1 } ) : NN --> RR )
4944, 47, 48sylancr 645 . . . . . . . . . . . . . . 15  |-  (  T. 
->  ( NN  X.  {
1 } ) : NN --> RR )
50 2nn 10067 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  NN
5150a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  (  T. 
->  2  e.  NN )
52 nnmulcl 9957 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 2  e.  NN  /\  n  e.  NN )  ->  ( 2  x.  n
)  e.  NN )
5351, 52sylan 458 . . . . . . . . . . . . . . . . . 18  |-  ( (  T.  /\  n  e.  NN )  ->  (
2  x.  n )  e.  NN )
5453peano2nnd 9951 . . . . . . . . . . . . . . . . 17  |-  ( (  T.  /\  n  e.  NN )  ->  (
( 2  x.  n
)  +  1 )  e.  NN )
5554nnrecred 9979 . . . . . . . . . . . . . . . 16  |-  ( (  T.  /\  n  e.  NN )  ->  (
1  /  ( ( 2  x.  n )  +  1 ) )  e.  RR )
56 basel.g . . . . . . . . . . . . . . . 16  |-  G  =  ( n  e.  NN  |->  ( 1  /  (
( 2  x.  n
)  +  1 ) ) )
5755, 56fmptd 5834 . . . . . . . . . . . . . . 15  |-  (  T. 
->  G : NN --> RR )
58 nnex 9940 . . . . . . . . . . . . . . . 16  |-  NN  e.  _V
5958a1i 11 . . . . . . . . . . . . . . 15  |-  (  T. 
->  NN  e.  _V )
60 inidm 3495 . . . . . . . . . . . . . . 15  |-  ( NN 
i^i  NN )  =  NN
6142, 49, 57, 59, 59, 60off 6261 . . . . . . . . . . . . . 14  |-  (  T. 
->  ( ( NN  X.  { 1 } )  o F  -  G
) : NN --> RR )
6228, 40, 61, 59, 59, 60off 6261 . . . . . . . . . . . . 13  |-  (  T. 
->  ( ( NN  X.  { ( ( pi
^ 2 )  / 
6 ) } )  o F  x.  (
( NN  X.  {
1 } )  o F  -  G ) ) : NN --> RR )
63 basel.h . . . . . . . . . . . . . 14  |-  H  =  ( ( NN  X.  { ( ( pi
^ 2 )  / 
6 ) } )  o F  x.  (
( NN  X.  {
1 } )  o F  -  G ) )
6463feq1i 5527 . . . . . . . . . . . . 13  |-  ( H : NN --> RR  <->  ( ( NN  X.  { ( ( pi ^ 2 )  /  6 ) } )  o F  x.  ( ( NN  X.  { 1 } )  o F  -  G
) ) : NN --> RR )
6562, 64sylibr 204 . . . . . . . . . . . 12  |-  (  T. 
->  H : NN --> RR )
66 readdcl 9008 . . . . . . . . . . . . . 14  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( x  +  y )  e.  RR )
6766adantl 453 . . . . . . . . . . . . 13  |-  ( (  T.  /\  ( x  e.  RR  /\  y  e.  RR ) )  -> 
( x  +  y )  e.  RR )
6813elexi 2910 . . . . . . . . . . . . . . . 16  |-  -u 2  e.  _V
6968fconst 5571 . . . . . . . . . . . . . . 15  |-  ( NN 
X.  { -u 2 } ) : NN --> { -u 2 }
7013zrei 10222 . . . . . . . . . . . . . . . . 17  |-  -u 2  e.  RR
7170a1i 11 . . . . . . . . . . . . . . . 16  |-  (  T. 
->  -u 2  e.  RR )
7271snssd 3888 . . . . . . . . . . . . . . 15  |-  (  T. 
->  { -u 2 } 
C_  RR )
73 fss 5541 . . . . . . . . . . . . . . 15  |-  ( ( ( NN  X.  { -u 2 } ) : NN --> { -u 2 }  /\  { -u 2 }  C_  RR )  -> 
( NN  X.  { -u 2 } ) : NN --> RR )
7469, 72, 73sylancr 645 . . . . . . . . . . . . . 14  |-  (  T. 
->  ( NN  X.  { -u 2 } ) : NN --> RR )
7528, 74, 57, 59, 59, 60off 6261 . . . . . . . . . . . . 13  |-  (  T. 
->  ( ( NN  X.  { -u 2 } )  o F  x.  G
) : NN --> RR )
7667, 49, 75, 59, 59, 60off 6261 . . . . . . . . . . . 12  |-  (  T. 
->  ( ( NN  X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G ) ) : NN --> RR )
7728, 65, 76, 59, 59, 60off 6261 . . . . . . . . . . 11  |-  (  T. 
->  ( H  o F  x.  ( ( NN 
X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G
) ) ) : NN --> RR )
78 basel.j . . . . . . . . . . . 12  |-  J  =  ( H  o F  x.  ( ( NN 
X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G
) ) )
7978feq1i 5527 . . . . . . . . . . 11  |-  ( J : NN --> RR  <->  ( H  o F  x.  (
( NN  X.  {
1 } )  o F  +  ( ( NN  X.  { -u
2 } )  o F  x.  G ) ) ) : NN --> RR )
8077, 79sylibr 204 . . . . . . . . . 10  |-  (  T. 
->  J : NN --> RR )
8180ffvelrnda 5811 . . . . . . . . 9  |-  ( (  T.  /\  n  e.  NN )  ->  ( J `  n )  e.  RR )
8281recnd 9049 . . . . . . . 8  |-  ( (  T.  /\  n  e.  NN )  ->  ( J `  n )  e.  CC )
8326, 82npcand 9349 . . . . . . 7  |-  ( (  T.  /\  n  e.  NN )  ->  (
( ( F `  n )  -  ( J `  n )
)  +  ( J `
 n ) )  =  ( F `  n ) )
8483mpteq2dva 4238 . . . . . 6  |-  (  T. 
->  ( n  e.  NN  |->  ( ( ( F `
 n )  -  ( J `  n ) )  +  ( J `
 n ) ) )  =  ( n  e.  NN  |->  ( F `
 n ) ) )
85 ovex 6047 . . . . . . . 8  |-  ( ( F `  n )  -  ( J `  n ) )  e. 
_V
8685a1i 11 . . . . . . 7  |-  ( (  T.  /\  n  e.  NN )  ->  (
( F `  n
)  -  ( J `
 n ) )  e.  _V )
8724feqmptd 5720 . . . . . . . 8  |-  (  T. 
->  F  =  (
n  e.  NN  |->  ( F `  n ) ) )
8880feqmptd 5720 . . . . . . . 8  |-  (  T. 
->  J  =  (
n  e.  NN  |->  ( J `  n ) ) )
8959, 25, 81, 87, 88offval2 6263 . . . . . . 7  |-  (  T. 
->  ( F  o F  -  J )  =  ( n  e.  NN  |->  ( ( F `  n )  -  ( J `  n )
) ) )
9059, 86, 81, 89, 88offval2 6263 . . . . . 6  |-  (  T. 
->  ( ( F  o F  -  J )  o F  +  J
)  =  ( n  e.  NN  |->  ( ( ( F `  n
)  -  ( J `
 n ) )  +  ( J `  n ) ) ) )
9184, 90, 873eqtr4d 2431 . . . . 5  |-  (  T. 
->  ( ( F  o F  -  J )  o F  +  J
)  =  F )
9267, 49, 57, 59, 59, 60off 6261 . . . . . . . . . 10  |-  (  T. 
->  ( ( NN  X.  { 1 } )  o F  +  G
) : NN --> RR )
93 recn 9015 . . . . . . . . . . . 12  |-  ( x  e.  RR  ->  x  e.  CC )
94 recn 9015 . . . . . . . . . . . 12  |-  ( y  e.  RR  ->  y  e.  CC )
95 recn 9015 . . . . . . . . . . . 12  |-  ( z  e.  RR  ->  z  e.  CC )
96 subdi 9401 . . . . . . . . . . . 12  |-  ( ( x  e.  CC  /\  y  e.  CC  /\  z  e.  CC )  ->  (
x  x.  ( y  -  z ) )  =  ( ( x  x.  y )  -  ( x  x.  z
) ) )
9793, 94, 95, 96syl3an 1226 . . . . . . . . . . 11  |-  ( ( x  e.  RR  /\  y  e.  RR  /\  z  e.  RR )  ->  (
x  x.  ( y  -  z ) )  =  ( ( x  x.  y )  -  ( x  x.  z
) ) )
9897adantl 453 . . . . . . . . . 10  |-  ( (  T.  /\  ( x  e.  RR  /\  y  e.  RR  /\  z  e.  RR ) )  -> 
( x  x.  (
y  -  z ) )  =  ( ( x  x.  y )  -  ( x  x.  z ) ) )
9959, 65, 92, 76, 98caofdi 6281 . . . . . . . . 9  |-  (  T. 
->  ( H  o F  x.  ( ( ( NN  X.  { 1 } )  o F  +  G )  o F  -  ( ( NN  X.  { 1 } )  o F  +  ( ( NN 
X.  { -u 2 } )  o F  x.  G ) ) ) )  =  ( ( H  o F  x.  ( ( NN 
X.  { 1 } )  o F  +  G ) )  o F  -  ( H  o F  x.  (
( NN  X.  {
1 } )  o F  +  ( ( NN  X.  { -u
2 } )  o F  x.  G ) ) ) ) )
100 basel.k . . . . . . . . . 10  |-  K  =  ( H  o F  x.  ( ( NN 
X.  { 1 } )  o F  +  G ) )
101100, 78oveq12i 6034 . . . . . . . . 9  |-  ( K  o F  -  J
)  =  ( ( H  o F  x.  ( ( NN  X.  { 1 } )  o F  +  G
) )  o F  -  ( H  o F  x.  ( ( NN  X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G
) ) ) )
10299, 101syl6eqr 2439 . . . . . . . 8  |-  (  T. 
->  ( H  o F  x.  ( ( ( NN  X.  { 1 } )  o F  +  G )  o F  -  ( ( NN  X.  { 1 } )  o F  +  ( ( NN 
X.  { -u 2 } )  o F  x.  G ) ) ) )  =  ( K  o F  -  J ) )
10336recni 9037 . . . . . . . . . . . . . 14  |-  ( ( pi ^ 2 )  /  6 )  e.  CC
1041eqimss2i 3348 . . . . . . . . . . . . . . 15  |-  ( ZZ>= ` 
1 )  C_  NN
105104, 58climconst2 12271 . . . . . . . . . . . . . 14  |-  ( ( ( ( pi ^
2 )  /  6
)  e.  CC  /\  1  e.  ZZ )  ->  ( NN  X.  {
( ( pi ^
2 )  /  6
) } )  ~~>  ( ( pi ^ 2 )  /  6 ) )
106103, 3, 105sylancr 645 . . . . . . . . . . . . 13  |-  (  T. 
->  ( NN  X.  {
( ( pi ^
2 )  /  6
) } )  ~~>  ( ( pi ^ 2 )  /  6 ) )
107 ovex 6047 . . . . . . . . . . . . . 14  |-  ( ( NN  X.  { ( ( pi ^ 2 )  /  6 ) } )  o F  x.  ( ( NN 
X.  { 1 } )  o F  -  G ) )  e. 
_V
108107a1i 11 . . . . . . . . . . . . 13  |-  (  T. 
->  ( ( NN  X.  { ( ( pi
^ 2 )  / 
6 ) } )  o F  x.  (
( NN  X.  {
1 } )  o F  -  G ) )  e.  _V )
109 ax-resscn 8982 . . . . . . . . . . . . . . . 16  |-  RR  C_  CC
110 fss 5541 . . . . . . . . . . . . . . . 16  |-  ( ( ( NN  X.  {
1 } ) : NN --> RR  /\  RR  C_  CC )  ->  ( NN  X.  { 1 } ) : NN --> CC )
11149, 109, 110sylancl 644 . . . . . . . . . . . . . . 15  |-  (  T. 
->  ( NN  X.  {
1 } ) : NN --> CC )
112 fss 5541 . . . . . . . . . . . . . . . 16  |-  ( ( G : NN --> RR  /\  RR  C_  CC )  ->  G : NN --> CC )
11357, 109, 112sylancl 644 . . . . . . . . . . . . . . 15  |-  (  T. 
->  G : NN --> CC )
114 ofnegsub 9932 . . . . . . . . . . . . . . 15  |-  ( ( NN  e.  _V  /\  ( NN  X.  { 1 } ) : NN --> CC  /\  G : NN --> CC )  ->  ( ( NN  X.  { 1 } )  o F  +  ( ( NN 
X.  { -u 1 } )  o F  x.  G ) )  =  ( ( NN 
X.  { 1 } )  o F  -  G ) )
11559, 111, 113, 114syl3anc 1184 . . . . . . . . . . . . . 14  |-  (  T. 
->  ( ( NN  X.  { 1 } )  o F  +  ( ( NN  X.  { -u 1 } )  o F  x.  G ) )  =  ( ( NN  X.  { 1 } )  o F  -  G ) )
116 neg1cn 10001 . . . . . . . . . . . . . . 15  |-  -u 1  e.  CC
11756, 116basellem7 20738 . . . . . . . . . . . . . 14  |-  ( ( NN  X.  { 1 } )  o F  +  ( ( NN 
X.  { -u 1 } )  o F  x.  G ) )  ~~>  1
118115, 117syl6eqbrr 4193 . . . . . . . . . . . . 13  |-  (  T. 
->  ( ( NN  X.  { 1 } )  o F  -  G
)  ~~>  1 )
11940ffvelrnda 5811 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
( NN  X.  {
( ( pi ^
2 )  /  6
) } ) `  k )  e.  RR )
120119recnd 9049 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( NN  X.  {
( ( pi ^
2 )  /  6
) } ) `  k )  e.  CC )
12161ffvelrnda 5811 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 1 } )  o F  -  G
) `  k )  e.  RR )
122121recnd 9049 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 1 } )  o F  -  G
) `  k )  e.  CC )
123 ffn 5533 . . . . . . . . . . . . . . 15  |-  ( ( NN  X.  { ( ( pi ^ 2 )  /  6 ) } ) : NN --> RR  ->  ( NN  X.  { ( ( pi
^ 2 )  / 
6 ) } )  Fn  NN )
12440, 123syl 16 . . . . . . . . . . . . . 14  |-  (  T. 
->  ( NN  X.  {
( ( pi ^
2 )  /  6
) } )  Fn  NN )
125 fnconstg 5573 . . . . . . . . . . . . . . . 16  |-  ( 1  e.  ZZ  ->  ( NN  X.  { 1 } )  Fn  NN )
1263, 125syl 16 . . . . . . . . . . . . . . 15  |-  (  T. 
->  ( NN  X.  {
1 } )  Fn  NN )
127 ffn 5533 . . . . . . . . . . . . . . . 16  |-  ( G : NN --> RR  ->  G  Fn  NN )
12857, 127syl 16 . . . . . . . . . . . . . . 15  |-  (  T. 
->  G  Fn  NN )
129126, 128, 59, 59, 60offn 6257 . . . . . . . . . . . . . 14  |-  (  T. 
->  ( ( NN  X.  { 1 } )  o F  -  G
)  Fn  NN )
130 eqidd 2390 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
( NN  X.  {
( ( pi ^
2 )  /  6
) } ) `  k )  =  ( ( NN  X.  {
( ( pi ^
2 )  /  6
) } ) `  k ) )
131 eqidd 2390 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 1 } )  o F  -  G
) `  k )  =  ( ( ( NN  X.  { 1 } )  o F  -  G ) `  k ) )
132124, 129, 59, 59, 60, 130, 131ofval 6255 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { ( ( pi
^ 2 )  / 
6 ) } )  o F  x.  (
( NN  X.  {
1 } )  o F  -  G ) ) `  k )  =  ( ( ( NN  X.  { ( ( pi ^ 2 )  /  6 ) } ) `  k
)  x.  ( ( ( NN  X.  {
1 } )  o F  -  G ) `
 k ) ) )
1331, 3, 106, 108, 118, 120, 122, 132climmul 12355 . . . . . . . . . . . 12  |-  (  T. 
->  ( ( NN  X.  { ( ( pi
^ 2 )  / 
6 ) } )  o F  x.  (
( NN  X.  {
1 } )  o F  -  G ) )  ~~>  ( ( ( pi ^ 2 )  /  6 )  x.  1 ) )
134103mulid1i 9027 . . . . . . . . . . . 12  |-  ( ( ( pi ^ 2 )  /  6 )  x.  1 )  =  ( ( pi ^
2 )  /  6
)
135133, 134syl6breq 4194 . . . . . . . . . . 11  |-  (  T. 
->  ( ( NN  X.  { ( ( pi
^ 2 )  / 
6 ) } )  o F  x.  (
( NN  X.  {
1 } )  o F  -  G ) )  ~~>  ( ( pi
^ 2 )  / 
6 ) )
13663, 135syl5eqbr 4188 . . . . . . . . . 10  |-  (  T. 
->  H  ~~>  ( (
pi ^ 2 )  /  6 ) )
137 ovex 6047 . . . . . . . . . . 11  |-  ( H  o F  x.  (
( ( NN  X.  { 1 } )  o F  +  G
)  o F  -  ( ( NN  X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G ) ) ) )  e. 
_V
138137a1i 11 . . . . . . . . . 10  |-  (  T. 
->  ( H  o F  x.  ( ( ( NN  X.  { 1 } )  o F  +  G )  o F  -  ( ( NN  X.  { 1 } )  o F  +  ( ( NN 
X.  { -u 2 } )  o F  x.  G ) ) ) )  e.  _V )
139 3cn 10006 . . . . . . . . . . . . 13  |-  3  e.  CC
140104, 58climconst2 12271 . . . . . . . . . . . . 13  |-  ( ( 3  e.  CC  /\  1  e.  ZZ )  ->  ( NN  X.  {
3 } )  ~~>  3 )
141139, 3, 140sylancr 645 . . . . . . . . . . . 12  |-  (  T. 
->  ( NN  X.  {
3 } )  ~~>  3 )
142 ovex 6047 . . . . . . . . . . . . 13  |-  ( ( NN  X.  { 3 } )  o F  x.  G )  e. 
_V
143142a1i 11 . . . . . . . . . . . 12  |-  (  T. 
->  ( ( NN  X.  { 3 } )  o F  x.  G
)  e.  _V )
14456basellem6 20737 . . . . . . . . . . . . 13  |-  G  ~~>  0
145144a1i 11 . . . . . . . . . . . 12  |-  (  T. 
->  G  ~~>  0 )
146 3re 10005 . . . . . . . . . . . . . . . . 17  |-  3  e.  RR
147146elexi 2910 . . . . . . . . . . . . . . . 16  |-  3  e.  _V
148147fconst 5571 . . . . . . . . . . . . . . 15  |-  ( NN 
X.  { 3 } ) : NN --> { 3 }
149146a1i 11 . . . . . . . . . . . . . . . 16  |-  (  T. 
->  3  e.  RR )
150149snssd 3888 . . . . . . . . . . . . . . 15  |-  (  T. 
->  { 3 }  C_  RR )
151 fss 5541 . . . . . . . . . . . . . . 15  |-  ( ( ( NN  X.  {
3 } ) : NN --> { 3 }  /\  { 3 } 
C_  RR )  -> 
( NN  X.  {
3 } ) : NN --> RR )
152148, 150, 151sylancr 645 . . . . . . . . . . . . . 14  |-  (  T. 
->  ( NN  X.  {
3 } ) : NN --> RR )
153152ffvelrnda 5811 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( NN  X.  {
3 } ) `  k )  e.  RR )
154153recnd 9049 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  (
( NN  X.  {
3 } ) `  k )  e.  CC )
15557ffvelrnda 5811 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  ( G `  k )  e.  RR )
156155recnd 9049 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  ( G `  k )  e.  CC )
157 ffn 5533 . . . . . . . . . . . . . 14  |-  ( ( NN  X.  { 3 } ) : NN --> RR  ->  ( NN  X.  { 3 } )  Fn  NN )
158152, 157syl 16 . . . . . . . . . . . . 13  |-  (  T. 
->  ( NN  X.  {
3 } )  Fn  NN )
159 eqidd 2390 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( NN  X.  {
3 } ) `  k )  =  ( ( NN  X.  {
3 } ) `  k ) )
160 eqidd 2390 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  ( G `  k )  =  ( G `  k ) )
161158, 128, 59, 59, 60, 159, 160ofval 6255 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 3 } )  o F  x.  G
) `  k )  =  ( ( ( NN  X.  { 3 } ) `  k
)  x.  ( G `
 k ) ) )
1621, 3, 141, 143, 145, 154, 156, 161climmul 12355 . . . . . . . . . . 11  |-  (  T. 
->  ( ( NN  X.  { 3 } )  o F  x.  G
)  ~~>  ( 3  x.  0 ) )
163139mul01i 9190 . . . . . . . . . . 11  |-  ( 3  x.  0 )  =  0
164162, 163syl6breq 4194 . . . . . . . . . 10  |-  (  T. 
->  ( ( NN  X.  { 3 } )  o F  x.  G
)  ~~>  0 )
16565ffvelrnda 5811 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  ( H `  k )  e.  RR )
166165recnd 9049 . . . . . . . . . 10  |-  ( (  T.  /\  k  e.  NN )  ->  ( H `  k )  e.  CC )
16728, 152, 57, 59, 59, 60off 6261 . . . . . . . . . . . 12  |-  (  T. 
->  ( ( NN  X.  { 3 } )  o F  x.  G
) : NN --> RR )
168167ffvelrnda 5811 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 3 } )  o F  x.  G
) `  k )  e.  RR )
169168recnd 9049 . . . . . . . . . 10  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 3 } )  o F  x.  G
) `  k )  e.  CC )
170 ffn 5533 . . . . . . . . . . . 12  |-  ( H : NN --> RR  ->  H  Fn  NN )
17165, 170syl 16 . . . . . . . . . . 11  |-  (  T. 
->  H  Fn  NN )
17242, 92, 76, 59, 59, 60off 6261 . . . . . . . . . . . 12  |-  (  T. 
->  ( ( ( NN 
X.  { 1 } )  o F  +  G )  o F  -  ( ( NN 
X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G
) ) ) : NN --> RR )
173 ffn 5533 . . . . . . . . . . . 12  |-  ( ( ( ( NN  X.  { 1 } )  o F  +  G
)  o F  -  ( ( NN  X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G ) ) ) : NN --> RR  ->  ( ( ( NN  X.  { 1 } )  o F  +  G )  o F  -  ( ( NN  X.  { 1 } )  o F  +  ( ( NN 
X.  { -u 2 } )  o F  x.  G ) ) )  Fn  NN )
174172, 173syl 16 . . . . . . . . . . 11  |-  (  T. 
->  ( ( ( NN 
X.  { 1 } )  o F  +  G )  o F  -  ( ( NN 
X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G
) ) )  Fn  NN )
175 eqidd 2390 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  ( H `  k )  =  ( H `  k ) )
176156mulid2d 9041 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  k  e.  NN )  ->  (
1  x.  ( G `
 k ) )  =  ( G `  k ) )
177 2cn 10004 . . . . . . . . . . . . . . . . . 18  |-  2  e.  CC
178 mulneg1 9404 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  e.  CC  /\  ( G `  k )  e.  CC )  -> 
( -u 2  x.  ( G `  k )
)  =  -u (
2  x.  ( G `
 k ) ) )
179177, 156, 178sylancr 645 . . . . . . . . . . . . . . . . 17  |-  ( (  T.  /\  k  e.  NN )  ->  ( -u 2  x.  ( G `
 k ) )  =  -u ( 2  x.  ( G `  k
) ) )
180179negeqd 9234 . . . . . . . . . . . . . . . 16  |-  ( (  T.  /\  k  e.  NN )  ->  -u ( -u 2  x.  ( G `
 k ) )  =  -u -u ( 2  x.  ( G `  k
) ) )
181 mulcl 9009 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  e.  CC  /\  ( G `  k )  e.  CC )  -> 
( 2  x.  ( G `  k )
)  e.  CC )
182177, 156, 181sylancr 645 . . . . . . . . . . . . . . . . 17  |-  ( (  T.  /\  k  e.  NN )  ->  (
2  x.  ( G `
 k ) )  e.  CC )
183182negnegd 9336 . . . . . . . . . . . . . . . 16  |-  ( (  T.  /\  k  e.  NN )  ->  -u -u (
2  x.  ( G `
 k ) )  =  ( 2  x.  ( G `  k
) ) )
184180, 183eqtr2d 2422 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  k  e.  NN )  ->  (
2  x.  ( G `
 k ) )  =  -u ( -u 2  x.  ( G `  k
) ) )
185176, 184oveq12d 6040 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 1  x.  ( G `  k )
)  +  ( 2  x.  ( G `  k ) ) )  =  ( ( G `
 k )  + 
-u ( -u 2  x.  ( G `  k
) ) ) )
186 remulcl 9010 . . . . . . . . . . . . . . . . 17  |-  ( (
-u 2  e.  RR  /\  ( G `  k
)  e.  RR )  ->  ( -u 2  x.  ( G `  k
) )  e.  RR )
18770, 155, 186sylancr 645 . . . . . . . . . . . . . . . 16  |-  ( (  T.  /\  k  e.  NN )  ->  ( -u 2  x.  ( G `
 k ) )  e.  RR )
188187recnd 9049 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  k  e.  NN )  ->  ( -u 2  x.  ( G `
 k ) )  e.  CC )
189156, 188negsubd 9351 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
( G `  k
)  +  -u ( -u 2  x.  ( G `
 k ) ) )  =  ( ( G `  k )  -  ( -u 2  x.  ( G `  k
) ) ) )
190185, 189eqtrd 2421 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 1  x.  ( G `  k )
)  +  ( 2  x.  ( G `  k ) ) )  =  ( ( G `
 k )  -  ( -u 2  x.  ( G `  k )
) ) )
191 df-3 9993 . . . . . . . . . . . . . . . 16  |-  3  =  ( 2  +  1 )
192 ax-1cn 8983 . . . . . . . . . . . . . . . . 17  |-  1  e.  CC
193177, 192addcomi 9191 . . . . . . . . . . . . . . . 16  |-  ( 2  +  1 )  =  ( 1  +  2 )
194191, 193eqtri 2409 . . . . . . . . . . . . . . 15  |-  3  =  ( 1  +  2 )
195194oveq1i 6032 . . . . . . . . . . . . . 14  |-  ( 3  x.  ( G `  k ) )  =  ( ( 1  +  2 )  x.  ( G `  k )
)
196192a1i 11 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  k  e.  NN )  ->  1  e.  CC )
197177a1i 11 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  k  e.  NN )  ->  2  e.  CC )
198196, 197, 156adddird 9048 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 1  +  2 )  x.  ( G `
 k ) )  =  ( ( 1  x.  ( G `  k ) )  +  ( 2  x.  ( G `  k )
) ) )
199195, 198syl5eq 2433 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
3  x.  ( G `
 k ) )  =  ( ( 1  x.  ( G `  k ) )  +  ( 2  x.  ( G `  k )
) ) )
200196, 156, 188pnpcand 9382 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 1  +  ( G `  k ) )  -  ( 1  +  ( -u 2  x.  ( G `  k
) ) ) )  =  ( ( G `
 k )  -  ( -u 2  x.  ( G `  k )
) ) )
201190, 199, 2003eqtr4rd 2432 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 1  +  ( G `  k ) )  -  ( 1  +  ( -u 2  x.  ( G `  k
) ) ) )  =  ( 3  x.  ( G `  k
) ) )
202126, 128, 59, 59, 60offn 6257 . . . . . . . . . . . . 13  |-  (  T. 
->  ( ( NN  X.  { 1 } )  o F  +  G
)  Fn  NN )
20313a1i 11 . . . . . . . . . . . . . . . 16  |-  (  T. 
->  -u 2  e.  ZZ )
204 fnconstg 5573 . . . . . . . . . . . . . . . 16  |-  ( -u
2  e.  ZZ  ->  ( NN  X.  { -u
2 } )  Fn  NN )
205203, 204syl 16 . . . . . . . . . . . . . . 15  |-  (  T. 
->  ( NN  X.  { -u 2 } )  Fn  NN )
206205, 128, 59, 59, 60offn 6257 . . . . . . . . . . . . . 14  |-  (  T. 
->  ( ( NN  X.  { -u 2 } )  o F  x.  G
)  Fn  NN )
207126, 206, 59, 59, 60offn 6257 . . . . . . . . . . . . 13  |-  (  T. 
->  ( ( NN  X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G ) )  Fn  NN )
20859, 46, 128, 160ofc1 6268 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 1 } )  o F  +  G
) `  k )  =  ( 1  +  ( G `  k
) ) )
20959, 71, 128, 160ofc1 6268 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { -u 2 } )  o F  x.  G
) `  k )  =  ( -u 2  x.  ( G `  k
) ) )
21059, 46, 206, 209ofc1 6268 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G ) ) `  k )  =  ( 1  +  ( -u 2  x.  ( G `  k
) ) ) )
211202, 207, 59, 59, 60, 208, 210ofval 6255 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( ( NN 
X.  { 1 } )  o F  +  G )  o F  -  ( ( NN 
X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G
) ) ) `  k )  =  ( ( 1  +  ( G `  k ) )  -  ( 1  +  ( -u 2  x.  ( G `  k
) ) ) ) )
21259, 149, 128, 160ofc1 6268 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 3 } )  o F  x.  G
) `  k )  =  ( 3  x.  ( G `  k
) ) )
213201, 211, 2123eqtr4d 2431 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( ( NN 
X.  { 1 } )  o F  +  G )  o F  -  ( ( NN 
X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G
) ) ) `  k )  =  ( ( ( NN  X.  { 3 } )  o F  x.  G
) `  k )
)
214171, 174, 59, 59, 60, 175, 213ofval 6255 . . . . . . . . . 10  |-  ( (  T.  /\  k  e.  NN )  ->  (
( H  o F  x.  ( ( ( NN  X.  { 1 } )  o F  +  G )  o F  -  ( ( NN  X.  { 1 } )  o F  +  ( ( NN 
X.  { -u 2 } )  o F  x.  G ) ) ) ) `  k
)  =  ( ( H `  k )  x.  ( ( ( NN  X.  { 3 } )  o F  x.  G ) `  k ) ) )
2151, 3, 136, 138, 164, 166, 169, 214climmul 12355 . . . . . . . . 9  |-  (  T. 
->  ( H  o F  x.  ( ( ( NN  X.  { 1 } )  o F  +  G )  o F  -  ( ( NN  X.  { 1 } )  o F  +  ( ( NN 
X.  { -u 2 } )  o F  x.  G ) ) ) )  ~~>  ( ( ( pi ^ 2 )  /  6 )  x.  0 ) )
216103mul01i 9190 . . . . . . . . 9  |-  ( ( ( pi ^ 2 )  /  6 )  x.  0 )  =  0
217215, 216syl6breq 4194 . . . . . . . 8  |-  (  T. 
->  ( H  o F  x.  ( ( ( NN  X.  { 1 } )  o F  +  G )  o F  -  ( ( NN  X.  { 1 } )  o F  +  ( ( NN 
X.  { -u 2 } )  o F  x.  G ) ) ) )  ~~>  0 )
218102, 217eqbrtrrd 4177 . . . . . . 7  |-  (  T. 
->  ( K  o F  -  J )  ~~>  0 )
219 ovex 6047 . . . . . . . 8  |-  ( F  o F  -  J
)  e.  _V
220219a1i 11 . . . . . . 7  |-  (  T. 
->  ( F  o F  -  J )  e. 
_V )
22128, 65, 92, 59, 59, 60off 6261 . . . . . . . . . 10  |-  (  T. 
->  ( H  o F  x.  ( ( NN 
X.  { 1 } )  o F  +  G ) ) : NN --> RR )
222100feq1i 5527 . . . . . . . . . 10  |-  ( K : NN --> RR  <->  ( H  o F  x.  (
( NN  X.  {
1 } )  o F  +  G ) ) : NN --> RR )
223221, 222sylibr 204 . . . . . . . . 9  |-  (  T. 
->  K : NN --> RR )
22442, 223, 80, 59, 59, 60off 6261 . . . . . . . 8  |-  (  T. 
->  ( K  o F  -  J ) : NN --> RR )
225224ffvelrnda 5811 . . . . . . 7  |-  ( (  T.  /\  k  e.  NN )  ->  (
( K  o F  -  J ) `  k )  e.  RR )
22642, 24, 80, 59, 59, 60off 6261 . . . . . . . 8  |-  (  T. 
->  ( F  o F  -  J ) : NN --> RR )
227226ffvelrnda 5811 . . . . . . 7  |-  ( (  T.  /\  k  e.  NN )  ->  (
( F  o F  -  J ) `  k )  e.  RR )
22824ffvelrnda 5811 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  ( F `  k )  e.  RR )
229223ffvelrnda 5811 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  ( K `  k )  e.  RR )
23080ffvelrnda 5811 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  ( J `  k )  e.  RR )
231 eqid 2389 . . . . . . . . . . . 12  |-  ( ( 2  x.  k )  +  1 )  =  ( ( 2  x.  k )  +  1 )
23256, 22, 63, 78, 100, 231basellem8 20739 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  (
( J `  k
)  <_  ( F `  k )  /\  ( F `  k )  <_  ( K `  k
) ) )
233232adantl 453 . . . . . . . . . 10  |-  ( (  T.  /\  k  e.  NN )  ->  (
( J `  k
)  <_  ( F `  k )  /\  ( F `  k )  <_  ( K `  k
) ) )
234233simprd 450 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  ( F `  k )  <_  ( K `  k
) )
235228, 229, 230, 234lesub1dd 9576 . . . . . . . 8  |-  ( (  T.  /\  k  e.  NN )  ->  (
( F `  k
)  -  ( J `
 k ) )  <_  ( ( K `
 k )  -  ( J `  k ) ) )
236 ffn 5533 . . . . . . . . . 10  |-  ( F : NN --> RR  ->  F  Fn  NN )
23724, 236syl 16 . . . . . . . . 9  |-  (  T. 
->  F  Fn  NN )
238 ffn 5533 . . . . . . . . . 10  |-  ( J : NN --> RR  ->  J  Fn  NN )
23980, 238syl 16 . . . . . . . . 9  |-  (  T. 
->  J  Fn  NN )
240 eqidd 2390 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  ( F `  k )  =  ( F `  k ) )
241 eqidd 2390 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  ( J `  k )  =  ( J `  k ) )
242237, 239, 59, 59, 60, 240, 241ofval 6255 . . . . . . . 8  |-  ( (  T.  /\  k  e.  NN )  ->  (
( F  o F  -  J ) `  k )  =  ( ( F `  k
)  -  ( J `
 k ) ) )
243 ffn 5533 . . . . . . . . . 10  |-  ( K : NN --> RR  ->  K  Fn  NN )
244223, 243syl 16 . . . . . . . . 9  |-  (  T. 
->  K  Fn  NN )
245 eqidd 2390 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  ( K `  k )  =  ( K `  k ) )
246244, 239, 59, 59, 60, 245, 241ofval 6255 . . . . . . . 8  |-  ( (  T.  /\  k  e.  NN )  ->  (
( K  o F  -  J ) `  k )  =  ( ( K `  k
)  -  ( J `
 k ) ) )
247235, 242, 2463brtr4d 4185 . . . . . . 7  |-  ( (  T.  /\  k  e.  NN )  ->  (
( F  o F  -  J ) `  k )  <_  (
( K  o F  -  J ) `  k ) )
248233simpld 446 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  ( J `  k )  <_  ( F `  k
) )
249228, 230subge0d 9550 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  (
0  <_  ( ( F `  k )  -  ( J `  k ) )  <->  ( J `  k )  <_  ( F `  k )
) )
250248, 249mpbird 224 . . . . . . . 8  |-  ( (  T.  /\  k  e.  NN )  ->  0  <_  ( ( F `  k )  -  ( J `  k )
) )
251250, 242breqtrrd 4181 . . . . . . 7  |-  ( (  T.  /\  k  e.  NN )  ->  0  <_  ( ( F  o F  -  J ) `  k ) )
2521, 3, 218, 220, 225, 227, 247, 251climsqz2 12364 . . . . . 6  |-  (  T. 
->  ( F  o F  -  J )  ~~>  0 )
253 ovex 6047 . . . . . . 7  |-  ( ( F  o F  -  J )  o F  +  J )  e. 
_V
254253a1i 11 . . . . . 6  |-  (  T. 
->  ( ( F  o F  -  J )  o F  +  J
)  e.  _V )
255 ovex 6047 . . . . . . . . . 10  |-  ( H  o F  x.  (
( NN  X.  {
1 } )  o F  +  ( ( NN  X.  { -u
2 } )  o F  x.  G ) ) )  e.  _V
256255a1i 11 . . . . . . . . 9  |-  (  T. 
->  ( H  o F  x.  ( ( NN 
X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G
) ) )  e. 
_V )
25770recni 9037 . . . . . . . . . . 11  |-  -u 2  e.  CC
25856, 257basellem7 20738 . . . . . . . . . 10  |-  ( ( NN  X.  { 1 } )  o F  +  ( ( NN 
X.  { -u 2 } )  o F  x.  G ) )  ~~>  1
259258a1i 11 . . . . . . . . 9  |-  (  T. 
->  ( ( NN  X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G ) )  ~~>  1 )
26076ffvelrnda 5811 . . . . . . . . . 10  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G ) ) `  k )  e.  RR )
261260recnd 9049 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G ) ) `  k )  e.  CC )
262 eqidd 2390 . . . . . . . . . 10  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G ) ) `  k )  =  ( ( ( NN  X.  { 1 } )  o F  +  ( ( NN 
X.  { -u 2 } )  o F  x.  G ) ) `
 k ) )
263171, 207, 59, 59, 60, 175, 262ofval 6255 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  (
( H  o F  x.  ( ( NN 
X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G
) ) ) `  k )  =  ( ( H `  k
)  x.  ( ( ( NN  X.  {
1 } )  o F  +  ( ( NN  X.  { -u
2 } )  o F  x.  G ) ) `  k ) ) )
2641, 3, 136, 256, 259, 166, 261, 263climmul 12355 . . . . . . . 8  |-  (  T. 
->  ( H  o F  x.  ( ( NN 
X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G
) ) )  ~~>  ( ( ( pi ^ 2 )  /  6 )  x.  1 ) )
265264, 134syl6breq 4194 . . . . . . 7  |-  (  T. 
->  ( H  o F  x.  ( ( NN 
X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G
) ) )  ~~>  ( ( pi ^ 2 )  /  6 ) )
26678, 265syl5eqbr 4188 . . . . . 6  |-  (  T. 
->  J  ~~>  ( (
pi ^ 2 )  /  6 ) )
267227recnd 9049 . . . . . 6  |-  ( (  T.  /\  k  e.  NN )  ->  (
( F  o F  -  J ) `  k )  e.  CC )
268230recnd 9049 . . . . . 6  |-  ( (  T.  /\  k  e.  NN )  ->  ( J `  k )  e.  CC )
269 ffn 5533 . . . . . . . 8  |-  ( ( F  o F  -  J ) : NN --> RR  ->  ( F  o F  -  J )  Fn  NN )
270226, 269syl 16 . . . . . . 7  |-  (  T. 
->  ( F  o F  -  J )  Fn  NN )
271 eqidd 2390 . . . . . . 7  |-  ( (  T.  /\  k  e.  NN )  ->  (
( F  o F  -  J ) `  k )  =  ( ( F  o F  -  J ) `  k ) )
272270, 239, 59, 59, 60, 271, 241ofval 6255 . . . . . 6  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( F  o F  -  J )  o F  +  J
) `  k )  =  ( ( ( F  o F  -  J ) `  k
)  +  ( J `
 k ) ) )
2731, 3, 252, 254, 266, 267, 268, 272climadd 12354 . . . . 5  |-  (  T. 
->  ( ( F  o F  -  J )  o F  +  J
)  ~~>  ( 0  +  ( ( pi ^
2 )  /  6
) ) )
27491, 273eqbrtrrd 4177 . . . 4  |-  (  T. 
->  F  ~~>  ( 0  +  ( ( pi
^ 2 )  / 
6 ) ) )
275103addid2i 9188 . . . 4  |-  ( 0  +  ( ( pi
^ 2 )  / 
6 ) )  =  ( ( pi ^
2 )  /  6
)
276274, 22, 2753brtr3g 4186 . . 3  |-  (  T. 
->  seq  1 (  +  ,  ( n  e.  NN  |->  ( n ^ -u 2 ) ) )  ~~>  ( ( pi ^
2 )  /  6
) )
2771, 3, 8, 20, 276isumclim 12470 . 2  |-  (  T. 
->  sum_ k  e.  NN  ( k ^ -u 2
)  =  ( ( pi ^ 2 )  /  6 ) )
278277trud 1329 1  |-  sum_ k  e.  NN  ( k ^ -u 2 )  =  ( ( pi ^ 2 )  /  6 )
Colors of variables: wff set class
Syntax hints:    /\ wa 359    /\ w3a 936    T. wtru 1322    = wceq 1649    e. wcel 1717   _Vcvv 2901    C_ wss 3265   {csn 3759   class class class wbr 4155    e. cmpt 4209    X. cxp 4818    Fn wfn 5391   -->wf 5392   ` cfv 5396  (class class class)co 6022    o Fcof 6244   CCcc 8923   RRcr 8924   0cc0 8925   1c1 8926    + caddc 8928    x. cmul 8930    <_ cle 9056    - cmin 9225   -ucneg 9226    / cdiv 9611   NNcn 9934   2c2 9983   3c3 9984   6c6 9987   ZZcz 10216   ZZ>=cuz 10422    seq cseq 11252   ^cexp 11311    ~~> cli 12207   sum_csu 12408   picpi 12598
This theorem is referenced by:  basel  20741
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-rep 4263  ax-sep 4273  ax-nul 4281  ax-pow 4320  ax-pr 4346  ax-un 4643  ax-inf2 7531  ax-cnex 8981  ax-resscn 8982  ax-1cn 8983  ax-icn 8984  ax-addcl 8985  ax-addrcl 8986  ax-mulcl 8987  ax-mulrcl 8988  ax-mulcom 8989  ax-addass 8990  ax-mulass 8991  ax-distr 8992  ax-i2m1 8993  ax-1ne0 8994  ax-1rid 8995  ax-rnegex 8996  ax-rrecex 8997  ax-cnre 8998  ax-pre-lttri 8999  ax-pre-lttrn 9000  ax-pre-ltadd 9001  ax-pre-mulgt0 9002  ax-pre-sup 9003  ax-addf 9004  ax-mulf 9005
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-nel 2555  df-ral 2656  df-rex 2657  df-reu 2658  df-rmo 2659  df-rab 2660  df-v 2903  df-sbc 3107  df-csb 3197  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-pss 3281  df-nul 3574  df-if 3685  df-pw 3746  df-sn 3765  df-pr 3766  df-tp 3767  df-op 3768  df-uni 3960  df-int 3995  df-iun 4039  df-iin 4040  df-br 4156  df-opab 4210  df-mpt 4211  df-tr 4246  df-eprel 4437  df-id 4441  df-po 4446  df-so 4447  df-fr 4484  df-se 4485  df-we 4486  df-ord 4527  df-on 4528  df-lim 4529  df-suc 4530  df-om 4788  df-xp 4826  df-rel 4827  df-cnv 4828  df-co 4829  df-dm 4830  df-rn 4831  df-res 4832  df-ima 4833  df-iota 5360  df-fun 5398  df-fn 5399  df-f 5400  df-f1 5401  df-fo 5402  df-f1o 5403  df-fv 5404  df-isom 5405  df-ov 6025  df-oprab 6026  df-mpt2 6027  df-of 6246  df-1st 6290  df-2nd 6291  df-riota 6487  df-recs 6571  df-rdg 6606  df-1o 6662  df-2o 6663  df-oadd 6666  df-er 6843  df-map 6958  df-pm 6959  df-ixp 7002  df-en 7048  df-dom 7049  df-sdom 7050  df-fin 7051  df-fi 7353  df-sup 7383  df-oi 7414  df-card 7761  df-cda 7983  df-pnf 9057  df-mnf 9058  df-xr 9059  df-ltxr 9060  df-le 9061  df-sub 9227  df-neg 9228  df-div 9612  df-nn 9935  df-2 9992  df-3 9993  df-4 9994  df-5 9995  df-6 9996  df-7 9997  df-8 9998  df-9 9999  df-10 10000  df-n0 10156  df-z 10217  df-dec 10317  df-uz 10423  df-q 10509  df-rp 10547  df-xneg 10644  df-xadd 10645  df-xmul 10646  df-ioo 10854  df-ioc 10855  df-ico 10856  df-icc 10857  df-fz 10978  df-fzo 11068  df-fl 11131  df-mod 11180  df-seq 11253  df-exp 11312  df-fac 11496  df-bc 11523  df-hash 11548  df-shft 11811  df-cj 11833  df-re 11834  df-im 11835  df-sqr 11969  df-abs 11970  df-limsup 12194  df-clim 12211  df-rlim 12212  df-sum 12409  df-ef 12599  df-sin 12601  df-cos 12602  df-tan 12603  df-pi 12604  df-struct 13400  df-ndx 13401  df-slot 13402  df-base 13403  df-sets 13404  df-ress 13405  df-plusg 13471  df-mulr 13472  df-starv 13473  df-sca 13474  df-vsca 13475  df-tset 13477  df-ple 13478  df-ds 13480  df-unif 13481  df-hom 13482  df-cco 13483  df-rest 13579  df-topn 13580  df-topgen 13596  df-pt 13597  df-prds 13600  df-xrs 13655  df-0g 13656  df-gsum 13657  df-qtop 13662  df-imas 13663  df-xps 13665  df-mre 13740  df-mrc 13741  df-acs 13743  df-mnd 14619  df-submnd 14668  df-mulg 14744  df-cntz 15045  df-cmn 15343  df-xmet 16621  df-met 16622  df-bl 16623  df-mopn 16624  df-fbas 16625  df-fg 16626  df-cnfld 16629  df-top 16888  df-bases 16890  df-topon 16891  df-topsp 16892  df-cld 17008  df-ntr 17009  df-cls 17010  df-nei 17087  df-lp 17125  df-perf 17126  df-cn 17215  df-cnp 17216  df-haus 17303  df-tx 17517  df-hmeo 17710  df-fil 17801  df-fm 17893  df-flim 17894  df-flf 17895  df-xms 18261  df-ms 18262  df-tms 18263  df-cncf 18781  df-0p 19431  df-limc 19622  df-dv 19623  df-ply 19976  df-idp 19977  df-coe 19978  df-dgr 19979  df-quot 20077
  Copyright terms: Public domain W3C validator