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