let n be non zero Nat; ( 1 <= ('I' . (2 * n)) / ('I' . ((2 * n) + 1)) & ('I' . (2 * n)) / ('I' . ((2 * n) + 1)) = ((((Product (odd-seq n)) |^ 2) / ((Product (even-seq n)) |^ 2)) * n) * ((1 + (1 / (2 * n))) * PI) )
set evenn = Product (even-seq n);
set oddn = Product (odd-seq n);
set oddn1 = Product (odd-seq (n + 1));
A1:
'I' . (2 * n) = ((Product (odd-seq n)) / (Product (even-seq n))) * (PI / 2)
by Th38;
A2: n + (1 / 2) =
(n * 1) + (1 / 2)
.=
n * (1 + ((1 / 2) / n))
by XCMPLX_1:235
.=
n * (1 + ((1 / 2) * (1 / n)))
.=
n * (1 + (1 / (2 * n)))
by XCMPLX_1:103
;
A3: ((Product (odd-seq n)) * (Product (odd-seq (n + 1)))) / ((Product (even-seq n)) * (Product (even-seq n))) =
((((2 * n) + 1) * (Product (odd-seq n))) * (Product (odd-seq n))) / ((Product (even-seq n)) * (Product (even-seq n)))
by Th10
.=
(((2 * n) + 1) * ((Product (odd-seq n)) * (Product (odd-seq n)))) / ((Product (even-seq n)) |^ 2)
by WSIERP_1:1
.=
(((2 * n) + 1) * ((Product (odd-seq n)) |^ 2)) / ((Product (even-seq n)) |^ 2)
by WSIERP_1:1
;
A4: ('I' . (2 * n)) / ('I' . ((2 * n) + 1)) =
(((Product (odd-seq n)) / (Product (even-seq n))) * (PI / 2)) / ((Product (even-seq n)) / (Product (odd-seq (n + 1))))
by Th37, A1
.=
(PI / 2) * (((Product (odd-seq n)) / (Product (even-seq n))) / ((Product (even-seq n)) / (Product (odd-seq (n + 1)))))
.=
(PI / 2) * ((((2 * n) + 1) * ((Product (odd-seq n)) |^ 2)) / ((Product (even-seq n)) |^ 2))
by A3, XCMPLX_1:84
.=
((((Product (odd-seq n)) |^ 2) / ((Product (even-seq n)) |^ 2)) * (n + (1 / 2))) * PI
.=
((((Product (odd-seq n)) |^ 2) / ((Product (even-seq n)) |^ 2)) * (n * (1 + (1 / (2 * n))))) * PI
by A2
;
'I' . ((2 * n) + 1) = (Product (even-seq n)) / (Product (odd-seq (n + 1)))
by Th37;
hence
( 1 <= ('I' . (2 * n)) / ('I' . ((2 * n) + 1)) & ('I' . (2 * n)) / ('I' . ((2 * n) + 1)) = ((((Product (odd-seq n)) |^ 2) / ((Product (even-seq n)) |^ 2)) * n) * ((1 + (1 / (2 * n))) * PI) )
by A4, Th43, XREAL_1:181; verum