deffunc H1( non zero Nat) -> Polynomial of F_Complex = cyclotomic_poly \$1;
set cPRFC = the carrier of ;
set cFC = the carrier of F_Complex;
defpred S1[ non zero Element of NAT ] means ( ( H1(\$1) . 0 = 1 or H1(\$1) . 0 = - 1 ) & ( for i being Element of NAT holds H1(\$1) . i is integer ) );
A1: - () = - 1 by ;
A2: now :: thesis: for k being non zero Element of NAT st ( for n being non zero Element of NAT st n < k holds
S1[n] ) holds
S1[k]
let k be non zero Element of NAT ; :: thesis: ( ( for n being non zero Element of NAT st n < k holds
S1[n] ) implies S1[b1] )

assume A3: for n being non zero Element of NAT st n < k holds
S1[n] ; :: thesis: S1[b1]
A4: 1 <= k by Lm1;
per cases ( k = 1 or k > 1 ) by ;
suppose A5: k = 1 ; :: thesis: S1[b1]
now :: thesis: for i being Element of NAT holds H1(k) . i is integer
let i be Element of NAT ; :: thesis: H1(k) . b1 is integer
per cases ( i = 0 or i = 1 or i >= 2 ) by NAT_1:23;
suppose i = 0 ; :: thesis: H1(k) . b1 is integer
hence H1(k) . i is integer by ; :: thesis: verum
end;
suppose i = 1 ; :: thesis: H1(k) . b1 is integer
hence H1(k) . i is integer by ; :: thesis: verum
end;
suppose i >= 2 ; :: thesis: H1(k) . b1 is integer
hence H1(k) . i is integer by ; :: thesis: verum
end;
end;
end;
hence S1[k] by A1, A5, Th48, POLYNOM5:38; :: thesis: verum
end;
suppose A6: k > 1 ; :: thesis: S1[b1]
consider f being FinSequence of the carrier of , p being Polynomial of F_Complex such that
A7: p = Product f and
A8: dom f = Seg k and
A9: for i being non zero Element of NAT st i in Seg k holds
( ( ( not i divides k or i = k ) implies f . i = ) & ( i divides k & i <> k implies f . i = H1(i) ) ) and
A10: unital_poly (F_Complex,k) = () *' p by Th50;
defpred S2[ Nat, object ] means ex g being FinSequence of the carrier of ex p being Polynomial of F_Complex st
( g = f | (Seg \$1) & p = Product g & \$2 = p & ( p . 0 = 1 or p . 0 = - 1 ) & ( for j being Element of NAT holds p . j is integer ) );
defpred S3[ Nat] means ( \$1 in Seg (len f) implies ex x being object st S2[\$1,x] );
A11: k = len f by ;
A12: for l being Nat st S3[l] holds
S3[l + 1]
proof
let l be Nat; :: thesis: ( S3[l] implies S3[l + 1] )
assume A13: S3[l] ; :: thesis: S3[l + 1]
assume A14: l + 1 in Seg (len f) ; :: thesis: ex x being object st S2[l + 1,x]
per cases ( l = 0 or 0 < l ) ;
suppose A15: l = 0 ; :: thesis: ex x being object st S2[l + 1,x]
reconsider fl1 = f . (l + 1) as Element of the carrier of by ;
reconsider g = f | (Seg (l + 1)) as FinSequence of the carrier of by FINSEQ_1:18;
reconsider p = Product g as Polynomial of F_Complex by POLYNOM3:def 10;
<*> the carrier of = f | () ;
then g = (<*> the carrier of ) ^ <*(f . (l + 1))*> by
.= <*(f . (l + 1))*> by FINSEQ_1:34 ;
then A16: p = fl1 by FINSOP_1:11;
take p ; :: thesis: S2[l + 1,p]
take g ; :: thesis: ex p being Polynomial of F_Complex st
( g = f | (Seg (l + 1)) & p = Product g & p = p & ( p . 0 = 1 or p . 0 = - 1 ) & ( for j being Element of NAT holds p . j is integer ) )

