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