set cPRFC = the carrier of (Polynom-Ring F_Complex);

let n be non zero Element of NAT ; :: thesis: ex f being FinSequence of the carrier of (Polynom-Ring F_Complex) ex p being Polynomial of F_Complex st

( p = Product f & dom f = Seg n & ( for i being non zero Element of NAT st i in Seg n holds

( ( ( not i divides n or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies f . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = (cyclotomic_poly n) *' p )

defpred S_{1}[ set , set ] means ex i being non zero Element of NAT st

( i = $1 & ( not i divides n implies $2 = <%(1_ F_Complex)%> ) & ( i divides n implies $2 = cyclotomic_poly i ) );

consider m being Nat such that

A1: n = m + 1 by NAT_1:6;

A2: for k being Nat st k in Seg n holds

ex x being Element of the carrier of (Polynom-Ring F_Complex) st S_{1}[k,x]

A5: dom f = Seg n and

A6: for k being Nat st k in Seg n holds

S_{1}[k,f /. k]
from RECDEF_1:sch 17(A2);

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

A7: len f = n by A5, FINSEQ_1:def 3;

<*FC1*> is FinSequence of the carrier of (Polynom-Ring F_Complex) ;

then reconsider h = fm ^ <*<%(1_ F_Complex)%>*> as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:75;

reconsider p = Product h as Polynomial of F_Complex by POLYNOM3:def 10;

take h ; :: thesis: ex p being Polynomial of F_Complex st

( p = Product h & dom h = Seg n & ( for i being non zero Element of NAT st i in Seg n holds

( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = (cyclotomic_poly n) *' p )

take p ; :: thesis: ( p = Product h & dom h = Seg n & ( for i being non zero Element of NAT st i in Seg n holds

( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = (cyclotomic_poly n) *' p )

thus p = Product h ; :: thesis: ( dom h = Seg n & ( for i being non zero Element of NAT st i in Seg n holds

( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = (cyclotomic_poly n) *' p )

A11: m <= n by A1, NAT_1:13;

then A12: len fm = m by A7, FINSEQ_1:17;

reconsider cpn = cyclotomic_poly n as Element of the carrier of (Polynom-Ring F_Complex) by POLYNOM3:def 10;

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

1 <= n by NAT_1:53;

then A13: n in Seg n by FINSEQ_1:1;

then A14: f . n = cyclotomic_poly n by A5, A8;

len <*<%(1_ F_Complex)%>*> = 1 by FINSEQ_1:40;

hence dom h = Seg n by A1, A12, FINSEQ_1:def 7; :: thesis: ( ( for i being non zero Element of NAT st i in Seg n holds

( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = (cyclotomic_poly n) *' p )

A15: dom fm = Seg m by A7, A11, FINSEQ_1:17;

thus for i being non zero Element of NAT st i in Seg n holds

( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) :: thesis: unital_poly (F_Complex,n) = (cyclotomic_poly n) *' p

reconsider Pfm = Product fm as Polynomial of F_Complex by POLYNOM3:def 10;

A21: Product h = (Product fm) * p1 by GROUP_4:6

.= Pfm *' <%(1_ F_Complex)%> by POLYNOM3:def 10

.= Product fm by UPROOTS:32 ;

f = fn by A7, FINSEQ_2:20

.= fm ^ <*(cyclotomic_poly n)*> by A5, A1, A13, A14, FINSEQ_5:10 ;

then A22: Product f = (Product fm) * cpn by GROUP_4:6;

unital_poly (F_Complex,n) = Product f by A7, A8, Th49;

hence unital_poly (F_Complex,n) = (cyclotomic_poly n) *' p by A21, A22, POLYNOM3:def 10; :: thesis: verum

let n be non zero Element of NAT ; :: thesis: ex f being FinSequence of the carrier of (Polynom-Ring F_Complex) ex p being Polynomial of F_Complex st

( p = Product f & dom f = Seg n & ( for i being non zero Element of NAT st i in Seg n holds

( ( ( not i divides n or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies f . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = (cyclotomic_poly n) *' p )

defpred S

( i = $1 & ( not i divides n implies $2 = <%(1_ F_Complex)%> ) & ( i divides n implies $2 = cyclotomic_poly i ) );

consider m being Nat such that

A1: n = m + 1 by NAT_1:6;

A2: for k being Nat st k in Seg n holds

ex x being Element of the carrier of (Polynom-Ring F_Complex) st S

proof

consider f being FinSequence of the carrier of (Polynom-Ring F_Complex) such that
let k be Nat; :: thesis: ( k in Seg n implies ex x being Element of the carrier of (Polynom-Ring F_Complex) st S_{1}[k,x] )

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

then reconsider i = k as non zero Element of NAT by FINSEQ_1:1;

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

then reconsider i = k as non zero Element of NAT by FINSEQ_1:1;

per cases
( not i divides n or i divides n )
;

end;

suppose A3:
not i divides n
; :: thesis: ex x being Element of the carrier of (Polynom-Ring F_Complex) st S_{1}[k,x]

reconsider FC1 = <%(1_ F_Complex)%> as Element of the carrier of (Polynom-Ring F_Complex) by POLYNOM3:def 10;

take FC1 ; :: thesis: S_{1}[k,FC1]

take i ; :: thesis: ( i = k & ( not i divides n implies FC1 = <%(1_ F_Complex)%> ) & ( i divides n implies FC1 = cyclotomic_poly i ) )

thus i = k ; :: thesis: ( ( not i divides n implies FC1 = <%(1_ F_Complex)%> ) & ( i divides n implies FC1 = cyclotomic_poly i ) )

thus ( ( not i divides n implies FC1 = <%(1_ F_Complex)%> ) & ( i divides n implies FC1 = cyclotomic_poly i ) ) by A3; :: thesis: verum

end;take FC1 ; :: thesis: S

take i ; :: thesis: ( i = k & ( not i divides n implies FC1 = <%(1_ F_Complex)%> ) & ( i divides n implies FC1 = cyclotomic_poly i ) )

thus i = k ; :: thesis: ( ( not i divides n implies FC1 = <%(1_ F_Complex)%> ) & ( i divides n implies FC1 = cyclotomic_poly i ) )

thus ( ( not i divides n implies FC1 = <%(1_ F_Complex)%> ) & ( i divides n implies FC1 = cyclotomic_poly i ) ) by A3; :: thesis: verum

suppose A4:
i divides n
; :: thesis: ex x being Element of the carrier of (Polynom-Ring F_Complex) st S_{1}[k,x]

reconsider FC1 = cyclotomic_poly i as Element of the carrier of (Polynom-Ring F_Complex) by POLYNOM3:def 10;

take FC1 ; :: thesis: S_{1}[k,FC1]

take i ; :: thesis: ( i = k & ( not i divides n implies FC1 = <%(1_ F_Complex)%> ) & ( i divides n implies FC1 = cyclotomic_poly i ) )

thus i = k ; :: thesis: ( ( not i divides n implies FC1 = <%(1_ F_Complex)%> ) & ( i divides n implies FC1 = cyclotomic_poly i ) )

thus ( ( not i divides n implies FC1 = <%(1_ F_Complex)%> ) & ( i divides n implies FC1 = cyclotomic_poly i ) ) by A4; :: thesis: verum

end;take FC1 ; :: thesis: S

take i ; :: thesis: ( i = k & ( not i divides n implies FC1 = <%(1_ F_Complex)%> ) & ( i divides n implies FC1 = cyclotomic_poly i ) )

thus i = k ; :: thesis: ( ( not i divides n implies FC1 = <%(1_ F_Complex)%> ) & ( i divides n implies FC1 = cyclotomic_poly i ) )

thus ( ( not i divides n implies FC1 = <%(1_ F_Complex)%> ) & ( i divides n implies FC1 = cyclotomic_poly i ) ) by A4; :: thesis: verum

A5: dom f = Seg n and

A6: for k being Nat st k in Seg n holds

S

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

A7: len f = n by A5, FINSEQ_1:def 3;

A8: now :: thesis: for i being non zero Element of NAT st i in dom f holds

( ( not i divides n implies f . i = <%(1_ F_Complex)%> ) & ( i divides n implies f . i = cyclotomic_poly i ) )

reconsider FC1 = <%(1_ F_Complex)%> as Element of the carrier of (Polynom-Ring F_Complex) by POLYNOM3:def 10;( ( not i divides n implies f . i = <%(1_ F_Complex)%> ) & ( i divides n implies f . i = cyclotomic_poly i ) )

let i be non zero Element of NAT ; :: thesis: ( i in dom f implies ( ( not i divides n implies f . i = <%(1_ F_Complex)%> ) & ( i divides n implies f . i = cyclotomic_poly i ) ) )

assume A9: i in dom f ; :: thesis: ( ( not i divides n implies f . i = <%(1_ F_Complex)%> ) & ( i divides n implies f . i = cyclotomic_poly i ) )

then A10: i <= n by A5, FINSEQ_1:1;

( ex j being non zero Element of NAT st

( j = i & ( not j divides n implies f /. i = <%(1_ F_Complex)%> ) & ( j divides n implies f /. i = cyclotomic_poly j ) ) & 1 <= i ) by A5, A6, A9, FINSEQ_1:1;

hence ( ( not i divides n implies f . i = <%(1_ F_Complex)%> ) & ( i divides n implies f . i = cyclotomic_poly i ) ) by A7, A10, FINSEQ_4:15; :: thesis: verum

end;assume A9: i in dom f ; :: thesis: ( ( not i divides n implies f . i = <%(1_ F_Complex)%> ) & ( i divides n implies f . i = cyclotomic_poly i ) )

then A10: i <= n by A5, FINSEQ_1:1;

( ex j being non zero Element of NAT st

( j = i & ( not j divides n implies f /. i = <%(1_ F_Complex)%> ) & ( j divides n implies f /. i = cyclotomic_poly j ) ) & 1 <= i ) by A5, A6, A9, FINSEQ_1:1;

hence ( ( not i divides n implies f . i = <%(1_ F_Complex)%> ) & ( i divides n implies f . i = cyclotomic_poly i ) ) by A7, A10, FINSEQ_4:15; :: thesis: verum

<*FC1*> is FinSequence of the carrier of (Polynom-Ring F_Complex) ;

then reconsider h = fm ^ <*<%(1_ F_Complex)%>*> as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:75;

reconsider p = Product h as Polynomial of F_Complex by POLYNOM3:def 10;

take h ; :: thesis: ex p being Polynomial of F_Complex st

( p = Product h & dom h = Seg n & ( for i being non zero Element of NAT st i in Seg n holds

( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = (cyclotomic_poly n) *' p )

take p ; :: thesis: ( p = Product h & dom h = Seg n & ( for i being non zero Element of NAT st i in Seg n holds

( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = (cyclotomic_poly n) *' p )

thus p = Product h ; :: thesis: ( dom h = Seg n & ( for i being non zero Element of NAT st i in Seg n holds

( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = (cyclotomic_poly n) *' p )

A11: m <= n by A1, NAT_1:13;

then A12: len fm = m by A7, FINSEQ_1:17;

reconsider cpn = cyclotomic_poly n as Element of the carrier of (Polynom-Ring F_Complex) by POLYNOM3:def 10;

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

1 <= n by NAT_1:53;

then A13: n in Seg n by FINSEQ_1:1;

then A14: f . n = cyclotomic_poly n by A5, A8;

len <*<%(1_ F_Complex)%>*> = 1 by FINSEQ_1:40;

hence dom h = Seg n by A1, A12, FINSEQ_1:def 7; :: thesis: ( ( for i being non zero Element of NAT st i in Seg n holds

( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = (cyclotomic_poly n) *' p )

A15: dom fm = Seg m by A7, A11, FINSEQ_1:17;

thus for i being non zero Element of NAT st i in Seg n holds

( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) :: thesis: unital_poly (F_Complex,n) = (cyclotomic_poly n) *' p

proof

reconsider p1 = <%(1_ F_Complex)%> as Element of the carrier of (Polynom-Ring F_Complex) by POLYNOM3:def 10;
let i be non zero Element of NAT ; :: thesis: ( i in Seg n implies ( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) )

assume A16: i in Seg n ; :: thesis: ( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) )

end;assume A16: i in Seg n ; :: thesis: ( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) )

per cases
( i in Seg m or not i in Seg m )
;

end;

suppose A17:
i in Seg m
; :: thesis: ( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) )

then A18:
( fm . i = f . i & i <= m )
by FINSEQ_1:1, FUNCT_1:49;

h . i = fm . i by A15, A17, FINSEQ_1:def 7;

hence ( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) by A5, A1, A8, A16, A18, NAT_1:13; :: thesis: verum

end;h . i = fm . i by A15, A17, FINSEQ_1:def 7;

hence ( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) by A5, A1, A8, A16, A18, NAT_1:13; :: thesis: verum

suppose
not i in Seg m
; :: thesis: ( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) )

then
( not 1 <= i or not i <= m )
by FINSEQ_1:1;

then A19: n <= i by A1, A16, FINSEQ_1:1, NAT_1:13;

A20: i <= n by A16, FINSEQ_1:1;

1 in Seg 1 by FINSEQ_1:1;

then 1 in dom <*<%(1_ F_Complex)%>*> by FINSEQ_1:38;

then h . n = <*<%(1_ F_Complex)%>*> . 1 by A1, A12, FINSEQ_1:def 7

.= <%(1_ F_Complex)%> by FINSEQ_1:40 ;

hence ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) by A19, A20, XXREAL_0:1; :: thesis: ( i divides n & i <> n implies h . i = cyclotomic_poly i )

thus ( i divides n & i <> n implies h . i = cyclotomic_poly i ) by A19, A20, XXREAL_0:1; :: thesis: verum

end;then A19: n <= i by A1, A16, FINSEQ_1:1, NAT_1:13;

A20: i <= n by A16, FINSEQ_1:1;

1 in Seg 1 by FINSEQ_1:1;

then 1 in dom <*<%(1_ F_Complex)%>*> by FINSEQ_1:38;

then h . n = <*<%(1_ F_Complex)%>*> . 1 by A1, A12, FINSEQ_1:def 7

.= <%(1_ F_Complex)%> by FINSEQ_1:40 ;

hence ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) by A19, A20, XXREAL_0:1; :: thesis: ( i divides n & i <> n implies h . i = cyclotomic_poly i )

thus ( i divides n & i <> n implies h . i = cyclotomic_poly i ) by A19, A20, XXREAL_0:1; :: thesis: verum

reconsider Pfm = Product fm as Polynomial of F_Complex by POLYNOM3:def 10;

A21: Product h = (Product fm) * p1 by GROUP_4:6

.= Pfm *' <%(1_ F_Complex)%> by POLYNOM3:def 10

.= Product fm by UPROOTS:32 ;

f = fn by A7, FINSEQ_2:20

.= fm ^ <*(cyclotomic_poly n)*> by A5, A1, A13, A14, FINSEQ_5:10 ;

then A22: Product f = (Product fm) * cpn by GROUP_4:6;

unital_poly (F_Complex,n) = Product f by A7, A8, Th49;

hence unital_poly (F_Complex,n) = (cyclotomic_poly n) *' p by A21, A22, POLYNOM3:def 10; :: thesis: verum