take p ; :: thesis: ( g = f | (Seg (l + 1)) & p = Product g & p = p & ( p . 0 = 1 or p . 0 = - 1 ) & ( for j being Element of NAT holds p . j is integer ) )
thus ( g = f | (Seg (l + 1)) & p = Product g & p = p ) ; :: thesis: ( ( p . 0 = 1 or p . 0 = - 1 ) & ( for j being Element of NAT holds p . j is integer ) )
1 divides k by NAT_D:6;
then A17: f . 1 = H1(1) by A6, A9, A11, A14, A15;
hence ( p . 0 = 1 or p . 0 = - 1 ) by ; :: thesis: for j being Element of NAT holds p . j is integer
let j be Element of NAT ; :: thesis: p . j is integer
thus p . j is integer :: thesis: verum
proof
per cases ( j = 0 or j = 1 or j >= 2 ) by NAT_1:23;
suppose j = 0 ; :: thesis: p . j is integer
hence p . j is integer by ; :: thesis: verum
end;
suppose j = 1 ; :: thesis: p . j is integer
hence p . j is integer by ; :: thesis: verum
end;
suppose j >= 2 ; :: thesis: p . j is integer
hence p . j is integer by ; :: thesis: verum
end;
end;
end;
end;
suppose A18: 0 < l ; :: thesis: ex x being object st S2[l + 1,x]
( l + 1 <= len f & l <= l + 1 ) by ;
then A19: l <= len f by XXREAL_0:2;
0 + 1 <= l by ;
then consider x being set such that
A20: S2[l,x] by A13, A19, FINSEQ_1:1;
reconsider fl1 = f . (l + 1) as Element of the carrier of by ;
reconsider g1 = f | (Seg (l + 1)) as FinSequence of the carrier of by FINSEQ_1:18;
reconsider p1 = Product g1 as Polynomial of F_Complex by POLYNOM3:def 10;
take p1 ; :: thesis: S2[l + 1,p1]
take g1 ; :: thesis: ex p being Polynomial of F_Complex st
( g1 = f | (Seg (l + 1)) & p = Product g1 & p1 = p & ( p . 0 = 1 or p . 0 = - 1 ) & ( for j being Element of NAT holds p . j is integer ) )

