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

Theorem basellem9 20861
Description: Lemma for basel 20862. Since by basellem8 20860 
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 12424. 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 10511 . . 3  |-  NN  =  ( ZZ>= `  1 )
2 1z 10301 . . . 4  |-  1  e.  ZZ
32a1i 11 . . 3  |-  (  T. 
->  1  e.  ZZ )
4 oveq1 6080 . . . . 5  |-  ( n  =  k  ->  (
n ^ -u 2
)  =  ( k ^ -u 2 ) )
5 eqid 2435 . . . . 5  |-  ( n  e.  NN  |->  ( n ^ -u 2 ) )  =  ( n  e.  NN  |->  ( n ^ -u 2 ) )
6 ovex 6098 . . . . 5  |-  ( k ^ -u 2 )  e.  _V
74, 5, 6fvmpt 5798 . . . 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 9997 . . . . . . . . 9  |-  ( n  e.  NN  ->  n  e.  RR )
10 nnne0 10022 . . . . . . . . 9  |-  ( n  e.  NN  ->  n  =/=  0 )
11 2z 10302 . . . . . . . . . . 11  |-  2  e.  ZZ
12 znegcl 10303 . . . . . . . . . . 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 11538 . . . . . . . 8  |-  ( n  e.  NN  ->  (
n ^ -u 2
)  e.  RR )
1615adantl 453 . . . . . . 7  |-  ( (  T.  /\  n  e.  NN )  ->  (
n ^ -u 2
)  e.  RR )
1716, 5fmptd 5885 . . . . . 6  |-  (  T. 
->  ( n  e.  NN  |->  ( n ^ -u 2
) ) : NN --> RR )
1817ffvelrnda 5862 . . . . 5  |-  ( (  T.  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( n ^ -u 2
) ) `  k
)  e.  RR )
198, 18eqeltrrd 2510 . . . 4  |-  ( (  T.  /\  k  e.  NN )  ->  (
k ^ -u 2
)  e.  RR )
2019recnd 9104 . . 3  |-  ( (  T.  /\  k  e.  NN )  ->  (
k ^ -u 2
)  e.  CC )
211, 3, 18serfre 11342 . . . . . . . . . . 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 5577 . . . . . . . . . . 11  |-  ( F : NN --> RR  <->  seq  1
(  +  ,  ( n  e.  NN  |->  ( n ^ -u 2
) ) ) : NN --> RR )
2421, 23sylibr 204 . . . . . . . . . 10  |-  (  T. 
->  F : NN --> RR )
2524ffvelrnda 5862 . . . . . . . . 9  |-  ( (  T.  /\  n  e.  NN )  ->  ( F `  n )  e.  RR )
2625recnd 9104 . . . . . . . 8  |-  ( (  T.  /\  n  e.  NN )  ->  ( F `  n )  e.  CC )
27 remulcl 9065 . . . . . . . . . . . . 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 6098 . . . . . . . . . . . . . . . 16  |-  ( ( pi ^ 2 )  /  6 )  e. 
_V
3029fconst 5621 . . . . . . . . . . . . . . 15  |-  ( NN 
X.  { ( ( pi ^ 2 )  /  6 ) } ) : NN --> { ( ( pi ^ 2 )  /  6 ) }
31 pire 20362 . . . . . . . . . . . . . . . . . . 19  |-  pi  e.  RR
3231resqcli 11457 . . . . . . . . . . . . . . . . . 18  |-  ( pi
^ 2 )  e.  RR
33 6re 10066 . . . . . . . . . . . . . . . . . 18  |-  6  e.  RR
34 6nn 10127 . . . . . . . . . . . . . . . . . . 19  |-  6  e.  NN
3534nnne0i 10024 . . . . . . . . . . . . . . . . . 18  |-  6  =/=  0
3632, 33, 35redivcli 9771 . . . . . . . . . . . . . . . . 17  |-  ( ( pi ^ 2 )  /  6 )  e.  RR
3736a1i 11 . . . . . . . . . . . . . . . 16  |-  (  T. 
->  ( ( pi ^
2 )  /  6
)  e.  RR )
3837snssd 3935 . . . . . . . . . . . . . . 15  |-  (  T. 
->  { ( ( pi
^ 2 )  / 
6 ) }  C_  RR )
39 fss 5591 . . . . . . . . . . . . . . 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 9355 . . . . . . . . . . . . . . . 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 9076 . . . . . . . . . . . . . . . . 17  |-  1  e.  _V
4443fconst 5621 . . . . . . . . . . . . . . . 16  |-  ( NN 
X.  { 1 } ) : NN --> { 1 }
45 1re 9080 . . . . . . . . . . . . . . . . . 18  |-  1  e.  RR
4645a1i 11 . . . . . . . . . . . . . . . . 17  |-  (  T. 
->  1  e.  RR )
4746snssd 3935 . . . . . . . . . . . . . . . 16  |-  (  T. 
->  { 1 }  C_  RR )
48 fss 5591 . . . . . . . . . . . . . . . 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 10123 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  NN
5150a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  (  T. 
->  2  e.  NN )
52 nnmulcl 10013 . . . . . . . . . . . . . . . . . . 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 10007 . . . . . . . . . . . . . . . . 17  |-  ( (  T.  /\  n  e.  NN )  ->  (
( 2  x.  n
)  +  1 )  e.  NN )
5554nnrecred 10035 . . . . . . . . . . . . . . . 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 5885 . . . . . . . . . . . . . . 15  |-  (  T. 
->  G : NN --> RR )
58 nnex 9996 . . . . . . . . . . . . . . . 16  |-  NN  e.  _V
5958a1i 11 . . . . . . . . . . . . . . 15  |-  (  T. 
->  NN  e.  _V )
60 inidm 3542 . . . . . . . . . . . . . . 15  |-  ( NN 
i^i  NN )  =  NN
6142, 49, 57, 59, 59, 60off 6312 . . . . . . . . . . . . . 14  |-  (  T. 
->  ( ( NN  X.  { 1 } )  o F  -  G
) : NN --> RR )
6228, 40, 61, 59, 59, 60off 6312 . . . . . . . . . . . . 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 5577 . . . . . . . . . . . . 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 9063 . . . . . . . . . . . . . 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 2957 . . . . . . . . . . . . . . . 16  |-  -u 2  e.  _V
6968fconst 5621 . . . . . . . . . . . . . . 15  |-  ( NN 
X.  { -u 2 } ) : NN --> { -u 2 }
7013zrei 10278 . . . . . . . . . . . . . . . . 17  |-  -u 2  e.  RR
7170a1i 11 . . . . . . . . . . . . . . . 16  |-  (  T. 
->  -u 2  e.  RR )
7271snssd 3935 . . . . . . . . . . . . . . 15  |-  (  T. 
->  { -u 2 } 
C_  RR )
73 fss 5591 . . . . . . . . . . . . . . 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 6312 . . . . . . . . . . . . 13  |-  (  T. 
->  ( ( NN  X.  { -u 2 } )  o F  x.  G
) : NN --> RR )
7667, 49, 75, 59, 59, 60off 6312 . . . . . . . . . . . 12  |-  (  T. 
->  ( ( NN  X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G ) ) : NN --> RR )
7728, 65, 76, 59, 59, 60off 6312 . . . . . . . . . . 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 5577 . . . . . . . . . . 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 5862 . . . . . . . . 9  |-  ( (  T.  /\  n  e.  NN )  ->  ( J `  n )  e.  RR )
8281recnd 9104 . . . . . . . 8  |-  ( (  T.  /\  n  e.  NN )  ->  ( J `  n )  e.  CC )
8326, 82npcand 9405 . . . . . . 7  |-  ( (  T.  /\  n  e.  NN )  ->  (
( ( F `  n )  -  ( J `  n )
)  +  ( J `
 n ) )  =  ( F `  n ) )
8483mpteq2dva 4287 . . . . . 6  |-  (  T. 
->  ( n  e.  NN  |->  ( ( ( F `
 n )  -  ( J `  n ) )  +  ( J `
 n ) ) )  =  ( n  e.  NN  |->  ( F `
 n ) ) )
85 ovex 6098 . . . . . . . 8  |-  ( ( F `  n )  -  ( J `  n ) )  e. 
_V
8685a1i 11 . . . . . . 7  |-  ( (  T.  /\  n  e.  NN )  ->  (
( F `  n
)  -  ( J `
 n ) )  e.  _V )
8724feqmptd 5771 . . . . . . . 8  |-  (  T. 
->  F  =  (
n  e.  NN  |->  ( F `  n ) ) )
8880feqmptd 5771 . . . . . . . 8  |-  (  T. 
->  J  =  (
n  e.  NN  |->  ( J `  n ) ) )
8959, 25, 81, 87, 88offval2 6314 . . . . . . 7  |-  (  T. 
->  ( F  o F  -  J )  =  ( n  e.  NN  |->  ( ( F `  n )  -  ( J `  n )
) ) )
9059, 86, 81, 89, 88offval2 6314 . . . . . 6  |-  (  T. 
->  ( ( F  o F  -  J )  o F  +  J
)  =  ( n  e.  NN  |->  ( ( ( F `  n
)  -  ( J `
 n ) )  +  ( J `  n ) ) ) )
9184, 90, 873eqtr4d 2477 . . . . 5  |-  (  T. 
->  ( ( F  o F  -  J )  o F  +  J
)  =  F )
9267, 49, 57, 59, 59, 60off 6312 . . . . . . . . . 10  |-  (  T. 
->  ( ( NN  X.  { 1 } )  o F  +  G
) : NN --> RR )
93 recn 9070 . . . . . . . . . . . 12  |-  ( x  e.  RR  ->  x  e.  CC )
94 recn 9070 . . . . . . . . . . . 12  |-  ( y  e.  RR  ->  y  e.  CC )
95 recn 9070 . . . . . . . . . . . 12  |-  ( z  e.  RR  ->  z  e.  CC )
96 subdi 9457 . . . . . . . . . . . 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 6332 . . . . . . . . 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 6085 . . . . . . . . 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 2485 . . . . . . . 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 9092 . . . . . . . . . . . . . 14  |-  ( ( pi ^ 2 )  /  6 )  e.  CC
1041eqimss2i 3395 . . . . . . . . . . . . . . 15  |-  ( ZZ>= ` 
1 )  C_  NN
105104, 58climconst2 12332 . . . . . . . . . . . . . 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 6098 . . . . . . . . . . . . . 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 9037 . . . . . . . . . . . . . . . 16  |-  RR  C_  CC
110 fss 5591 . . . . . . . . . . . . . . . 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 5591 . . . . . . . . . . . . . . . 16  |-  ( ( G : NN --> RR  /\  RR  C_  CC )  ->  G : NN --> CC )
11357, 109, 112sylancl 644 . . . . . . . . . . . . . . 15  |-  (  T. 
->  G : NN --> CC )
114 ofnegsub 9988 . . . . . . . . . . . . . . 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 10057 . . . . . . . . . . . . . . 15  |-  -u 1  e.  CC
11756, 116basellem7 20859 . . . . . . . . . . . . . 14  |-  ( ( NN  X.  { 1 } )  o F  +  ( ( NN 
X.  { -u 1 } )  o F  x.  G ) )  ~~>  1
118115, 117syl6eqbrr 4242 . . . . . . . . . . . . 13  |-  (  T. 
->  ( ( NN  X.  { 1 } )  o F  -  G
)  ~~>  1 )
11940ffvelrnda 5862 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
( NN  X.  {
( ( pi ^
2 )  /  6
) } ) `  k )  e.  RR )
120119recnd 9104 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( NN  X.  {
( ( pi ^
2 )  /  6
) } ) `  k )  e.  CC )
12161ffvelrnda 5862 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 1 } )  o F  -  G
) `  k )  e.  RR )
122121recnd 9104 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 1 } )  o F  -  G
) `  k )  e.  CC )
123 ffn 5583 . . . . . . . . . . . . . . 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 5623 . . . . . . . . . . . . . . . 16  |-  ( 1  e.  ZZ  ->  ( NN  X.  { 1 } )  Fn  NN )
1263, 125syl 16 . . . . . . . . . . . . . . 15  |-  (  T. 
->  ( NN  X.  {
1 } )  Fn  NN )
127 ffn 5583 . . . . . . . . . . . . . . . 16  |-  ( G : NN --> RR  ->  G  Fn  NN )
12857, 127syl 16 . . . . . . . . . . . . . . 15  |-  (  T. 
->  G  Fn  NN )
129126, 128, 59, 59, 60offn 6308 . . . . . . . . . . . . . 14  |-  (  T. 
->  ( ( NN  X.  { 1 } )  o F  -  G
)  Fn  NN )
130 eqidd 2436 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
( NN  X.  {
( ( pi ^
2 )  /  6
) } ) `  k )  =  ( ( NN  X.  {
( ( pi ^
2 )  /  6
) } ) `  k ) )
131 eqidd 2436 . . . . . . . . . . . . . 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 6306 . . . . . . . . . . . . 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 12416 . . . . . . . . . . . 12  |-  (  T. 
->  ( ( NN  X.  { ( ( pi
^ 2 )  / 
6 ) } )  o F  x.  (
( NN  X.  {
1 } )  o F  -  G ) )  ~~>  ( ( ( pi ^ 2 )  /  6 )  x.  1 ) )
134103mulid1i 9082 . . . . . . . . . . . 12  |-  ( ( ( pi ^ 2 )  /  6 )  x.  1 )  =  ( ( pi ^
2 )  /  6
)
135133, 134syl6breq 4243 . . . . . . . . . . 11  |-  (  T. 
->  ( ( NN  X.  { ( ( pi
^ 2 )  / 
6 ) } )  o F  x.  (
( NN  X.  {
1 } )  o F  -  G ) )  ~~>  ( ( pi
^ 2 )  / 
6 ) )
13663, 135syl5eqbr 4237 . . . . . . . . . 10  |-  (  T. 
->  H  ~~>  ( (
pi ^ 2 )  /  6 ) )
137 ovex 6098 . . . . . . . . . . 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 10062 . . . . . . . . . . . . 13  |-  3  e.  CC
140104, 58climconst2 12332 . . . . . . . . . . . . 13  |-  ( ( 3  e.  CC  /\  1  e.  ZZ )  ->  ( NN  X.  {
3 } )  ~~>  3 )
141139, 3, 140sylancr 645 . . . . . . . . . . . 12  |-  (  T. 
->  ( NN  X.  {
3 } )  ~~>  3 )
142 ovex 6098 . . . . . . . . . . . . 13  |-  ( ( NN  X.  { 3 } )  o F  x.  G )  e. 
_V
143142a1i 11 . . . . . . . . . . . 12  |-  (  T. 
->  ( ( NN  X.  { 3 } )  o F  x.  G
)  e.  _V )
14456basellem6 20858 . . . . . . . . . . . . 13  |-  G  ~~>  0
145144a1i 11 . . . . . . . . . . . 12  |-  (  T. 
->  G  ~~>  0 )
146 3re 10061 . . . . . . . . . . . . . . . . 17  |-  3  e.  RR
147146elexi 2957 . . . . . . . . . . . . . . . 16  |-  3  e.  _V
148147fconst 5621 . . . . . . . . . . . . . . 15  |-  ( NN 
X.  { 3 } ) : NN --> { 3 }
149146a1i 11 . . . . . . . . . . . . . . . 16  |-  (  T. 
->  3  e.  RR )
150149snssd 3935 . . . . . . . . . . . . . . 15  |-  (  T. 
->  { 3 }  C_  RR )
151 fss 5591 . . . . . . . . . . . . . . 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 5862 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( NN  X.  {
3 } ) `  k )  e.  RR )
154153recnd 9104 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  (
( NN  X.  {
3 } ) `  k )  e.  CC )
15557ffvelrnda 5862 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  ( G `  k )  e.  RR )
156155recnd 9104 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  ( G `  k )  e.  CC )
157 ffn 5583 . . . . . . . . . . . . . 14  |-  ( ( NN  X.  { 3 } ) : NN --> RR  ->  ( NN  X.  { 3 } )  Fn  NN )
158152, 157syl 16 . . . . . . . . . . . . 13  |-  (  T. 
->  ( NN  X.  {
3 } )  Fn  NN )
159 eqidd 2436 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( NN  X.  {
3 } ) `  k )  =  ( ( NN  X.  {
3 } ) `  k ) )
160 eqidd 2436 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  ( G `  k )  =  ( G `  k ) )
161158, 128, 59, 59, 60, 159, 160ofval 6306 . . . . . . . . . . . 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 12416 . . . . . . . . . . 11  |-  (  T. 
->  ( ( NN  X.  { 3 } )  o F  x.  G
)  ~~>  ( 3  x.  0 ) )
163139mul01i 9246 . . . . . . . . . . 11  |-  ( 3  x.  0 )  =  0
164162, 163syl6breq 4243 . . . . . . . . . 10  |-  (  T. 
->  ( ( NN  X.  { 3 } )  o F  x.  G
)  ~~>  0 )
16565ffvelrnda 5862 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  ( H `  k )  e.  RR )
166165recnd 9104 . . . . . . . . . 10  |-  ( (  T.  /\  k  e.  NN )  ->  ( H `  k )  e.  CC )
16728, 152, 57, 59, 59, 60off 6312 . . . . . . . . . . . 12  |-  (  T. 
->  ( ( NN  X.  { 3 } )  o F  x.  G
) : NN --> RR )
168167ffvelrnda 5862 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 3 } )  o F  x.  G
) `  k )  e.  RR )
169168recnd 9104 . . . . . . . . . 10  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 3 } )  o F  x.  G
) `  k )  e.  CC )
170 ffn 5583 . . . . . . . . . . . 12  |-  ( H : NN --> RR  ->  H  Fn  NN )
17165, 170syl 16 . . . . . . . . . . 11  |-  (  T. 
->  H  Fn  NN )
17242, 92, 76, 59, 59, 60off 6312 . . . . . . . . . . . 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 5583 . . . . . . . . . . . 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 2436 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  ( H `  k )  =  ( H `  k ) )
176156mulid2d 9096 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  k  e.  NN )  ->  (
1  x.  ( G `
 k ) )  =  ( G `  k ) )
