let n be non zero Nat; :: thesis: 1 / ((1 + (1 / (2 * n))) * PI) <= (((Product (odd-seq n)) |^ 2) / ((Product (even-seq n)) |^ 2)) * n
set s = (((Product (odd-seq n)) |^ 2) / ((Product (even-seq n)) |^ 2)) * n;
1 <= ('I' . (2 * n)) / ('I' . ((2 * n) + 1)) by Th44;
then A1: 1 <= ((((Product (odd-seq n)) |^ 2) / ((Product (even-seq n)) |^ 2)) * n) * ((1 + (1 / (2 * n))) * PI) by Th44;
(((((Product (odd-seq n)) |^ 2) / ((Product (even-seq n)) |^ 2)) * n) * ((1 + (1 / (2 * n))) * PI)) * (1 / ((1 + (1 / (2 * n))) * PI)) = ((((Product (odd-seq n)) |^ 2) / ((Product (even-seq n)) |^ 2)) * n) * (((1 + (1 / (2 * n))) * PI) * (1 / ((1 + (1 / (2 * n))) * PI)))
.= (((Product (odd-seq n)) |^ 2) / ((Product (even-seq n)) |^ 2)) * n by COMPTRIG:5, XCMPLX_1:108 ;
hence 1 / ((1 + (1 / (2 * n))) * PI) <= (((Product (odd-seq n)) |^ 2) / ((Product (even-seq n)) |^ 2)) * n by A1, XREAL_1:64; :: thesis: verum