let n be non zero Nat; :: thesis: ('I' . (2 * n)) / ('I' . ((2 * n) + 1)) <= 1 + (1 / (2 * n))
set evenn = Product (even-seq n);
set oddn = Product (odd-seq n);
set oddn1 = Product (odd-seq (n + 1));
(Product (even-seq n)) / (Product (odd-seq (n + 1))) > 0 ;
then A1: 'I' . ((2 * n) + 1) > 0 by Th37;
0 < 0 + n ;
then 1 <= n by NAT_1:19;
then A2: 2 * n >= 2 * 1 by XREAL_1:64;
then A3: (2 * n) + 1 > 2 by NAT_1:13;
then A4: ((2 * n) + 1) -' 2 = ((2 * n) + 1) - 2 by XREAL_1:233
.= (2 * n) - 1
.= (2 * n) -' 1 by A2, XXREAL_0:2, XREAL_1:233 ;
A5: 'I' . ((2 * n) + 1) = ((((2 * n) + 1) -' 1) / ((2 * n) + 1)) * ('I' . (((2 * n) + 1) -' 2)) by A3, Th36
.= ((2 * n) / ((2 * n) + 1)) * ('I' . ((2 * n) -' 1)) by A4 ;
A6: 'I' . ((2 * n) -' 1) <> 0 by Lm8;
set s1 = (2 * n) / ((2 * n) + 1);
('I' . ((2 * n) -' 1)) / ('I' . ((2 * n) + 1)) = (1 / ('I' . ((2 * n) -' 1))) * (('I' . ((2 * n) -' 1)) / ((2 * n) / ((2 * n) + 1))) by A5, XCMPLX_1:103
.= (('I' . ((2 * n) -' 1)) * (1 / ('I' . ((2 * n) -' 1)))) / ((2 * n) / ((2 * n) + 1))
.= 1 / ((2 * n) / ((2 * n) + 1)) by A6, XCMPLX_1:106
.= (1 + ((2 * n) * 1)) / (2 * n) by XCMPLX_1:57
.= (1 / (2 * n)) + 1 by XCMPLX_1:113 ;
hence ('I' . (2 * n)) / ('I' . ((2 * n) + 1)) <= 1 + (1 / (2 * n)) by A1, Th43, XREAL_1:72; :: thesis: verum