A1: 1_. F_Complex =
(1_ F_Complex) * (1_. F_Complex)
by POLYNOM5:27

.= <%(1_ F_Complex)%> by POLYNOM5:29 ;

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 zero 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 zero 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 zero 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 zero 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 zero 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:8, POLYNOM4:18;

.= <%(1_ F_Complex)%> by POLYNOM5:29 ;

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 zero 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 zero 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 zero 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 zero 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 zero 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:8, POLYNOM4:18;

per cases
( len f = 0 or 0 < len f )
;

end;

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:8

.= 1. (Polynom-Ring F_Complex) ;

hence eval (p,c) is integer by A5, POLYNOM3:def 10; :: thesis: verum

end;then p = 1_ (Polynom-Ring F_Complex) by A2, GROUP_4:8

.= 1. (Polynom-Ring F_Complex) ;

hence eval (p,c) is integer by A5, POLYNOM3:def 10; :: thesis: verum

suppose A6:
0 < len f
; :: thesis: eval (p,c) is integer

defpred S_{1}[ 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:49;

dom F = Seg (len f) and

A9: for i being Nat st i in Seg (len f) holds

S_{1}[i,F . i]
from FINSEQ_1:sch 5(A8);

defpred S_{2}[ Nat] means ex r being Polynomial of F_Complex st

( r = F . $1 & eval (r,c) is integer );

then A22: 1 in Seg (len f) by FINSEQ_1:1;

A23: S_{2}[1]

S_{2}[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:3; :: thesis: verum

end;$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 (Polynom-Ring F_Complex) st S_{1}[i,x]

consider F being FinSequence of the carrier of (Polynom-Ring F_Complex) such that ex x being Element of the carrier of (Polynom-Ring F_Complex) st S

let i be Nat; :: thesis: ( i in Seg (len f) implies ex x being Element of the carrier of (Polynom-Ring F_Complex) st S_{1}[i,x] )

assume i in Seg (len f) ; :: thesis: ex x being Element of the carrier of (Polynom-Ring F_Complex) st S_{1}[i,x]

reconsider fi = f | (Seg i) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;

set x = Product fi;

take x = Product fi; :: thesis: S_{1}[i,x]

thus S_{1}[i,x]
; :: thesis: verum

end;assume i in Seg (len f) ; :: thesis: ex x being Element of the carrier of (Polynom-Ring F_Complex) st S

reconsider fi = f | (Seg i) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;

set x = Product fi;

take x = Product fi; :: thesis: S

thus S

dom F = Seg (len f) and

A9: for i being Nat st i in Seg (len f) holds

S

defpred S

( r = F . $1 & eval (r,c) is integer );

A10: now :: thesis: for i being Element of NAT st 1 <= i & i < len f & S_{2}[i] holds

S_{2}[i + 1]

A21:
0 + 1 <= len f
by A6, NAT_1:13;S

let i be Element of NAT ; :: thesis: ( 1 <= i & i < len f & S_{2}[i] implies S_{2}[i + 1] )

assume that

A11: 1 <= i and

A12: i < len f ; :: thesis: ( S_{2}[i] implies S_{2}[i + 1] )

A13: i in Seg (len f) by A11, A12, FINSEQ_1:1;

reconsider fi1 = f | (Seg (i + 1)) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;

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:21;

1 <= i + 1 by A11, NAT_1:13;

then A16: i + 1 in Seg (len f) by A14, FINSEQ_1:1;

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:18;

assume A18: S_{2}[i]
; :: thesis: S_{2}[i + 1]

A19: (f | (Seg (i + 1))) . (i + 1) = f . (i + 1) by FINSEQ_1:4, FUNCT_1:49;

then reconsider fi1d1 = fi1 . (i + 1) as Element of the carrier of (Polynom-Ring F_Complex) by A17, FINSEQ_2:11;

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 Lm2, NAT_1:12;

then fi1 = fi ^ <*fi1d1*> by A15, FINSEQ_3:55;

then A20: Product fi1 = (Product fi) * fi1d1 by GROUP_4:6;

thus S_{2}[i + 1]
:: thesis: verum

end;assume that

A11: 1 <= i and

A12: i < len f ; :: thesis: ( S

A13: i in Seg (len f) by A11, A12, FINSEQ_1:1;

reconsider fi1 = f | (Seg (i + 1)) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;

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:21;

1 <= i + 1 by A11, NAT_1:13;

then A16: i + 1 in Seg (len f) by A14, FINSEQ_1:1;

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:18;

assume A18: S

A19: (f | (Seg (i + 1))) . (i + 1) = f . (i + 1) by FINSEQ_1:4, FUNCT_1:49;

then reconsider fi1d1 = fi1 . (i + 1) as Element of the carrier of (Polynom-Ring F_Complex) by A17, FINSEQ_2:11;

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 Lm2, NAT_1:12;

then fi1 = fi ^ <*fi1d1*> by A15, FINSEQ_3:55;

then A20: Product fi1 = (Product fi) * fi1d1 by GROUP_4:6;

thus S

proof

reconsider epfi = eval (pfi,c), efi1d1p = eval (fi1d1p,c) as Element of COMPLEX by COMPLFLD:def 1;

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 10;

then eval (pfi1,c) = (eval (pfi,c)) * (eval (fi1d1p,c)) by POLYNOM4:24

.= iepfi * iefi1d1p ;

hence eval (pfi1,c) is integer ; :: thesis: verum

end;now :: thesis: eval (fi1d1p,c) is integer

then reconsider iefi1d1p = efi1d1p as Integer ;reconsider i1 = i + 1 as non zero Element of NAT by ORDINAL1:def 12;

end;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 10;

then eval (pfi1,c) = (eval (pfi,c)) * (eval (fi1d1p,c)) by POLYNOM4:24

.= iepfi * iefi1d1p ;

hence eval (pfi1,c) is integer ; :: thesis: verum

then A22: 1 in Seg (len f) by FINSEQ_1:1;

A23: S

proof

for i being Element of NAT st 1 <= i & i <= len f holds
reconsider f1 = f | (Seg 1) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;

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: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 A21, Th1;

hence fd1 = Product f1 by FINSOP_1:11

.= F . 1 by A9, A22 ;

:: thesis: eval (fd1,c) is integer

end;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: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 A21, Th1;

hence fd1 = Product f1 by FINSOP_1:11

.= F . 1 by A9, A22 ;

:: thesis: eval (fd1,c) is integer

S

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:3; :: thesis: verum