theorem Th44: :: WALLIS01:44

for n being non zero Nat holds
( 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) )