177 2cn 10060 . . . . . . . . . . . . . . . . . 18  |-  2  e.  CC
178 mulneg1 9460 . . . . . . . . . . . . . . . . . 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 9290 . . . . . . . . . . . . . . . 16  |-  ( (  T.  /\  k  e.  NN )  ->  -u ( -u 2  x.  ( G `
 k ) )  =  -u -u ( 2  x.  ( G `  k
) ) )
181 mulcl 9064 . . . . . . . . . . . . . . . . . 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 9392 . . . . . . . . . . . . . . . 16  |-  ( (  T.  /\  k  e.  NN )  ->  -u -u (
2  x.  ( G `
 k ) )  =  ( 2  x.  ( G `  k
) ) )
184180, 183eqtr2d 2468 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  k  e.  NN )  ->  (
2  x.  ( G `
 k ) )  =  -u ( -u 2  x.  ( G `  k
) ) )
185176, 184oveq12d 6091 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 1  x.  ( G `  k )
)  +  ( 2  x.  ( G `  k ) ) )  =  ( ( G `
 k )  + 
-u ( -u 2  x.  ( G `  k
) ) ) )
186 remulcl 9065 . . . . . . . . . . . . . . . . 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 9104 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  k  e.  NN )  ->  ( -u 2  x.  ( G `
 k ) )  e.  CC )
189156, 188negsubd 9407 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
( G `  k
)  +  -u ( -u 2  x.  ( G `
 k ) ) )  =  ( ( G `  k )  -  ( -u 2  x.  ( G `  k
) ) ) )
190185, 189eqtrd 2467 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 1  x.  ( G `  k )
)  +  ( 2  x.  ( G `  k ) ) )  =  ( ( G `
 k )  -  ( -u 2  x.  ( G `  k )
) ) )
191 df-3 10049 . . . . . . . . . . . . . . . 16  |-  3  =  ( 2  +  1 )
192 ax-1cn 9038 . . . . . . . . . . . . . . . . 17  |-  1  e.  CC
193177, 192addcomi 9247 . . . . . . . . . . . . . . . 16  |-  ( 2  +  1 )  =  ( 1  +  2 )
194191, 193eqtri 2455 . . . . . . . . . . . . . . 15  |-  3  =  ( 1  +  2 )
195194oveq1i 6083 . . . . . . . . . . . . . 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 9103 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 1  +  2 )  x.  ( G `
 k ) )  =  ( ( 1  x.  ( G `  k ) )  +  ( 2  x.  ( G `  k )
) ) )
199195, 198syl5eq 2479 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
3  x.  ( G `
 k ) )  =  ( ( 1  x.  ( G `  k ) )  +  ( 2  x.  ( G `  k )
) ) )
200196, 156, 188pnpcand 9438 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 1  +  ( G `  k ) )  -  ( 1  +  ( -u 2  x.  ( G `  k
) ) ) )  =  ( ( G `
 k )  -  ( -u 2  x.  ( G `  k )
) ) )
201190, 199, 2003eqtr4rd 2478 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 1  +  ( G `  k ) )  -  ( 1  +  ( -u 2  x.  ( G `  k
) ) ) )  =  ( 3  x.  ( G `  k
) ) )
202126, 128, 59, 59, 60offn 6308 . . . . . . . . . . . . 13  |-  (  T. 
->  ( ( NN  X.  { 1 } )  o F  +  G
)  Fn  NN )
20313a1i 11 . . . . . . . . . . . . . . . 16  |-  (  T. 
->  -u 2  e.  ZZ )
204 fnconstg 5623 . . . . . . . . . . . . . . . 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 6308 . . . . . . . . . . . . . 14  |-  (  T. 
->  ( ( NN  X.  { -u 2 } )  o F  x.  G
)  Fn  NN )
207126, 206, 59, 59, 60offn 6308 . . . . . . . . . . . . 13  |-  (  T. 
->  ( ( NN  X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G ) )  Fn  NN )
20859, 46, 128, 160ofc1 6319 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 1 } )  o F  +  G
) `  k )  =  ( 1  +  ( G `  k
) ) )
20959, 71, 128, 160ofc1 6319 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { -u 2 } )  o F  x.  G
) `  k )  =  ( -u 2  x.  ( G `  k
) ) )
21059, 46, 206, 209ofc1 6319 . . . . . . . . . . . . 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 6306 . . . . . . . . . . . 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 6319 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 3 } )  o F  x.  G
) `  k )  =  ( 3  x.  ( G `  k
) ) )
213201, 211, 2123eqtr4d 2477 . . . . . . . . . . 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 6306 . . . . . . . . . 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 12416 . . . . . . . . 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 9246 . . . . . . . . 9  |-  ( ( ( pi ^ 2 )  /  6 )  x.  0 )  =  0
217215, 216syl6breq 4243 . . . . . . . 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 4226 . . . . . . 7  |-  (  T. 
->  ( K  o F  -  J )  ~~>  0 )
219 ovex 6098 . . . . . . . 8  |-  ( F  o F  -  J
)  e.  _V
220219a1i 11 . . . . . . 7  |-  (  T. 
->  ( F  o F  -  J )  e. 
_V )
22128, 65, 92, 59, 59, 60off 6312 . . . . . . . . . 10  |-  (  T. 
->  ( H  o F  x.  ( ( NN 
X.  { 1 } )  o F  +  G ) ) : NN --> RR )
222100feq1i 5577 . . . . . . . . . 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 6312 . . . . . . . 8  |-  (  T. 
->  ( K  o F  -  J ) : NN --> RR )
225224ffvelrnda 5862 . . . . . . 7  |-  ( (  T.  /\  k  e.  NN )  ->  (
( K  o F  -  J ) `  k )  e.  RR )
22642, 24, 80, 59, 59, 60off 6312 . . . . . . . 8  |-  (  T. 
->  ( F  o F  -  J ) : NN --> RR )
227226ffvelrnda 5862 . . . . . . 7  |-  ( (  T.  /\  k  e.  NN )  ->  (
( F  o F  -  J ) `  k )  e.  RR )
22824ffvelrnda 5862 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  ( F `  k )  e.  RR )
229223ffvelrnda 5862 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  ( K `  k )  e.  RR )
23080ffvelrnda 5862 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  ( J `  k )  e.  RR )
231 eqid 2435 . . . . . . . . . . . 12  |-  ( ( 2  x.  k )  +  1 )  =  ( ( 2  x.  k )  +  1 )
23256, 22, 63, 78, 100, 231basellem8 20860 . . . . . . . . . . 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 9632 . . . . . . . 8  |-  ( (  T.  /\  k  e.  NN )  ->  (
( F `  k
)  -  ( J `
 k ) )  <_  ( ( K `
 k )  -  ( J `  k ) ) )
236 ffn 5583 . . . . . . . . . 10  |-  ( F : NN --> RR  ->  F  Fn  NN )
23724, 236syl 16 . . . . . . . . 9  |-  (  T. 
->  F  Fn  NN )
238 ffn 5583 . . . . . . . . . 10  |-  ( J : NN --> RR  ->  J  Fn  NN )
23980, 238syl 16 . . . . . . . . 9  |-  (  T. 
->  J  Fn  NN )
240 eqidd 2436 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  ( F `  k )  =  ( F `  k ) )
241 eqidd 2436 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  ( J `  k )  =  ( J `  k ) )
242237, 239, 59, 59, 60, 240, 241ofval 6306 . . . . . . . 8  |-  ( (  T.  /\  k  e.  NN )  ->  (
( F  o F  -  J ) `  k )  =  ( ( F `  k
)  -  ( J `
 k ) ) )
