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

Theorem basellem9 20824
Description: Lemma for basel 20825. Since by basellem8 20823 
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 12389. 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 10477 . . 3  |-  NN  =  ( ZZ>= `  1 )
2 1z 10267 . . . 4  |-  1  e.  ZZ
32a1i 11 . . 3  |-  (  T. 
->  1  e.  ZZ )
4 oveq1 6047 . . . . 5  |-  ( n  =  k  ->  (
n ^ -u 2
)  =  ( k ^ -u 2 ) )
5 eqid 2404 . . . . 5  |-  ( n  e.  NN  |->  ( n ^ -u 2 ) )  =  ( n  e.  NN  |->  ( n ^ -u 2 ) )
6 ovex 6065 . . . . 5  |-  ( k ^ -u 2 )  e.  _V
74, 5, 6fvmpt 5765 . . . 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 9963 . . . . . . . . 9  |-  ( n  e.  NN  ->  n  e.  RR )
10 nnne0 9988 . . . . . . . . 9  |-  ( n  e.  NN  ->  n  =/=  0 )
11 2z 10268 . . . . . . . . . . 11  |-  2  e.  ZZ
12 znegcl 10269 . . . . . . . . . . 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 11503 . . . . . . . 8  |-  ( n  e.  NN  ->  (
n ^ -u 2
)  e.  RR )
1615adantl 453 . . . . . . 7  |-  ( (  T.  /\  n  e.  NN )  ->  (
n ^ -u 2
)  e.  RR )
1716, 5fmptd 5852 . . . . . 6  |-  (  T. 
->  ( n  e.  NN  |->  ( n ^ -u 2
) ) : NN --> RR )
1817ffvelrnda 5829 . . . . 5  |-  ( (  T.  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( n ^ -u 2
) ) `  k
)  e.  RR )
198, 18eqeltrrd 2479 . . . 4  |-  ( (  T.  /\  k  e.  NN )  ->  (
k ^ -u 2
)  e.  RR )
2019recnd 9070 . . 3  |-  ( (  T.  /\  k  e.  NN )  ->  (
k ^ -u 2
)  e.  CC )
211, 3, 18serfre 11307 . . . . . . . . . . 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 5544 . . . . . . . . . . 11  |-  ( F : NN --> RR  <->  seq  1
(  +  ,  ( n  e.  NN  |->  ( n ^ -u 2
) ) ) : NN --> RR )
2421, 23sylibr 204 . . . . . . . . . 10  |-  (  T. 
->  F : NN --> RR )
2524ffvelrnda 5829 . . . . . . . . 9  |-  ( (  T.  /\  n  e.  NN )  ->  ( F `  n )  e.  RR )
2625recnd 9070 . . . . . . . 8  |-  ( (  T.  /\  n  e.  NN )  ->  ( F `  n )  e.  CC )
27 remulcl 9031 . . . . . . . . . . . . 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 6065 . . . . . . . . . . . . . . . 16  |-  ( ( pi ^ 2 )  /  6 )  e. 
_V
3029fconst 5588 . . . . . . . . . . . . . . 15  |-  ( NN 
X.  { ( ( pi ^ 2 )  /  6 ) } ) : NN --> { ( ( pi ^ 2 )  /  6 ) }
31 pire 20325 . . . . . . . . . . . . . . . . . . 19  |-  pi  e.  RR
3231resqcli 11422 . . . . . . . . . . . . . . . . . 18  |-  ( pi
^ 2 )  e.  RR
33 6re 10032 . . . . . . . . . . . . . . . . . 18  |-  6  e.  RR
34 6nn 10093 . . . . . . . . . . . . . . . . . . 19  |-  6  e.  NN
3534nnne0i 9990 . . . . . . . . . . . . . . . . . 18  |-  6  =/=  0
3632, 33, 35redivcli 9737 . . . . . . . . . . . . . . . . 17  |-  ( ( pi ^ 2 )  /  6 )  e.  RR
3736a1i 11 . . . . . . . . . . . . . . . 16  |-  (  T. 
->  ( ( pi ^
2 )  /  6
)  e.  RR )
3837snssd 3903 . . . . . . . . . . . . . . 15  |-  (  T. 
->  { ( ( pi
^ 2 )  / 
6 ) }  C_  RR )
39 fss 5558 . . . . . . . . . . . . . . 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 9321 . . . . . . . . . . . . . . . 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 9042 . . . . . . . . . . . . . . . . 17  |-  1  e.  _V
4443fconst 5588 . . . . . . . . . . . . . . . 16  |-  ( NN 
X.  { 1 } ) : NN --> { 1 }
45 1re 9046 . . . . . . . . . . . . . . . . . 18  |-  1  e.  RR
4645a1i 11 . . . . . . . . . . . . . . . . 17  |-  (  T. 
->  1  e.  RR )
4746snssd 3903 . . . . . . . . . . . . . . . 16  |-  (  T. 
->  { 1 }  C_  RR )
48 fss 5558 . . . . . . . . . . . . . . . 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 10089 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  NN
5150a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  (  T. 
->  2  e.  NN )
52 nnmulcl 9979 . . . . . . . . . . . . . . . . . . 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 9973 . . . . . . . . . . . . . . . . 17  |-  ( (  T.  /\  n  e.  NN )  ->  (
( 2  x.  n
)  +  1 )  e.  NN )
5554nnrecred 10001 . . . . . . . . . . . . . . . 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 5852 . . . . . . . . . . . . . . 15  |-  (  T. 
->  G : NN --> RR )
58 nnex 9962 . . . . . . . . . . . . . . . 16  |-  NN  e.  _V
5958a1i 11 . . . . . . . . . . . . . . 15  |-  (  T. 
->  NN  e.  _V )
60 inidm 3510 . . . . . . . . . . . . . . 15  |-  ( NN 
i^i  NN )  =  NN
6142, 49, 57, 59, 59, 60off 6279 . . . . . . . . . . . . . 14  |-  (  T. 
->  ( ( NN  X.  { 1 } )  o F  -  G
) : NN --> RR )
6228, 40, 61, 59, 59, 60off 6279 . . . . . . . . . . . . 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 5544 . . . . . . . . . . . . 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 9029 . . . . . . . . . . . . . 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 2925 . . . . . . . . . . . . . . . 16  |-  -u 2  e.  _V
6968fconst 5588 . . . . . . . . . . . . . . 15  |-  ( NN 
X.  { -u 2 } ) : NN --> { -u 2 }
7013zrei 10244 . . . . . . . . . . . . . . . . 17  |-  -u 2  e.  RR
7170a1i 11 . . . . . . . . . . . . . . . 16  |-  (  T. 
->  -u 2  e.  RR )
7271snssd 3903 . . . . . . . . . . . . . . 15  |-  (  T. 
->  { -u 2 } 
C_  RR )
73 fss 5558 . . . . . . . . . . . . . . 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 6279 . . . . . . . . . . . . 13  |-  (  T. 
->  ( ( NN  X.  { -u 2 } )  o F  x.  G
) : NN --> RR )
7667, 49, 75, 59, 59, 60off 6279 . . . . . . . . . . . 12  |-  (  T. 
->  ( ( NN  X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G ) ) : NN --> RR )
7728, 65, 76, 59, 59, 60off 6279 . . . . . . . . . . 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 5544 . . . . . . . . . . 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 5829 . . . . . . . . 9  |-  ( (  T.  /\  n  e.  NN )  ->  ( J `  n )  e.  RR )
8281recnd 9070 . . . . . . . 8  |-  ( (  T.  /\  n  e.  NN )  ->  ( J `  n )  e.  CC )
8326, 82npcand 9371 . . . . . . 7  |-  ( (  T.  /\  n  e.  NN )  ->  (
( ( F `  n )  -  ( J `  n )
)  +  ( J `
 n ) )  =  ( F `  n ) )
8483mpteq2dva 4255 . . . . . 6  |-  (  T. 
->  ( n  e.  NN  |->  ( ( ( F `
 n )  -  ( J `  n ) )  +  ( J `
 n ) ) )  =  ( n  e.  NN  |->  ( F `
 n ) ) )
85 ovex 6065 . . . . . . . 8  |-  ( ( F `  n )  -  ( J `  n ) )  e. 
_V
8685a1i 11 . . . . . . 7  |-  ( (  T.  /\  n  e.  NN )  ->  (
( F `  n
)  -  ( J `
 n ) )  e.  _V )
8724feqmptd 5738 . . . . . . . 8  |-  (  T. 
->  F  =  (
n  e.  NN  |->  ( F `  n ) ) )
8880feqmptd 5738 . . . . . . . 8  |-  (  T. 
->  J  =  (
n  e.  NN  |->  ( J `  n ) ) )
8959, 25, 81, 87, 88offval2 6281 . . . . . . 7  |-  (  T. 
->  ( F  o F  -  J )  =  ( n  e.  NN  |->  ( ( F `  n )  -  ( J `  n )
) ) )
9059, 86, 81, 89, 88offval2 6281 . . . . . 6  |-  (  T. 
->  ( ( F  o F  -  J )  o F  +  J
)  =  ( n  e.  NN  |->  ( ( ( F `  n
)  -  ( J `
 n ) )  +  ( J `  n ) ) ) )
9184, 90, 873eqtr4d 2446 . . . . 5  |-  (  T. 
->  ( ( F  o F  -  J )  o F  +  J
)  =  F )
9267, 49, 57, 59, 59, 60off 6279 . . . . . . . . . 10  |-  (  T. 
->  ( ( NN  X.  { 1 } )  o F  +  G
) : NN --> RR )
93 recn 9036 . . . . . . . . . . . 12  |-  ( x  e.  RR  ->  x  e.  CC )
94 recn 9036 . . . . . . . . . . . 12  |-  ( y  e.  RR  ->  y  e.  CC )
95 recn 9036 . . . . . . . . . . . 12  |-  ( z  e.  RR  ->  z  e.  CC )
96 subdi 9423 . . . . . . . . . . . 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 6299 . . . . . . . . 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 6052 . . . . . . . . 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 2454 . . . . . . . 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 9058 . . . . . . . . . . . . . 14  |-  ( ( pi ^ 2 )  /  6 )  e.  CC
1041eqimss2i 3363 . . . . . . . . . . . . . . 15  |-  ( ZZ>= ` 
1 )  C_  NN
105104, 58climconst2 12297 . . . . . . . . . . . . . 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 6065 . . . . . . . . . . . . . 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 9003 . . . . . . . . . . . . . . . 16  |-  RR  C_  CC
110 fss 5558 . . . . . . . . . . . . . . . 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 5558 . . . . . . . . . . . . . . . 16  |-  ( ( G : NN --> RR  /\  RR  C_  CC )  ->  G : NN --> CC )
11357, 109, 112sylancl 644 . . . . . . . . . . . . . . 15  |-  (  T. 
->  G : NN --> CC )
114 ofnegsub 9954 . . . . . . . . . . . . . . 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 10023 . . . . . . . . . . . . . . 15  |-  -u 1  e.  CC
11756, 116basellem7 20822 . . . . . . . . . . . . . 14  |-  ( ( NN  X.  { 1 } )  o F  +  ( ( NN 
X.  { -u 1 } )  o F  x.  G ) )  ~~>  1
118115, 117syl6eqbrr 4210 . . . . . . . . . . . . 13  |-  (  T. 
->  ( ( NN  X.  { 1 } )  o F  -  G
)  ~~>  1 )
11940ffvelrnda 5829 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
( NN  X.  {
( ( pi ^
2 )  /  6
) } ) `  k )  e.  RR )
120119recnd 9070 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( NN  X.  {
( ( pi ^
2 )  /  6
) } ) `  k )  e.  CC )
12161ffvelrnda 5829 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 1 } )  o F  -  G
) `  k )  e.  RR )
122121recnd 9070 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 1 } )  o F  -  G
) `  k )  e.  CC )
123 ffn 5550 . . . . . . . . . . . . . . 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 5590 . . . . . . . . . . . . . . . 16  |-  ( 1  e.  ZZ  ->  ( NN  X.  { 1 } )  Fn  NN )
1263, 125syl 16 . . . . . . . . . . . . . . 15  |-  (  T. 
->  ( NN  X.  {
1 } )  Fn  NN )
127 ffn 5550 . . . . . . . . . . . . . . . 16  |-  ( G : NN --> RR  ->  G  Fn  NN )
12857, 127syl 16 . . . . . . . . . . . . . . 15  |-  (  T. 
->  G  Fn  NN )
129126, 128, 59, 59, 60offn 6275 . . . . . . . . . . . . . 14  |-  (  T. 
->  ( ( NN  X.  { 1 } )  o F  -  G
)  Fn  NN )
130 eqidd 2405 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
( NN  X.  {
( ( pi ^
2 )  /  6
) } ) `  k )  =  ( ( NN  X.  {
( ( pi ^
2 )  /  6
) } ) `  k ) )
131 eqidd 2405 . . . . . . . . . . . . . 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 6273 . . . . . . . . . . . . 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 12381 . . . . . . . . . . . 12  |-  (  T. 
->  ( ( NN  X.  { ( ( pi
^ 2 )  / 
6 ) } )  o F  x.  (
( NN  X.  {
1 } )  o F  -  G ) )  ~~>  ( ( ( pi ^ 2 )  /  6 )  x.  1 ) )
134103mulid1i 9048 . . . . . . . . . . . 12  |-  ( ( ( pi ^ 2 )  /  6 )  x.  1 )  =  ( ( pi ^
2 )  /  6
)
135133, 134syl6breq 4211 . . . . . . . . . . 11  |-  (  T. 
->  ( ( NN  X.  { ( ( pi
^ 2 )  / 
6 ) } )  o F  x.  (
( NN  X.  {
1 } )  o F  -  G ) )  ~~>  ( ( pi
^ 2 )  / 
6 ) )
13663, 135syl5eqbr 4205 . . . . . . . . . 10  |-  (  T. 
->  H  ~~>  ( (
pi ^ 2 )  /  6 ) )
137 ovex 6065 . . . . . . . . . . 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 10028 . . . . . . . . . . . . 13  |-  3  e.  CC
140104, 58climconst2 12297 . . . . . . . . . . . . 13  |-  ( ( 3  e.  CC  /\  1  e.  ZZ )  ->  ( NN  X.  {
3 } )  ~~>  3 )
141139, 3, 140sylancr 645 . . . . . . . . . . . 12  |-  (  T. 
->  ( NN  X.  {
3 } )  ~~>  3 )
142 ovex 6065 . . . . . . . . . . . . 13  |-  ( ( NN  X.  { 3 } )  o F  x.  G )  e. 
_V
143142a1i 11 . . . . . . . . . . . 12  |-  (  T. 
->  ( ( NN  X.  { 3 } )  o F  x.  G
)  e.  _V )
14456basellem6 20821 . . . . . . . . . . . . 13  |-  G  ~~>  0
145144a1i 11 . . . . . . . . . . . 12  |-  (  T. 
->  G  ~~>  0 )
146 3re 10027 . . . . . . . . . . . . . . . . 17  |-  3  e.  RR
147146elexi 2925 . . . . . . . . . . . . . . . 16  |-  3  e.  _V
148147fconst 5588 . . . . . . . . . . . . . . 15  |-  ( NN 
X.  { 3 } ) : NN --> { 3 }
149146a1i 11 . . . . . . . . . . . . . . . 16  |-  (  T. 
->  3  e.  RR )
150149snssd 3903 . . . . . . . . . . . . . . 15  |-  (  T. 
->  { 3 }  C_  RR )
151 fss 5558 . . . . . . . . . . . . . . 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 5829 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( NN  X.  {
3 } ) `  k )  e.  RR )
154153recnd 9070 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  (
( NN  X.  {
3 } ) `  k )  e.  CC )
15557ffvelrnda 5829 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  ( G `  k )  e.  RR )
156155recnd 9070 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  ( G `  k )  e.  CC )
157 ffn 5550 . . . . . . . . . . . . . 14  |-  ( ( NN  X.  { 3 } ) : NN --> RR  ->  ( NN  X.  { 3 } )  Fn  NN )
158152, 157syl 16 . . . . . . . . . . . . 13  |-  (  T. 
->  ( NN  X.  {
3 } )  Fn  NN )
159 eqidd 2405 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( NN  X.  {
3 } ) `  k )  =  ( ( NN  X.  {
3 } ) `  k ) )
160 eqidd 2405 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  ( G `  k )  =  ( G `  k ) )
161158, 128, 59, 59, 60, 159, 160ofval 6273 . . . . . . . . . . . 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 12381 . . . . . . . . . . 11  |-  (  T. 
->  ( ( NN  X.  { 3 } )  o F  x.  G
)  ~~>  ( 3  x.  0 ) )
163139mul01i 9212 . . . . . . . . . . 11  |-  ( 3  x.  0 )  =  0
164162, 163syl6breq 4211 . . . . . . . . . 10  |-  (  T. 
->  ( ( NN  X.  { 3 } )  o F  x.  G
)  ~~>  0 )
16565ffvelrnda 5829 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  ( H `  k )  e.  RR )
166165recnd 9070 . . . . . . . . . 10  |-  ( (  T.  /\  k  e.  NN )  ->  ( H `  k )  e.  CC )
16728, 152, 57, 59, 59, 60off 6279 . . . . . . . . . . . 12  |-  (  T. 
->  ( ( NN  X.  { 3 } )  o F  x.  G
) : NN --> RR )
168167ffvelrnda 5829 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 3 } )  o F  x.  G
) `  k )  e.  RR )
169168recnd 9070 . . . . . . . . . 10  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 3 } )  o F  x.  G
) `  k )  e.  CC )
170 ffn 5550 . . . . . . . . . . . 12  |-  ( H : NN --> RR  ->  H  Fn  NN )
17165, 170syl 16 . . . . . . . . . . 11  |-  (  T. 
->  H  Fn  NN )
17242, 92, 76, 59, 59, 60off 6279 . . . . . . . . . . . 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 5550 . . . . . . . . . . . 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 2405 . . . . . . . . . . 11  |-  ( (  T.  /\  k  e.  NN )  ->  ( H `  k )  =  ( H `  k ) )
176156mulid2d 9062 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  k  e.  NN )  ->  (
1  x.  ( G `
 k ) )  =  ( G `  k ) )
