set cMGFC = the carrier of (MultGroup F_Complex);
set cPRFC = the carrier of (Polynom-Ring F_Complex);
let n, ni be non zero Element of NAT ; for f being FinSequence of the carrier of (Polynom-Ring F_Complex)
for s being finite Subset of F_Complex st s = { y where y is Element of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } & dom f = Seg n & ( for i being non zero Element of NAT st i in dom f holds
( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) holds
Product f = poly_with_roots ((s,1) -bag)
let f be FinSequence of the carrier of (Polynom-Ring F_Complex); for s being finite Subset of F_Complex st s = { y where y is Element of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } & dom f = Seg n & ( for i being non zero Element of NAT st i in dom f holds
( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) holds
Product f = poly_with_roots ((s,1) -bag)
let s be finite Subset of F_Complex; ( s = { y where y is Element of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } & dom f = Seg n & ( for i being non zero Element of NAT st i in dom f holds
( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) implies Product f = poly_with_roots ((s,1) -bag) )
assume that
A1:
s = { y where y is Element of the carrier of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) }
and
A2:
dom f = Seg n
and
A3:
for i being non zero Element of NAT st i in dom f holds
( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) )
; Product f = poly_with_roots ((s,1) -bag)
deffunc H1( Nat) -> set = { y where y is Element of the carrier of (MultGroup F_Complex) : ( y in s & ord y <= $1 ) } ;
then reconsider sB = H1(n) as finite Subset of F_Complex ;
A5:
len f = n
by A2, FINSEQ_1:def 3;
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;
consider F being FinSequence of the carrier of (Polynom-Ring F_Complex) such that
dom F = Seg (len f)
and
A7:
for i being Nat st i in Seg (len f) holds
S1[i,F . i]
from FINSEQ_1:sch 5(A6);
defpred S2[ Nat] means ex t being finite Subset of F_Complex st
( t = H1($1) & F . $1 = poly_with_roots ((t,1) -bag) );
A8:
for i being Element of NAT st 1 <= i & i < len f & S2[i] holds
S2[i + 1]
proof
let i be
Element of
NAT ;
( 1 <= i & i < len f & S2[i] implies S2[i + 1] )
assume that A9:
1
<= i
and A10:
i < len f
and A11:
S2[
i]
;
S2[i + 1]
reconsider fi =
f | (Seg i) as
FinSequence of the
carrier of
(Polynom-Ring F_Complex) by FINSEQ_1:18;
i in Seg (len f)
by A9, A10, FINSEQ_1:1;
then A12:
F . i = Product fi
by A7;
reconsider fi1 =
f | (Seg (i + 1)) as
FinSequence of the
carrier of
(Polynom-Ring F_Complex) by FINSEQ_1:18;
A13:
i + 1
<= len f
by A10, NAT_1:13;
then
i + 1
= min (
(i + 1),
(len f))
by XXREAL_0:def 9;
then A14:
len fi1 = i + 1
by FINSEQ_2:21;
i + 1
in NAT
by ORDINAL1:def 12;
then reconsider sB =
H1(
i + 1) as
finite Subset of
F_Complex by A4;
take
sB
;
( sB = H1(i + 1) & F . (i + 1) = poly_with_roots ((sB,1) -bag) )
thus
sB = H1(
i + 1)
;
F . (i + 1) = poly_with_roots ((sB,1) -bag)
set B = (
sB,1)
-bag ;
consider sb being
finite Subset of
F_Complex such that A15:
sb = H1(
i)
and A16:
F . i = poly_with_roots ((sb,1) -bag)
by A11;
1
<= i + 1
by A9, NAT_1:13;
then A17:
i + 1
in Seg (len f)
by A13, FINSEQ_1:1;
then A18:
i + 1
in dom f
by FINSEQ_1:def 3;
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 A18, FINSEQ_2:11;
reconsider fi1d1p =
fi1d1 as
Polynomial of
F_Complex by POLYNOM3:def 10;
A20:
F . (i + 1) = Product fi1
by A7, A17;
set b = (
sb,1)
-bag ;
fi = fi1 | (Seg i)
by Lm2, NAT_1:12;
then
fi1 = fi ^ <*fi1d1*>
by A14, FINSEQ_3:55;
then
Product fi1 = (Product fi) * fi1d1
by GROUP_4:6;
then A21:
Product fi1 = (poly_with_roots ((sb,1) -bag)) *' fi1d1p
by A12, A16, POLYNOM3:def 10;
per cases
( not i + 1 divides n or i + 1 divides ni or i + 1 = n or ( i + 1 divides n & not i + 1 divides ni & i + 1 <> n ) )
;
suppose A29:
(
i + 1
divides n & not
i + 1
divides ni &
i + 1
<> n )
;
F . (i + 1) = poly_with_roots ((sB,1) -bag)consider scb being non
empty finite Subset of
F_Complex such that A30:
scb = { y where y is Element of the carrier of (MultGroup F_Complex) : ord y = i + 1 }
and A31:
cyclotomic_poly (i + 1) = poly_with_roots ((scb,1) -bag)
by Def5;
now for x being object holds
( ( x in sB implies x in sb \/ scb ) & ( x in sb \/ scb implies x in sB ) )let x be
object ;
( ( x in sB implies x in sb \/ scb ) & ( x in sb \/ scb implies b1 in sB ) )hereby ( x in sb \/ scb implies b1 in sB )
end; assume A35:
x in sb \/ scb
;
b1 in sB end; then A40:
sB = sb \/ scb
by TARSKI:2;
set cb = (
scb,1)
-bag ;
A41:
sb misses scb
f . (i + 1) = poly_with_roots ((scb,1) -bag)
by A3, A18, A29, A31;
then F . (i + 1) =
(poly_with_roots ((sb,1) -bag)) *' (poly_with_roots ((scb,1) -bag))
by A7, A17, A19, A21
.=
poly_with_roots (((sb,1) -bag) + ((scb,1) -bag))
by UPROOTS:64
.=
poly_with_roots ((sB,1) -bag)
by A40, A41, UPROOTS:10
;
hence
F . (i + 1) = poly_with_roots ((sB,1) -bag)
;
verum end;
end;
now for x being object holds
( ( x in s implies x in sB ) & ( x in sB implies x in s ) )end;
then A47:
s = sB
by TARSKI:2;
A48:
0 + 1 <= n
by NAT_1:13;
A49:
S2[1]
proof
reconsider t =
H1(1) as
finite Subset of
F_Complex by A4;
take
t
;
( t = H1(1) & F . 1 = poly_with_roots ((t,1) -bag) )
thus
t = H1(1)
;
F . 1 = poly_with_roots ((t,1) -bag)
reconsider f1 =
f | (Seg 1) as
FinSequence of the
carrier of
(Polynom-Ring F_Complex) by FINSEQ_1:18;
A50:
1
in dom f
by A5, A48, FINSEQ_3:25;
A51:
1
divides ni
by NAT_D:6;
then A58:
(
t,1)
-bag = EmptyBag the
carrier of
F_Complex
by UPROOTS:9;
A59:
1
in Seg (len f)
by A5, A48, FINSEQ_1:1;
then
1
in dom f
by FINSEQ_1:def 3;
then reconsider fd1 =
f . 1 as
Element of the
carrier of
(Polynom-Ring F_Complex) by FINSEQ_2:11;
f1 = <*(f . 1)*>
by A5, A48, Th1;
then F . 1 =
Product <*fd1*>
by A7, A59
.=
fd1
by FINSOP_1:11
.=
<%(1_ F_Complex)%>
by A3, A50, A51
;
hence
F . 1
= poly_with_roots ((t,1) -bag)
by A58, UPROOTS:60;
verum
end;
for i being Element of NAT st 1 <= i & i <= len f holds
S2[i]
from INT_1:sch 7(A49, A8);
then
( f = f | (Seg (len f)) & ex S being finite Subset of F_Complex st
( S = H1( len f) & F . (len f) = poly_with_roots ((S,1) -bag) ) )
by A5, A48, FINSEQ_3:49;
hence
Product f = poly_with_roots ((s,1) -bag)
by A5, A7, A47, FINSEQ_1:3; verum