243 ffn 5583 . . . . . . . . . 10  |-  ( K : NN --> RR  ->  K  Fn  NN )
244223, 243syl 16 . . . . . . . . 9  |-  (  T. 
->  K  Fn  NN )
245 eqidd 2436 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  ( K `  k )  =  ( K `  k ) )
246244, 239, 59, 59, 60, 245, 241ofval 6306 . . . . . . . 8  |-  ( (  T.  /\  k  e.  NN )  ->  (
( K  o F  -  J ) `  k )  =  ( ( K `  k
)  -  ( J `
 k ) ) )
247235, 242, 2463brtr4d 4234 . . . . . . 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 9606 . . . . . . . . 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 4230 . . . . . . 7  |-  ( (  T.  /\  k  e.  NN )  ->  0  <_  ( ( F  o F  -  J ) `  k ) )
2521, 3, 218, 220, 225, 227, 247, 251climsqz2 12425 . . . . . 6  |-  (  T. 
->  ( F  o F  -  J )  ~~>  0 )
253 ovex 6098 . . . . . . 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 6098 . . . . . . . . . 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 9092 . . . . . . . . . . 11  |-  -u 2  e.  CC
25856, 257basellem7 20859 . . . . . . . . . 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 5862 . . . . . . . . . 10  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G ) ) `  k )  e.  RR )
261260recnd 9104 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G ) ) `  k )  e.  CC )
262 eqidd 2436 . . . . . . . . . 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 6306 . . . . . . . . 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 12416 . . . . . . . 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 4243 . . . . . . 7  |-  (  T. 
->  ( H  o F  x.  ( ( NN 
X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G
) ) )  ~~>  ( ( pi ^ 2 )  /  6 ) )
26678, 265syl5eqbr 4237 . . . . . 6  |-  (  T. 
->  J  ~~>  ( (
pi ^ 2 )  /  6 ) )
267227recnd 9104 . . . . . 6  |-  ( (  T.  /\  k  e.  NN )  ->  (
( F  o F  -  J ) `  k )  e.  CC )
268230recnd 9104 . . . . . 6  |-  ( (  T.  /\  k  e.  NN )  ->  ( J `  k )  e.  CC )
269 ffn 5583 . . . . . . . 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 2436 . . . . . . 7  |-  ( (  T.  /\  k  e.  NN )  ->  (
( F  o F  -  J ) `  k )  =  ( ( F  o F  -  J ) `  k ) )
272270, 239, 59, 59, 60, 271, 241ofval 6306 . . . . . 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 12415 . . . . 5  |-  (  T. 
->  ( ( F  o F  -  J )  o F  +  J
)  ~~>  ( 0  +  ( ( pi ^
2 )  /  6
) ) )
27491, 273eqbrtrrd 4226 . . . 4  |-  (  T. 
->  F  ~~>  ( 0  +  ( ( pi
^ 2 )  / 
6 ) ) )
275103addid2i 9244 . . . 4  |-  ( 0  +  ( ( pi
^ 2 )  / 
6 ) )  =  ( ( pi ^
2 )  /  6
)
276274, 22, 2753brtr3g 4235 . . 3  |-  (  T. 
->  seq  1 (  +  ,  ( n  e.  NN  |->  ( n ^ -u 2 ) ) )  ~~>  ( ( pi ^
2 )  /  6
) )
2771, 3, 8, 20, 276isumclim 12531 . 2  |-  (  T. 
->  sum_ k  e.  NN  ( k ^ -u 2
)  =  ( ( pi ^ 2 )  /  6 ) )
278277trud 1332 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 1325    = wceq 1652    e. wcel 1725   _Vcvv 2948    C_ wss 3312   {csn 3806   class class class wbr 4204    e. cmpt 4258    X. cxp 4868    Fn wfn 5441   -->wf 5442   ` cfv 5446  (class class class)co 6073    o Fcof 6295   CCcc 8978   RRcr 8979   0cc0 8980   1c1 8981    + caddc 8983    x. cmul 8985    <_ cle 9111    - cmin 9281   -ucneg 9282    / cdiv 9667   NNcn 9990   2c2 10039   3c3 10040   6c6 10043   ZZcz 10272   ZZ>=cuz 10478    seq cseq 11313   ^cexp 11372    ~~> cli 12268   sum_csu 12469   picpi 12659
This theorem is referenced by:  basel  20862
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-rep 4312  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-inf2 7586  ax-cnex 9036  ax-resscn 9037  ax-1cn 9038  ax-icn 9039  ax-addcl 9040  ax-addrcl 9041  ax-mulcl 9042  ax-mulrcl 9043  ax-mulcom 9044  ax-addass 9045  ax-mulass 9046  ax-distr 9047  ax-i2m1 9048  ax-1ne0 9049  ax-1rid 9050  ax-rnegex 9051  ax-rrecex 9052  ax-cnre 9053  ax-pre-lttri 9054  ax-pre-lttrn 9055  ax-pre-ltadd 9056  ax-pre-mulgt0 9057  ax-pre-sup 9058  ax-addf 9059  ax-mulf 9060
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-reu 2704  df-rmo 2705  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-int 4043  df-iun 4087  df-iin 4088  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-se 4534  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-isom 5455  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-of 6297  df-1st 6341  df-2nd 6342  df-riota 6541  df-recs 6625  df-rdg 6660  df-1o 6716  df-2o 6717  df-oadd 6720  df-er 6897  df-map 7012  df-pm 7013  df-ixp 7056  df-en 7102  df-dom 7103  df-sdom 7104  df-fin 7105  df-fi 7408  df-sup 7438  df-oi 7469  df-card 7816  df-cda 8038  df-pnf 9112  df-mnf 9113  df-xr 9114  df-ltxr 9115  df-le 9116  df-sub 9283  df-neg 9284  df-div 9668  df-nn 9991  df-2 10048  df-3 10049  df-4 10050  df-5 10051  df-6 10052  df-7 10053  df-8 10054  df-9 10055  df-10 10056  df-n0 10212  df-z 10273  df-dec 10373  df-uz 10479  df-q 10565  df-rp 10603  df-xneg 10700  df-xadd 10701  df-xmul 10702  df-ioo 10910  df-ioc 10911  df-ico 10912  df-icc 10913  df-fz 11034  df-fzo 11126  df-fl 11192  df-mod 11241  df-seq 11314  df-exp 11373  df-fac 11557  df-bc 11584  df-hash 11609  df-shft 11872  df-cj 11894  df-re 11895  df-im 11896  df-sqr 12030  df-abs 12031  df-limsup 12255  df-clim 12272  df-rlim 12273  df-sum 12470  df-ef 12660  df-sin 12662  df-cos 12663  df-tan 12664  df-pi 12665  df-struct 13461  df-ndx 13462  df-slot 13463  df-base 13464  df-sets 13465  df-ress 13466  df-plusg 13532  df-mulr 13533  df-starv 13534  df-sca 13535  df-vsca 13536  df-tset 13538  df-ple 13539  df-ds 13541  df-unif 13542  df-hom 13543  df-cco 13544  df-rest 13640  df-topn 13641  df-topgen 13657  df-pt 13658  df-prds 13661  df-xrs 13716  df-0g 13717  df-gsum 13718  df-qtop 13723  df-imas 13724  df-xps 13726  df-mre 13801  df-mrc 13802  df-acs 13804  df-mnd 14680  df-submnd 14729  df-mulg 14805  df-cntz 15106  df-cmn 15404  df-psmet 16684  df-xmet 16685  df-met 16686  df-bl 16687  df-mopn 16688  df-fbas 16689  df-fg 16690  df-cnfld 16694  df-top 16953  df-bases 16955  df-topon 16956  df-topsp 16957  df-cld 17073  df-ntr 17074  df-cls 17075  df-nei 17152  df-lp 17190  df-perf 17191  df-cn 17281  df-cnp 17282  df-haus 17369  df-tx 17584  df-hmeo 17777  df-fil 17868  df-fm 17960  df-flim 17961  df-flf 17962  df-xms 18340  df-ms 18341  df-tms 18342  df-cncf 18898  df-0p 19552  df-limc 19743  df-dv 19744  df-ply 20097  df-idp 20098  df-coe 20099  df-dgr 20100  df-quot 20198
  Copyright terms: Public domain W3C validator