let m be Nat; :: thesis: Basel-seq1 . m <= Sum (Basel-seq,m)
set 2m1 = (2 * m) + 1;
set 2mI = (2 * m) - 1;
A1: ((((2 * m) * ((2 * m) - 1)) / 6) / (((2 * m) + 1) ^2)) / ((PI ^2) ") = ((((2 * m) * ((2 * m) - 1)) / (((2 * m) + 1) * ((2 * m) + 1))) * (PI ^2)) * (6 ")
.= ((((2 * m) / ((2 * m) + 1)) * (((2 * m) - 1) / ((2 * m) + 1))) * (PI ^2)) * (6 ") by XCMPLX_1:76
.= (((PI ^2) / 6) * ((2 * m) / ((2 * m) + 1))) * (((2 * m) - 1) / ((2 * m) + 1))
.= Basel-seq1 . m by BASEL_1:32 ;
Sum (sqr (cot (x_r-seq m))) <= Sum ((sqr (x_r-seq m)) ") by BASEL_1:29;
then ((2 * m) * ((2 * m) - 1)) / 6 <= Sum ((sqr (x_r-seq m)) ") by Th28;
then ((2 * m) * ((2 * m) - 1)) / 6 <= ((((2 * m) + 1) ^2) / (PI ^2)) * (Sum (Basel-seq,m)) by BASEL_1:35;
then ((2 * m) * ((2 * m) - 1)) / 6 <= (((2 * m) + 1) ^2) * (((PI ^2) ") * (Sum (Basel-seq,m))) ;
then (((2 * m) * ((2 * m) - 1)) / 6) / (((2 * m) + 1) ^2) <= ((PI ^2) ") * (Sum (Basel-seq,m)) by XREAL_1:79;
hence Basel-seq1 . m <= Sum (Basel-seq,m) by A1, XREAL_1:79; :: thesis: verum