let n be Nat; :: thesis: len (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) = n + 1
set PPn = <%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1);
A1: n + 1 is_at_least_length_of sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)

proof

let i be Nat; :: according to ALGSEQ_1:def 2 :: thesis: ( not n + 1 <= i or (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) . i = 0. F_Complex )
assume i >= n + 1 ; :: thesis: (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) . i = 0. F_Complex
then ( i + i >= (n + 1) + (n + 1) & ((2 * n) + 1) + 1 > ((2 * n) + 1) + 0 ) by XREAL_1:7, XREAL_1:8;
then 2 * i > (2 * n) + 1 by XXREAL_0:2;
then A2: ((2 * n) + 1) choose (2 * i) = 0 by NEWTON:def 3;
thus (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) . i = (<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)) . (2 * i) by Def5
.= 0 * (((1. F_Complex) |^ (2 * i)) * (i_FC |^ (((2 * n) + 1) -' (2 * i)))) by A2, Th13
.= 0. F_Complex ; :: thesis: verum

end;

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

proof

let m be Nat; :: thesis: ( m is_at_least_length_of sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2) implies n + 1 <= m )
assume A3: m is_at_least_length_of sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2) ; :: thesis: n + 1 <= m
assume m < n + 1 ; :: thesis: contradiction
then m <= n by NAT_1:13;
then (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) . n = 0. F_Complex by A3, ALGSEQ_1:def 2;
then (((2 * n) + 1) choose 1) * i_FC = 0. F_Complex by Th23;
hence contradiction ; :: thesis: verum

end;

hence len (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) = n + 1 by A1, ALGSEQ_1:def 3; :: thesis: verum