177 2cn 10026 . . . . . . . . . . . . . . . . . 18  |-  2  e.  CC
178 mulneg1 9426 . . . . . . . . . . . . . . . . . 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 9256 . . . . . . . . . . . . . . . 16  |-  ( (  T.  /\  k  e.  NN )  ->  -u ( -u 2  x.  ( G `
 k ) )  =  -u -u ( 2  x.  ( G `  k
) ) )
181 mulcl 9030 . . . . . . . . . . . . . . . . . 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 9358 . . . . . . . . . . . . . . . 16  |-  ( (  T.  /\  k  e.  NN )  ->  -u -u (
2  x.  ( G `
 k ) )  =  ( 2  x.  ( G `  k
) ) )
184180, 183eqtr2d 2437 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  k  e.  NN )  ->  (
2  x.  ( G `
 k ) )  =  -u ( -u 2  x.  ( G `  k
) ) )
185176, 184oveq12d 6058 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 1  x.  ( G `  k )
)  +  ( 2  x.  ( G `  k ) ) )  =  ( ( G `
 k )  + 
-u ( -u 2  x.  ( G `  k
) ) ) )
186 remulcl 9031 . . . . . . . . . . . . . . . . 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 9070 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  k  e.  NN )  ->  ( -u 2  x.  ( G `
 k ) )  e.  CC )
189156, 188negsubd 9373 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
( G `  k
)  +  -u ( -u 2  x.  ( G `
 k ) ) )  =  ( ( G `  k )  -  ( -u 2  x.  ( G `  k
) ) ) )
190185, 189eqtrd 2436 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 1  x.  ( G `  k )
)  +  ( 2  x.  ( G `  k ) ) )  =  ( ( G `
 k )  -  ( -u 2  x.  ( G `  k )
) ) )
191 df-3 10015 . . . . . . . . . . . . . . . 16  |-  3  =  ( 2  +  1 )
192 ax-1cn 9004 . . . . . . . . . . . . . . . . 17  |-  1  e.  CC
193177, 192addcomi 9213 . . . . . . . . . . . . . . . 16  |-  ( 2  +  1 )  =  ( 1  +  2 )
194191, 193eqtri 2424 . . . . . . . . . . . . . . 15  |-  3  =  ( 1  +  2 )
195194oveq1i 6050 . . . . . . . . . . . . . 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 9069 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 1  +  2 )  x.  ( G `
 k ) )  =  ( ( 1  x.  ( G `  k ) )  +  ( 2  x.  ( G `  k )
) ) )
199195, 198syl5eq 2448 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
3  x.  ( G `
 k ) )  =  ( ( 1  x.  ( G `  k ) )  +  ( 2  x.  ( G `  k )
) ) )
200196, 156, 188pnpcand 9404 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 1  +  ( G `  k ) )  -  ( 1  +  ( -u 2  x.  ( G `  k
) ) ) )  =  ( ( G `
 k )  -  ( -u 2  x.  ( G `  k )
) ) )
201190, 199, 2003eqtr4rd 2447 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  (
( 1  +  ( G `  k ) )  -  ( 1  +  ( -u 2  x.  ( G `  k
) ) ) )  =  ( 3  x.  ( G `  k
) ) )
202126, 128, 59, 59, 60offn 6275 . . . . . . . . . . . . 13  |-  (  T. 
->  ( ( NN  X.  { 1 } )  o F  +  G
)  Fn  NN )
20313a1i 11 . . . . . . . . . . . . . . . 16  |-  (  T. 
->  -u 2  e.  ZZ )
204 fnconstg 5590 . . . . . . . . . . . . . . . 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 6275 . . . . . . . . . . . . . 14  |-  (  T. 
->  ( ( NN  X.  { -u 2 } )  o F  x.  G
)  Fn  NN )
207126, 206, 59, 59, 60offn 6275 . . . . . . . . . . . . 13  |-  (  T. 
->  ( ( NN  X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G ) )  Fn  NN )
20859, 46, 128, 160ofc1 6286 . . . . . . . . . . . . 13  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 1 } )  o F  +  G
) `  k )  =  ( 1  +  ( G `  k
) ) )
20959, 71, 128, 160ofc1 6286 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { -u 2 } )  o F  x.  G
) `  k )  =  ( -u 2  x.  ( G `  k
) ) )
21059, 46, 206, 209ofc1 6286 . . . . . . . . . . . . 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 6273 . . . . . . . . . . . 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 6286 . . . . . . . . . . . 12  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 3 } )  o F  x.  G
) `  k )  =  ( 3  x.  ( G `  k
) ) )
213201, 211, 2123eqtr4d 2446 . . . . . . . . . . 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 6273 . . . . . . . . . 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 12381 . . . . . . . . 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 9212 . . . . . . . . 9  |-  ( ( ( pi ^ 2 )  /  6 )  x.  0 )  =  0
217215, 216syl6breq 4211 . . . . . . . 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 4194 . . . . . . 7  |-  (  T. 
->  ( K  o F  -  J )  ~~>  0 )
219 ovex 6065 . . . . . . . 8  |-  ( F  o F  -  J
)  e.  _V
220219a1i 11 . . . . . . 7  |-  (  T. 
->  ( F  o F  -  J )  e. 
_V )
22128, 65, 92, 59, 59, 60off 6279 . . . . . . . . . 10  |-  (  T. 
->  ( H  o F  x.  ( ( NN 
X.  { 1 } )  o F  +  G ) ) : NN --> RR )
222100feq1i 5544 . . . . . . . . . 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 6279 . . . . . . . 8  |-  (  T. 
->  ( K  o F  -  J ) : NN --> RR )
225224ffvelrnda 5829 . . . . . . 7  |-  ( (  T.  /\  k  e.  NN )  ->  (
( K  o F  -  J ) `  k )  e.  RR )
22642, 24, 80, 59, 59, 60off 6279 . . . . . . . 8  |-  (  T. 
->  ( F  o F  -  J ) : NN --> RR )
227226ffvelrnda 5829 . . . . . . 7  |-  ( (  T.  /\  k  e.  NN )  ->  (
( F  o F  -  J ) `  k )  e.  RR )
22824ffvelrnda 5829 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  ( F `  k )  e.  RR )
229223ffvelrnda 5829 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  ( K `  k )  e.  RR )
23080ffvelrnda 5829 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  ( J `  k )  e.  RR )
231 eqid 2404 . . . . . . . . . . . 12  |-  ( ( 2  x.  k )  +  1 )  =  ( ( 2  x.  k )  +  1 )
23256, 22, 63, 78, 100, 231basellem8 20823 . . . . . . . . . . 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 9598 . . . . . . . 8  |-  ( (  T.  /\  k  e.  NN )  ->  (
( F `  k
)  -  ( J `
 k ) )  <_  ( ( K `
 k )  -  ( J `  k ) ) )
236 ffn 5550 . . . . . . . . . 10  |-  ( F : NN --> RR  ->  F  Fn  NN )
23724, 236syl 16 . . . . . . . . 9  |-  (  T. 
->  F  Fn  NN )
238 ffn 5550 . . . . . . . . . 10  |-  ( J : NN --> RR  ->  J  Fn  NN )
23980, 238syl 16 . . . . . . . . 9  |-  (  T. 
->  J  Fn  NN )
240 eqidd 2405 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  ( F `  k )  =  ( F `  k ) )
241 eqidd 2405 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  ( J `  k )  =  ( J `  k ) )
242237, 239, 59, 59, 60, 240, 241ofval 6273 . . . . . . . 8  |-  ( (  T.  /\  k  e.  NN )  ->  (
( F  o F  -  J ) `  k )  =  ( ( F `  k
)  -  ( J `
 k ) ) )
