let i be Integer; :: thesis: for c being Element of F_Complex
for f being FinSequence of the carrier of (Polynom-Ring F_Complex )
for p being Polynomial of F_Complex st p = Product f & c = i & ( for i being non empty Element of NAT holds
( not i in dom f or f . i = <%(1_ F_Complex )%> 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 (Polynom-Ring F_Complex )
for p being Polynomial of F_Complex st p = Product f & c = i & ( for i being non empty Element of NAT holds
( not i in dom f or f . i = <%(1_ F_Complex )%> or f . i = cyclotomic_poly i ) ) holds
eval p,c is integer
let f be FinSequence of the carrier of (Polynom-Ring F_Complex ); :: thesis: for p being Polynomial of F_Complex st p = Product f & c = i & ( for i being non empty Element of NAT holds
( not i in dom f or f . i = <%(1_ F_Complex )%> 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 empty Element of NAT holds
( not i in dom f or f . i = <%(1_ F_Complex )%> or f . i = cyclotomic_poly i ) ) implies eval p,c is integer )
assume that
A1: p = Product f and
A2: c = i and
A3: for i being non empty Element of NAT holds
( not i in dom f or f . i = <%(1_ F_Complex )%> or f . i = cyclotomic_poly i ) ; :: thesis: eval p,c is integer
A4: eval (1_. F_Complex ),c = 1 by COMPLFLD:10, POLYNOM4:21;
A5: 1_. F_Complex = (1_ F_Complex ) * (1_. F_Complex ) by POLYNOM5:28
.= <%(1_ F_Complex )%> by POLYNOM5:30 ;
per cases ( len f = 0 or 0 < len f ) ;
suppose len f = 0 ; :: thesis: eval p,c is integer
then f = <*> the carrier of (Polynom-Ring F_Complex ) ;
then p = 1_ (Polynom-Ring F_Complex ) by A1, GROUP_4:11
.= 1. (Polynom-Ring F_Complex ) ;
hence eval p,c is integer by A4, POLYNOM3:def 12; :: thesis: verum
end;
suppose A6: 0 < len f ; :: thesis: eval p,c is integer
then A7: 0 + 1 <= len f by NAT_1:13;
defpred S1[ Nat, set ] means for fi being FinSequence of the carrier of (Polynom-Ring F_Complex ) st fi = f | (Seg $1) holds
$2 = Product fi;
A8: now
let i be Nat; :: thesis: ( i in Seg (len f) implies ex x being Element of the carrier of (Polynom-Ring F_Complex ) st S1[i,x] )
assume i in Seg (len f) ; :: thesis: ex x being Element of the carrier of (Polynom-Ring F_Complex ) st S1[i,x]
reconsider fi = f | (Seg i) as FinSequence of the carrier of (Polynom-Ring F_Complex ) by FINSEQ_1:23;
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 (Polynom-Ring F_Complex ) 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 FINSEQ_1:sch 5(A8);
A10: 1 in Seg (len f) by A7, FINSEQ_1:3;
defpred S2[ Element of NAT ] means ex r being Polynomial of F_Complex st
( r = F . $1 & eval r,c is integer );
A11: S2[1]
proof
reconsider f1 = f | (Seg 1) as FinSequence of the carrier of (Polynom-Ring F_Complex ) by FINSEQ_1:23;
A12: f1 = <*(f . 1)*> by A7, Th2;
A13: 1 in dom f by A10, FINSEQ_1:def 3;
then reconsider fd1 = f . 1 as Element of the carrier of (Polynom-Ring F_Complex ) by FINSEQ_2:13;
reconsider fd1 = fd1 as Polynomial of F_Complex by POLYNOM3:def 12;
take fd1 ; :: thesis: ( fd1 = F . 1 & eval fd1,c is integer )
thus fd1 = Product f1 by A12, FINSOP_1:12
.= F . 1 by A9, A10 ; :: thesis: eval fd1,c is integer
end;
A14: now
let i be Element of NAT ; :: thesis: ( 1 <= i & i < len f & S2[i] implies S2[i + 1] )
assume that
A15: 1 <= i and
A16: i < len f ; :: thesis: ( S2[i] implies S2[i + 1] )
assume S2[i] ; :: thesis: S2[i + 1]
then consider r being Polynomial of F_Complex such that
A17: r = F . i and
A18: eval r,c is integer ;
A19: i in Seg (len f) by A15, A16, FINSEQ_1:3;
A20: ( 1 <= i + 1 & i + 1 <= len f ) by A15, A16, NAT_1:13;
then A21: i + 1 in Seg (len f) by FINSEQ_1:3;
then A22: i + 1 in dom f by FINSEQ_1:def 3;
reconsider fi = f | (Seg i) as FinSequence of the carrier of (Polynom-Ring F_Complex ) by FINSEQ_1:23;
reconsider fi1 = f | (Seg (i + 1)) as FinSequence of the carrier of (Polynom-Ring F_Complex ) by FINSEQ_1:23;
A23: fi = fi1 | (Seg i) by Lm2, NAT_1:12;
i + 1 = min (i + 1),(len f) by A20, XXREAL_0:def 9;
then A24: len fi1 = i + 1 by FINSEQ_2:24;
A25: (f | (Seg (i + 1))) . (i + 1) = f . (i + 1) by FINSEQ_1:6, FUNCT_1:72;
then reconsider fi1d1 = fi1 . (i + 1) as Element of the carrier of (Polynom-Ring F_Complex ) by A22, FINSEQ_2:13;
reconsider fi1d1p = fi1d1 as Polynomial of F_Complex by POLYNOM3:def 12;
fi1 = fi ^ <*fi1d1*> by A23, A24, FINSEQ_3:61;
then A26: Product fi1 = (Product fi) * fi1d1 by GROUP_4:9;
reconsider pfi1 = Product fi1, pfi = Product fi as Polynomial of F_Complex by POLYNOM3:def 12;
thus S2[i + 1] :: thesis: verum
proof
take pfi1 ; :: thesis: ( pfi1 = F . (i + 1) & eval pfi1,c is integer )
thus pfi1 = F . (i + 1) by A9, A21; :: thesis: eval pfi1,c is integer
reconsider epfi = eval pfi,c, efi1d1p = eval fi1d1p,c as Element of COMPLEX by COMPLFLD:def 1;
reconsider iepfi = epfi as Integer by A9, A17, A18, A19;
now
reconsider i1 = i + 1 as non empty Element of NAT ;
per cases ( f . i1 = <%(1_ F_Complex )%> or f . i1 = cyclotomic_poly i1 ) by A3, A22;
suppose f . i1 = cyclotomic_poly i1 ; :: thesis: eval fi1d1p,c is integer
hence eval fi1d1p,c is integer by A2, A25, Th56; :: thesis: verum
end;
end;
end;
then reconsider iefi1d1p = efi1d1p as Integer ;
pfi1 = pfi *' fi1d1p by A26, POLYNOM3:def 12;
then eval pfi1,c = (eval pfi,c) * (eval fi1d1p,c) by POLYNOM4:27
.= iepfi * iefi1d1p ;
hence eval pfi1,c is integer ; :: thesis: verum
end;
end;
for i being Element of NAT st 1 <= i & i <= len f holds
S2[i] from POLYNOM2:sch 4(A11, A14);
then consider r being Polynomial of F_Complex such that
A27: r = F . (len f) and
A28: eval r,c is integer by A7;
f = f | (Seg (len f)) by FINSEQ_3:55;
hence eval p,c is integer by A1, A6, A9, A27, A28, FINSEQ_1:5; :: thesis: verum
end;
end;