theorem Th24: :: BASEL_2:24

for n being Nat st n >= 1 holds
(sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) . (n - 1) = (((2 * n) + 1) choose 3) * (- i_FC)