243 ffn 5550 . . . . . . . . . 10  |-  ( K : NN --> RR  ->  K  Fn  NN )
244223, 243syl 16 . . . . . . . . 9  |-  (  T. 
->  K  Fn  NN )
245 eqidd 2405 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  ( K `  k )  =  ( K `  k ) )
246244, 239, 59, 59, 60, 245, 241ofval 6273 . . . . . . . 8  |-  ( (  T.  /\  k  e.  NN )  ->  (
( K  o F  -  J ) `  k )  =  ( ( K `  k
)  -  ( J `
 k ) ) )
247235, 242, 2463brtr4d 4202 . . . . . . 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 9572 . . . . . . . . 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 4198 . . . . . . 7  |-  ( (  T.  /\  k  e.  NN )  ->  0  <_  ( ( F  o F  -  J ) `  k ) )
2521, 3, 218, 220, 225, 227, 247, 251climsqz2 12390 . . . . . 6  |-  (  T. 
->  ( F  o F  -  J )  ~~>  0 )
253 ovex 6065 . . . . . . 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 6065 . . . . . . . . . 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 9058 . . . . . . . . . . 11  |-  -u 2  e.  CC
25856, 257basellem7 20822 . . . . . . . . . 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 5829 . . . . . . . . . 10  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G ) ) `  k )  e.  RR )
261260recnd 9070 . . . . . . . . 9  |-  ( (  T.  /\  k  e.  NN )  ->  (
( ( NN  X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G ) ) `  k )  e.  CC )
262 eqidd 2405 . . . . . . . . . 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 6273 . . . . . . . . 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 12381 . . . . . . . 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 4211 . . . . . . 7  |-  (  T. 
->  ( H  o F  x.  ( ( NN 
X.  { 1 } )  o F  +  ( ( NN  X.  { -u 2 } )  o F  x.  G
) ) )  ~~>  ( ( pi ^ 2 )  /  6 ) )
26678, 265syl5eqbr 4205 . . . . . 6  |-  (  T. 
->  J  ~~>  ( (
pi ^ 2 )  /  6 ) )
267227recnd 9070 . . . . . 6  |-  ( (  T.  /\  k  e.  NN )  ->  (
( F  o F  -  J ) `  k )  e.  CC )
268230recnd 9070 . . . . . 6  |-  ( (  T.  /\  k  e.  NN )  ->  ( J `  k )  e.  CC )
269 ffn 5550 . . . . . . . 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 2405 . . . . . . 7  |-  ( (  T.  /\  k  e.  NN )  ->  (
( F  o F  -  J ) `  k )  =  ( ( F  o F  -  J ) `  k ) )
272270, 239, 59, 59, 60, 271, 241ofval 6273 . . . . . 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 12380 . . . . 5  |-  (  T. 
->  ( ( F  o F  -  J )  o F  +  J
)  ~~>  ( 0  +  ( ( pi ^
2 )  /  6
) ) )
27491, 273eqbrtrrd 4194 . . . 4  |-  (  T. 
->  F  ~~>  ( 0  +  ( ( pi
^ 2 )  / 
6 ) ) )
275103addid2i 9210 . . . 4  |-  ( 0  +  ( ( pi
^ 2 )  / 
6 ) )  =  ( ( pi ^
2 )  /  6
)
276274, 22, 2753brtr3g 4203 . . 3  |-  (  T. 
->  seq  1 (  +  ,  ( n  e.  NN  |->  ( n ^ -u 2 ) ) )  ~~>  ( ( pi ^
2 )  /  6
) )
2771, 3, 8, 20, 276isumclim 12496 . 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 1721   _Vcvv 2916    C_ wss 3280   {csn 3774   class class class wbr 4172    e. cmpt 4226    X. cxp 4835    Fn wfn 5408   -->wf 5409   ` cfv 5413  (class class class)co 6040    o Fcof 6262   CCcc 8944   RRcr 8945   0cc0 8946   1c1 8947    + caddc 8949    x. cmul 8951    <_ cle 9077    - cmin 9247   -ucneg 9248    / cdiv 9633   NNcn 9956   2c2 10005   3c3 10006   6c6 10009   ZZcz 10238   ZZ>=cuz 10444    seq cseq 11278   ^cexp 11337    ~~> cli 12233   sum_csu 12434   picpi 12624
This theorem is referenced by:  basel  20825
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 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024  ax-addf 9025  ax-mulf 9026
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 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-iin 4056  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-of 6264  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-2o 6684  df-oadd 6687  df-er 6864  df-map 6979  df-pm 6980  df-ixp 7023  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-fi 7374  df-sup 7404  df-oi 7435  df-card 7782  df-cda 8004  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-4 10016  df-5 10017  df-6 10018  df-7 10019  df-8 10020  df-9 10021  df-10 10022  df-n0 10178  df-z 10239  df-dec 10339  df-uz 10445  df-q 10531  df-rp 10569  df-xneg 10666  df-xadd 10667  df-xmul 10668  df-ioo 10876  df-ioc 10877  df-ico 10878  df-icc 10879  df-fz 11000  df-fzo 11091  df-fl 11157  df-mod 11206  df-seq 11279  df-exp 11338  df-fac 11522  df-bc 11549  df-hash 11574  df-shft 11837  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-limsup 12220  df-clim 12237  df-rlim 12238  df-sum 12435  df-ef 12625  df-sin 12627  df-cos 12628  df-tan 12629  df-pi 12630  df-struct 13426  df-ndx 13427  df-slot 13428  df-base 13429  df-sets 13430  df-ress 13431  df-plusg 13497  df-mulr 13498  df-starv 13499  df-sca 13500  df-vsca 13501  df-tset 13503  df-ple 13504  df-ds 13506  df-unif 13507  df-hom 13508  df-cco 13509  df-rest 13605  df-topn 13606  df-topgen 13622  df-pt 13623  df-prds 13626  df-xrs 13681  df-0g 13682  df-gsum 13683  df-qtop 13688  df-imas 13689  df-xps 13691  df-mre 13766  df-mrc 13767  df-acs 13769  df-mnd 14645  df-submnd 14694  df-mulg 14770  df-cntz 15071  df-cmn 15369  df-psmet 16649  df-xmet 16650  df-met 16651  df-bl 16652  df-mopn 16653  df-fbas 16654  df-fg 16655  df-cnfld 16659  df-top 16918  df-bases 16920  df-topon 16921  df-topsp 16922  df-cld 17038  df-ntr 17039  df-cls 17040  df-nei 17117  df-lp 17155  df-perf 17156  df-cn 17245  df-cnp 17246  df-haus 17333  df-tx 17547  df-hmeo 17740  df-fil 17831  df-fm 17923  df-flim 17924  df-flf 17925  df-xms 18303  df-ms 18304  df-tms 18305  df-cncf 18861  df-0p 19515  df-limc 19706  df-dv 19707  df-ply 20060  df-idp 20061  df-coe 20062  df-dgr 20063  df-quot 20161
  Copyright terms: Public domain W3C validator