Metamath Proof Explorer

Theorem basel

Description: The sum of the inverse squares is _pi ^ 2 / 6 . This is commonly known as the Basel problem, with the first known proof attributed to Euler. See http://en.wikipedia.org/wiki/Basel_problem . This particular proof approach is due to Cauchy (1821). This is Metamath 100 proof #14. (Contributed by Mario Carneiro, 30-Jul-2014)

Ref Expression
Assertion basel 
|- sum_ k e. NN ( k ^ -u 2 ) = ( ( _pi ^ 2 ) / 6 )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( m = n -> ( 2 x. m ) = ( 2 x. n ) )
2 1 oveq1d 
 |-  ( m = n -> ( ( 2 x. m ) + 1 ) = ( ( 2 x. n ) + 1 ) )
3 2 oveq2d 
 |-  ( m = n -> ( 1 / ( ( 2 x. m ) + 1 ) ) = ( 1 / ( ( 2 x. n ) + 1 ) ) )
4 3 cbvmptv 
 |-  ( m e. NN |-> ( 1 / ( ( 2 x. m ) + 1 ) ) ) = ( n e. NN |-> ( 1 / ( ( 2 x. n ) + 1 ) ) )
5 oveq1 
 |-  ( m = n -> ( m ^ -u 2 ) = ( n ^ -u 2 ) )
6 5 cbvmptv 
 |-  ( m e. NN |-> ( m ^ -u 2 ) ) = ( n e. NN |-> ( n ^ -u 2 ) )
7 seqeq3 
 |-  ( ( m e. NN |-> ( m ^ -u 2 ) ) = ( n e. NN |-> ( n ^ -u 2 ) ) -> seq 1 ( + , ( m e. NN |-> ( m ^ -u 2 ) ) ) = seq 1 ( + , ( n e. NN |-> ( n ^ -u 2 ) ) ) )
8 6 7 ax-mp 
 |-  seq 1 ( + , ( m e. NN |-> ( m ^ -u 2 ) ) ) = seq 1 ( + , ( n e. NN |-> ( n ^ -u 2 ) ) )
9 eqid 
 |-  ( ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) oF x. ( ( NN X. { 1 } ) oF - ( m e. NN |-> ( 1 / ( ( 2 x. m ) + 1 ) ) ) ) ) = ( ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) oF x. ( ( NN X. { 1 } ) oF - ( m e. NN |-> ( 1 / ( ( 2 x. m ) + 1 ) ) ) ) )
10 eqid 
 |-  ( ( ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) oF x. ( ( NN X. { 1 } ) oF - ( m e. NN |-> ( 1 / ( ( 2 x. m ) + 1 ) ) ) ) ) oF x. ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. ( m e. NN |-> ( 1 / ( ( 2 x. m ) + 1 ) ) ) ) ) ) = ( ( ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) oF x. ( ( NN X. { 1 } ) oF - ( m e. NN |-> ( 1 / ( ( 2 x. m ) + 1 ) ) ) ) ) oF x. ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. ( m e. NN |-> ( 1 / ( ( 2 x. m ) + 1 ) ) ) ) ) )
11 eqid 
 |-  ( ( ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) oF x. ( ( NN X. { 1 } ) oF - ( m e. NN |-> ( 1 / ( ( 2 x. m ) + 1 ) ) ) ) ) oF x. ( ( NN X. { 1 } ) oF + ( m e. NN |-> ( 1 / ( ( 2 x. m ) + 1 ) ) ) ) ) = ( ( ( NN X. { ( ( _pi ^ 2 ) / 6 ) } ) oF x. ( ( NN X. { 1 } ) oF - ( m e. NN |-> ( 1 / ( ( 2 x. m ) + 1 ) ) ) ) ) oF x. ( ( NN X. { 1 } ) oF + ( m e. NN |-> ( 1 / ( ( 2 x. m ) + 1 ) ) ) ) )
12 4 8 9 10 11 basellem9 
 |-  sum_ k e. NN ( k ^ -u 2 ) = ( ( _pi ^ 2 ) / 6 )