A1: 1_. F_Complex = () * () by POLYNOM5:27
.= by POLYNOM5:29 ;
let i be Integer; :: thesis: for c being Element of F_Complex
for f being FinSequence of the carrier of
for p being Polynomial of F_Complex st p = Product f & c = i & ( for i being non zero Element of NAT holds
( not i in dom f or f . i = or f . i = cyclotomic_poly i ) ) holds
eval (p,c) is integer

let c be Element of F_Complex; :: thesis: for f being FinSequence of the carrier of
for p being Polynomial of F_Complex st p = Product f & c = i & ( for i being non zero Element of NAT holds
( not i in dom f or f . i = or f . i = cyclotomic_poly i ) ) holds
eval (p,c) is integer

let f be FinSequence of the carrier of ; :: thesis: for p being Polynomial of F_Complex st p = Product f & c = i & ( for i being non zero Element of NAT holds
( not i in dom f or f . i = or f . i = cyclotomic_poly i ) ) holds
eval (p,c) is integer

let p be Polynomial of F_Complex; :: thesis: ( p = Product f & c = i & ( for i being non zero Element of NAT holds
( not i in dom f or f . i = or f . i = cyclotomic_poly i ) ) implies eval (p,c) is integer )

assume that
A2: p = Product f and
A3: c = i and
A4: for i being non zero Element of NAT holds
( not i in dom f or f . i = or f . i = cyclotomic_poly i ) ; :: thesis: eval (p,c) is integer
A5: eval ((),c) = 1 by ;
per cases ( len f = 0 or 0 < len f ) ;
suppose len f = 0 ; :: thesis: eval (p,c) is integer
then f = <*> the carrier of ;
then p = 1_ by
.= 1. ;
hence eval (p,c) is integer by ; :: thesis: verum
end;
suppose A6: 0 < len f ; :: thesis: eval (p,c) is integer
defpred S1[ Nat, set ] means for fi being FinSequence of the carrier of st fi = f | (Seg \$1) holds
\$2 = Product fi;
A7: f = f | (Seg (len f)) by FINSEQ_3:49;
A8: now :: thesis: for i being Nat st i in Seg (len f) holds
ex x being Element of the carrier of st S1[i,x]
let i be Nat; :: thesis: ( i in Seg (len f) implies ex x being Element of the carrier of st S1[i,x] )
assume i in Seg (len f) ; :: thesis: ex x being Element of the carrier of st S1[i,x]
reconsider fi = f | (Seg i) as FinSequence of the carrier of by FINSEQ_1:18;
set x = Product fi;
take x = Product fi; :: thesis: S1[i,x]
thus S1[i,x] ; :: thesis: verum
end;
consider F being FinSequence of the carrier of such that
dom F = Seg (len f) and
A9: for i being Nat st i in Seg (len f) holds
S1[i,F . i] from defpred S2[ Nat] means ex r being Polynomial of F_Complex st
( r = F . \$1 & eval (r,c) is integer );
A10: now :: thesis: for i being Element of NAT st 1 <= i & i < len f & S2[i] holds
S2[i + 1]
let i be Element of NAT ; :: thesis: ( 1 <= i & i < len f & S2[i] implies S2[i + 1] )
assume that
A11: 1 <= i and
A12: i < len f ; :: thesis: ( S2[i] implies S2[i + 1] )
A13: i in Seg (len f) by ;
reconsider fi1 = f | (Seg (i + 1)) as FinSequence of the carrier of by FINSEQ_1:18;
A14: i + 1 <= len f by ;
then i + 1 = min ((i + 1),(len f)) by XXREAL_0:def 9;
then A15: len fi1 = i + 1 by FINSEQ_2:21;
1 <= i + 1 by ;
then A16: i + 1 in Seg (len f) by ;
then A17: i + 1 in dom f by FINSEQ_1:def 3;
reconsider fi = f | (Seg i) as FinSequence of the carrier of by FINSEQ_1:18;
assume A18: S2[i] ; :: thesis: S2[i + 1]
A19: (f | (Seg (i + 1))) . (i + 1) = f . (i + 1) by ;
then reconsider fi1d1 = fi1 . (i + 1) as Element of the carrier of by ;
reconsider pfi1 = Product fi1, pfi = Product fi as Polynomial of F_Complex by POLYNOM3:def 10;
reconsider fi1d1p = fi1d1 as Polynomial of F_Complex by POLYNOM3:def 10;
fi = fi1 | (Seg i) by ;
then fi1 = fi ^ <*fi1d1*> by ;
then A20: Product fi1 = (Product fi) * fi1d1 by GROUP_4:6;
thus S2[i + 1] :: thesis: verum
proof
reconsider epfi = eval (pfi,c), efi1d1p = eval (fi1d1p,c) as Element of COMPLEX by COMPLFLD:def 1;
now :: thesis: eval (fi1d1p,c) is integer
reconsider i1 = i + 1 as non zero Element of NAT by ORDINAL1:def 12;
per cases ( f . i1 = or f . i1 = cyclotomic_poly i1 ) by ;
suppose f . i1 = ; :: thesis: eval (fi1d1p,c) is integer
hence eval (fi1d1p,c) is integer by ; :: thesis: verum
end;
suppose f . i1 = cyclotomic_poly i1 ; :: thesis: eval (fi1d1p,c) is integer
hence eval (fi1d1p,c) is integer by ; :: thesis: verum
end;
end;
end;
then reconsider iefi1d1p = efi1d1p as Integer ;
reconsider iepfi = epfi as Integer by A9, A18, A13;
take pfi1 ; :: thesis: ( pfi1 = F . (i + 1) & eval (pfi1,c) is integer )
thus pfi1 = F . (i + 1) by ; :: thesis: eval (pfi1,c) is integer
pfi1 = pfi *' fi1d1p by ;
then eval (pfi1,c) = (eval (pfi,c)) * (eval (fi1d1p,c)) by POLYNOM4:24
.= iepfi * iefi1d1p ;
hence eval (pfi1,c) is integer ; :: thesis: verum
end;
end;
A21: 0 + 1 <= len f by ;
then A22: 1 in Seg (len f) by FINSEQ_1:1;
A23: S2
proof
reconsider f1 = f | (Seg 1) as FinSequence of the carrier of by FINSEQ_1:18;
A24: 1 in dom f by ;
then reconsider fd1 = f . 1 as Element of the carrier of by FINSEQ_2:11;
reconsider fd1 = fd1 as Polynomial of F_Complex by POLYNOM3:def 10;
take fd1 ; :: thesis: ( fd1 = F . 1 & eval (fd1,c) is integer )
f1 = <*(f . 1)*> by ;
hence fd1 = Product f1 by FINSOP_1:11
.= F . 1 by ;
:: thesis: eval (fd1,c) is integer
per cases ( f . 1 = or f . 1 = cyclotomic_poly 1 ) by ;
suppose f . 1 = ; :: thesis: eval (fd1,c) is integer
hence eval (fd1,c) is integer by ; :: thesis: verum
end;
suppose f . 1 = cyclotomic_poly 1 ; :: thesis: eval (fd1,c) is integer
hence eval (fd1,c) is integer by ; :: thesis: verum
end;
end;
end;
for i being Element of NAT st 1 <= i & i <= len f holds
S2[i] from then ex r being Polynomial of F_Complex st
( r = F . (len f) & eval (r,c) is integer ) by A21;
hence eval (p,c) is integer by ; :: thesis: verum
end;
end;