let m be Nat; :: thesis: Sum (Basel-seq,m) <= Basel-seq2 . m
set 2m1 = (2 * m) + 1;
set 2m2 = (2 * m) + 2;
A1: ((((2 * m) * ((2 * m) + 2)) / 6) / (((2 * m) + 1) ^2)) / ((PI ^2) ") = ((((2 * m) * ((2 * m) + 2)) / (((2 * m) + 1) * ((2 * m) + 1))) * (PI ^2)) * (6 ")
.= ((((2 * m) / ((2 * m) + 1)) * (((2 * m) + 2) / ((2 * m) + 1))) * (PI ^2)) * (6 ") by XCMPLX_1:76
.= (((PI ^2) / 6) * ((2 * m) / ((2 * m) + 1))) * (((2 * m) + 2) / ((2 * m) + 1))
.= Basel-seq2 . m by BASEL_1:33 ;
Sum (sqr (cosec (x_r-seq m))) >= Sum ((sqr (x_r-seq m)) ") by BASEL_1:30;
then ((2 * m) * ((2 * m) + 2)) / 6 >= Sum ((sqr (x_r-seq m)) ") by Th29;
then ((2 * m) * ((2 * m) + 2)) / 6 >= ((((2 * m) + 1) ^2) / (PI ^2)) * (Sum (Basel-seq,m)) by BASEL_1:35;
then ((2 * m) * ((2 * m) + 2)) / 6 >= (((2 * m) + 1) ^2) * (((PI ^2) ") * (Sum (Basel-seq,m))) ;
then (((2 * m) * ((2 * m) + 2)) / 6) / (((2 * m) + 1) ^2) >= ((PI ^2) ") * (Sum (Basel-seq,m)) by XREAL_1:77;
hence Sum (Basel-seq,m) <= Basel-seq2 . m by A1, XREAL_1:77; :: thesis: verum