A1: 1_. F_Complex =
(1_ F_Complex) * (1_. F_Complex)
by POLYNOM5:27
.=
<%(1_ F_Complex)%>
by POLYNOM5:29
;
let i be Integer; 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; 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); 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; ( 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 )
; 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 )
;
suppose A6:
0 < len f
;
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:49;
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[
Nat]
means ex
r being
Polynomial of
F_Complex st
(
r = F . $1 &
eval (
r,
c) is
integer );
A10:
now for i being Element of NAT st 1 <= i & i < len f & S2[i] holds
S2[i + 1]let i be
Element of
NAT ;
( 1 <= i & i < len f & S2[i] implies S2[i + 1] )assume that A11:
1
<= i
and A12:
i < len f
;
( S2[i] implies S2[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:
S2[
i]
;
S2[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
S2[
i + 1]
verumproof
reconsider epfi =
eval (
pfi,
c),
efi1d1p =
eval (
fi1d1p,
c) as
Element of
COMPLEX by COMPLFLD:def 1;
then reconsider iefi1d1p =
efi1d1p as
Integer ;
reconsider iepfi =
epfi as
Integer by A9, A18, A13;
take
pfi1
;
( pfi1 = F . (i + 1) & eval (pfi1,c) is integer )
thus
pfi1 = F . (i + 1)
by A9, A16;
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
;
verum
end; end; A21:
0 + 1
<= len f
by A6, NAT_1:13;
then A22:
1
in Seg (len f)
by FINSEQ_1:1;
A23:
S2[1]
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:3;
verum end; end;