let n be Nat; :: thesis: ( n >= 1 implies (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) . (n - 1) = (((2 * n) + 1) choose 3) * (- i_FC) )
A1: i_FC |^ 1 = i_FC by BINOM:8;
assume n >= 1 ; :: thesis: (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) . (n - 1) = (((2 * n) + 1) choose 3) * (- i_FC)
then reconsider n1 = n - 1 as Nat ;
n1 <= n1 + 1 by NAT_1:11;
then A2: 2 * n1 < (2 * n) + 1 by NAT_1:13, XREAL_1:64;
then ((2 * n) + 1) -' (2 * n1) = ((2 * n) + 1) - (2 * n1) by XREAL_1:233;
then A3: i_FC |^ (((2 * n) + 1) -' (2 * n1)) = i_FC |^ (2 + 1)
.= (i_FC |^ (1 + 1)) * (i_FC |^ 1) by BINOM:10
.= (i_FC * i_FC) * i_FC by A1, BINOM:10
.= - ((1_ F_Complex) * i_FC) by HAHNBAN1:4, VECTSP_1:9
.= - i_FC ;
A4: (1. F_Complex) |^ (2 * n1) = 1_ F_Complex by Th3;
((2 * n) + 1) - (2 * n1) = 3 ;
then A5: ((2 * n) + 1) choose (2 * n1) = ((2 * n) + 1) choose 3 by A2, NEWTON:20;
(sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) . n1 = (<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)) . (2 * n1) by Def5
.= (((2 * n) + 1) choose 3) * (((1. F_Complex) |^ (2 * n1)) * (- i_FC)) by A3, A5, Th13
.= (((2 * n) + 1) choose 3) * (- i_FC) by A4 ;
hence (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) . (n - 1) = (((2 * n) + 1) choose 3) * (- i_FC) ; :: thesis: verum