take p1 ; :: thesis: ( g1 = f | (Seg (l + 1)) & p1 = Product g1 & p1 = p1 & ( p1 . 0 = 1 or p1 . 0 = - 1 ) & ( for j being Element of NAT holds p1 . j is integer ) )
thus ( g1 = f | (Seg (l + 1)) & p1 = Product g1 & p1 = p1 ) ; :: thesis: ( ( p1 . 0 = 1 or p1 . 0 = - 1 ) & ( for j being Element of NAT holds p1 . j is integer ) )
reconsider fl1p = fl1 as Polynomial of F_Complex by POLYNOM3:def 10;
reconsider m1 = - 1 as Element of COMPLEX by XCMPLX_0:def 2;
consider g being FinSequence of the carrier of , p being Polynomial of F_Complex such that
A21: g = f | (Seg l) and
A22: p = Product g and
x = p and
A23: ( p . 0 = 1 or p . 0 = - 1 ) and
A24: for j being Element of NAT holds p . j is integer by A20;
g1 = g ^ <*fl1*> by ;
then Product g1 = () * fl1 by GROUP_4:6;
then A25: p1 = p *' fl1p by ;
thus ( ( p1 . 0 = 1 or p1 . 0 = - 1 ) & ( for j being Element of NAT holds p1 . j is integer ) ) :: thesis: verum
proof
per cases ( not l + 1 divides k or l + 1 = k or ( l + 1 divides k & l + 1 <> k ) ) ;
suppose ( not l + 1 divides k or l + 1 = k ) ; :: thesis: ( ( p1 . 0 = 1 or p1 . 0 = - 1 ) & ( for j being Element of NAT holds p1 . j is integer ) )
then A26: fl1p = by A9, A11, A14;
consider r being FinSequence of F_Complex such that
A27: len r = 0 + 1 and
A28: p1 . 0 = Sum r and
A29: for m being Element of NAT st m in dom r holds
r . m = (p . (m -' 1)) * (fl1p . ((0 + 1) -' m)) by ;
1 in dom r by ;
then reconsider r1 = r . 1 as Element of F_Complex by FINSEQ_2:11;
r = <*r1*> by ;
then A30: p1 . 0 = r1 by ;
1 in dom r by ;
then A31: p1 . 0 = (p . (1 -' 1)) * (fl1p . ((0 + 1) -' 1)) by
.= (p . ((0 + 1) -' 1)) * (fl1p . 0) by NAT_D:34
.= (p . 0) * (fl1p . 0) by NAT_D:34
.= (p . 0) * () by ;
thus ( p1 . 0 = 1 or p1 . 0 = - 1 ) :: thesis: for j being Element of NAT holds p1 . j is integer
proof
per cases ( p . 0 = 1 or p . 0 = - 1 ) by A23;
suppose p . 0 = 1 ; :: thesis: ( p1 . 0 = 1 or p1 . 0 = - 1 )
hence ( p1 . 0 = 1 or p1 . 0 = - 1 ) by A31; :: thesis: verum
end;
suppose p . 0 = - 1 ; :: thesis: ( p1 . 0 = 1 or p1 . 0 = - 1 )
hence ( p1 . 0 = 1 or p1 . 0 = - 1 ) by A31; :: thesis: verum
end;
end;
end;
let j be Element of NAT ; :: thesis: p1 . j is integer
consider r being FinSequence of F_Complex such that
len r = j + 1 and
A32: p1 . j = Sum r and
A33: for m being Element of NAT st m in dom r holds
r . m = (p . (m -' 1)) * (fl1p . ((j + 1) -' m)) by ;
for i being Element of NAT st i in dom r holds
r . i is integer
proof
let i be Element of NAT ; :: thesis: ( i in dom r implies r . i is integer )
reconsider pi1 = p . (i -' 1) as Integer by A24;
set j1i = (j + 1) -' i;
now :: thesis: ( ( (j + 1) -' i = 0 & fl1p . ((j + 1) -' i) = 1 ) or ( (j + 1) -' i >= 1 & fl1p . ((j + 1) -' i) = 0 ) )
A34: ( (j + 1) -' i = 0 or (j + 1) -' i >= 0 + 1 ) by NAT_1:13;
per cases ) -' i = 0 or (j + 1) -' i >= 1 ) by A34;
case (j + 1) -' i = 0 ; :: thesis: fl1p . ((j + 1) -' i) = 1
hence fl1p . ((j + 1) -' i) = 1 by ; :: thesis: verum
end;
case (j + 1) -' i >= 1 ; :: thesis: fl1p . ((j + 1) -' i) = 0
hence fl1p . ((j + 1) -' i) = 0 by ; :: thesis: verum
end;
end;
end;
then reconsider fl1pj1i = fl1p . ((j + 1) -' i) as Integer ;
assume i in dom r ; :: thesis: r . i is integer
then r . i = (p . (i -' 1)) * (fl1p . ((j + 1) -' i)) by A33
.= pi1 * fl1pj1i ;
hence r . i is integer ; :: thesis: verum
end;
hence p1 . j is integer by ; :: thesis: verum
end;
suppose A35: ( l + 1 divides k & l + 1 <> k ) ; :: thesis: ( ( p1 . 0 = 1 or p1 . 0 = - 1 ) & ( for j being Element of NAT holds p1 . j is integer ) )
consider r being FinSequence of F_Complex such that
A36: len r = 0 + 1 and
A37: p1 . 0 = Sum r and
A38: for m being Element of NAT st m in dom r holds
r . m = (p . (m -' 1)) * (fl1p . ((0 + 1) -' m)) by ;
1 in dom r by ;
then reconsider r1 = r . 1 as Element of F_Complex by FINSEQ_2:11;
r = <*r1*> by ;
then A39: p1 . 0 = r1 by ;
1 in dom r by ;
then A40: p1 . 0 = (p . (1 -' 1)) * (fl1p . ((0 + 1) -' 1)) by
.= (p . ((0 + 1) -' 1)) * (fl1p . 0) by NAT_D:34
.= (p . 0) * (fl1p . 0) by NAT_D:34 ;
l + 1 <= k by ;
then A41: l + 1 < k by ;
A42: l + 1 in NAT by ORDINAL1:def 12;
A43: fl1p = H1(l + 1) by A9, A11, A14, A35;
then reconsider fl1p0 = fl1p . 0 as Integer by A3, A41, A42;
A44: ( fl1p0 = 1 or fl1p0 = m1 ) by A3, A43, A41, A42;
thus ( p1 . 0 = 1 or p1 . 0 = - 1 ) :: thesis: for j being Element of NAT holds p1 . j is integer
proof
per cases ( p . 0 = 1 or p . 0 = - 1 ) by A23;
suppose p . 0 = 1 ; :: thesis: ( p1 . 0 = 1 or p1 . 0 = - 1 )
hence ( p1 . 0 = 1 or p1 . 0 = - 1 ) by A3, A43, A41, A40; :: thesis: verum
end;
suppose p . 0 = - 1 ; :: thesis: ( p1 . 0 = 1 or p1 . 0 = - 1 )
hence ( p1 . 0 = 1 or p1 . 0 = - 1 ) by ; :: thesis: verum
end;
end;
end;
let j be Element of NAT ; :: thesis: p1 . j is integer
consider r being FinSequence of F_Complex such that
len r = j + 1 and
A45: p1 . j = Sum r and
A46: for m being Element of NAT st m in dom r holds
r . m = (p . (m -' 1)) * (fl1p . ((j + 1) -' m)) by ;
for i being Element of NAT st i in dom r holds
r . i is integer
proof
let i be Element of NAT ; :: thesis: ( i in dom r implies r . i is integer )
l + 1 in NAT by ORDINAL1:def 12;
then reconsider fl1pj1i = fl1p . ((j + 1) -' i) as Integer by A3, A43, A41;
reconsider pi1 = p . (i -' 1) as Integer by A24;
assume i in dom r ; :: thesis: r . i is integer
then r . i = (p . (i -' 1)) * (fl1p . ((j + 1) -' i)) by A46
.= pi1 * fl1pj1i ;
hence r . i is integer ; :: thesis: verum
end;
hence p1 . j is integer by ; :: thesis: verum
end;
end;
end;
end;
end;
end;
defpred S4[ Nat] means H1(k) . \$1 is integer ;
A47: (0 + 1) -' 1 = 0 by NAT_D:34;
A48: S3[ 0 ] by FINSEQ_1:1;
for l being Nat holds S3[l] from then A49: for l being Nat st l in Seg (len f) holds
ex x being object st S2[l,x] ;
consider F being FinSequence such that
dom F = Seg (len f) and
A50: for i being Nat st i in Seg (len f) holds
S2[i,F . i] from consider g being FinSequence of the carrier of , p1 being Polynomial of F_Complex such that
A51: ( g = f | (Seg k) & p1 = Product g ) and
F . k = p1 and
A52: ( p1 . 0 = 1 or p1 . 0 = - 1 ) and
A53: for j being Element of NAT holds p1 . j is integer by ;
A54: p = p1 by ;
A55: now :: thesis: for m being Nat st ( for n being Nat st n < m holds
S4[n] ) holds
S4[m]
let m be Nat; :: thesis: ( ( for n being Nat st n < m holds
S4[n] ) implies S4[b1] )

reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
consider r being FinSequence of the carrier of F_Complex such that
A56: len r = m + 1 and
A57: (unital_poly (F_Complex,k)) . m = Sum r and
A58: for l being Element of NAT st l in dom r holds
r . l = (p . (l -' 1)) * (H1(k) . ((m1 + 1) -' l)) by ;
reconsider Src = Sum r as Element of COMPLEX by COMPLFLD:def 1;
now :: thesis: Src is integer
per cases ( m1 = 0 or m1 = k or ( m1 <> 0 & m1 <> k ) ) ;
end;
end;
then reconsider Sr = Src as Integer ;
A59: ((1,1) -cut r) ^ (((1 + 1),(len r)) -cut r) = r by ;
set s = ((1 + 1),(len r)) -cut r;
reconsider Ssc = Sum (((1 + 1),(len r)) -cut r) as Element of COMPLEX by COMPLFLD:def 1;
assume A60: for n being Nat st n < m holds
S4[n] ; :: thesis: S4[b1]
now :: thesis: for i being Element of NAT st i in dom (((1 + 1),(len r)) -cut r) holds
(((1 + 1),(len r)) -cut r) . i is integer
let i be Element of NAT ; :: thesis: ( i in dom (((1 + 1),(len r)) -cut r) implies (((1 + 1),(len r)) -cut r) . b1 is integer )
assume A61: i in dom (((1 + 1),(len r)) -cut r) ; :: thesis: (((1 + 1),(len r)) -cut r) . b1 is integer
per cases ( len r < 2 or 1 + 1 <= len r ) ;
suppose len r < 2 ; :: thesis: (((1 + 1),(len r)) -cut r) . b1 is integer
then ((1 + 1),(len r)) -cut r = {} by FINSEQ_6:def 4;
hence (((1 + 1),(len r)) -cut r) . i is integer ; :: thesis: verum
end;
suppose A62: 1 + 1 <= len r ; :: thesis: (((1 + 1),(len r)) -cut r) . b1 is integer
then A63: (len (((1 + 1),(len r)) -cut r)) + (1 + 1) = (len r) + 1 by FINSEQ_6:def 4;
per cases ( m = 0 or m > 0 ) ;
suppose m = 0 ; :: thesis: (((1 + 1),(len r)) -cut r) . b1 is integer
hence (((1 + 1),(len r)) -cut r) . i is integer by ; :: thesis: verum
end;
suppose A64: m > 0 ; :: thesis: (((1 + 1),(len r)) -cut r) . b1 is integer
i <> 0 by ;
then reconsider cpkmi = H1(k) . (m -' i) as Integer by ;
reconsider ppi = p . i as Integer by ;
i <> 0 by ;
then consider i1 being Nat such that
A65: i = i1 + 1 by NAT_1:6;
A66: i <= len (((1 + 1),(len r)) -cut r) by ;
then ( 1 <= i + 1 & i + 1 <= (len (((1 + 1),(len r)) -cut r)) + 1 ) by ;
then 1 + i in dom r by ;
then A67: r . (1 + i) = (p . ((1 + i) -' 1)) * (H1(k) . ((m + 1) -' (1 + i))) by A58
.= (p . ((i + 1) -' 1)) * (H1(k) . (((m + 1) -' 1) -' i)) by NAT_2:30
.= (p . i) * (H1(k) . (((m + 1) -' 1) -' i)) by NAT_D:34
.= ppi * cpkmi by NAT_D:34 ;
i1 < len (((1 + 1),(len r)) -cut r) by ;
then (((1 + 1),(len r)) -cut r) . i = r . ((1 + 1) + i1) by
.= r . (1 + i) by A65 ;
hence (((1 + 1),(len r)) -cut r) . i is integer by A67; :: thesis: verum
end;
end;
end;
end;
end;
then reconsider Ss = Ssc as Integer by Th4;
A68: 1 <= len r by ;
then A69: 1 in dom r by FINSEQ_3:25;
then reconsider r1 = r . 1 as Element of the carrier of F_Complex by FINSEQ_2:11;
reconsider r1c = r1 as Element of COMPLEX by COMPLFLD:def 1;
(1,1) -cut r = <*r1*> by ;
then Sum r = r1 + (Sum (((1 + 1),(len r)) -cut r)) by ;
then r1c = Sr - Ss ;
then reconsider r1i = r1 as Integer ;
A70: r1i = (p . (1 -' 1)) * (H1(k) . ((m + 1) -' 1)) by
.= (p . 0) * (H1(k) . m1) by ;
per cases ( p . 0 = 1 or p . 0 = - 1 ) by ;
suppose p . 0 = - 1 ; :: thesis: S4[b1]
then r1 = (- ()) * (H1(k) . m1) by
.= - (() * (H1(k) . m1)) by VECTSP_1:9
.= - (H1(k) . m1) ;
then 0. F_Complex = (- (H1(k) . m1)) + (- r1) by RLVECT_1:def 10
.= (- r1) - (H1(k) . m1) ;
then - r1 = H1(k) . m by VECTSP_1:19;
then - r1i = H1(k) . m by COMPLFLD:2;
hence S4[m] ; :: thesis: verum
end;
end;
end;
A71: for i being Nat holds S4[i] from consider r being FinSequence of the carrier of F_Complex such that
A72: len r = 0 + 1 and
A73: (unital_poly (F_Complex,k)) . 0 = Sum r and
A74: for l being Element of NAT st l in dom r holds
r . l = (p . (l -' 1)) * (H1(k) . ((0 + 1) -' l)) by ;
A75: 1 in dom r by ;
then reconsider r1 = r . 1 as Element of the carrier of F_Complex by FINSEQ_2:11;
r = <*r1*> by ;
then A76: Sum r = r . 1 by RLVECT_1:44
.= (p . 0) * (H1(k) . 0) by ;
( H1(k) . 0 = 1 or H1(k) . 0 = - 1 )
proof
per cases ( p . 0 = 1 or p . 0 = - 1 ) by ;
suppose p . 0 = 1 ; :: thesis: ( H1(k) . 0 = 1 or H1(k) . 0 = - 1 )
hence ( H1(k) . 0 = 1 or H1(k) . 0 = - 1 ) by A1, A73, A76, Th38; :: thesis: verum
end;
suppose p . 0 = - 1 ; :: thesis: ( H1(k) . 0 = 1 or H1(k) . 0 = - 1 )
then - () = (- ()) * (H1(k) . 0) by A1, A73, A76, Th38
.= - (() * (H1(k) . 0)) by VECTSP_1:9
.= - (H1(k) . 0) ;
hence ( H1(k) . 0 = 1 or H1(k) . 0 = - 1 ) by ; :: thesis: verum
end;
end;
end;
hence S1[k] by A71; :: thesis: verum
end;
end;
end;
for d being non zero Element of NAT holds S1[d] from hence for d being non zero Element of NAT
for i being Element of NAT holds
( ( () . 0 = 1 or () . 0 = - 1 ) & () . i is integer ) ; :: thesis: verum