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 ; ( ni < n & ni divides n implies 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 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 ) ) ) & unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)) *' p ) )
assume that
A1:
ni < n
and
A2:
ni divides n
; 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 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 ) ) ) & unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)) *' p )
set rbp = { y where y is Element of the carrier of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } ;
{ y where y is Element of the carrier of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } c= n -roots_of_1
then reconsider rbp = { y where y is Element of the carrier of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } as finite Subset of F_Complex by XBOOLE_1:1;
A3:
n -roots_of_1 c= the carrier of (MultGroup F_Complex)
by Th32;
set bp = (rbp,1) -bag ;
defpred S1[ set , set ] means ex d being non zero Nat st
( $1 = d & ( ( not d divides n or d divides ni or d = n ) implies $2 = <%(1_ F_Complex)%> ) & ( d divides n & not d divides ni & d <> n implies $2 = cyclotomic_poly d ) );
consider f being FinSequence of the carrier of (Polynom-Ring F_Complex) such that
A9:
dom f = Seg n
and
A10:
for i being Nat st i in Seg n holds
S1[i,f . i]
from FINSEQ_1:sch 5(A4);
then
Product f = poly_with_roots ((rbp,1) -bag)
by A9, Th53;
then reconsider p = Product f as Polynomial of F_Complex ;
take
f
; 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 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 ) ) ) & unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)) *' p )
take
p
; ( 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 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 ) ) ) & unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)) *' p )
thus
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 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 ) ) ) & unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)) *' p )
thus
dom f = Seg n
by A9; ( ( for i being non zero Element of NAT st i in Seg n 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 ) ) ) & unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)) *' p )
thus
for i being non zero Element of NAT st i in Seg n 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 ) )
by A11; unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)) *' p
set b = ((n -roots_of_1),1) -bag ;
set bi = ((ni -roots_of_1),1) -bag ;
consider rbn being non empty finite Subset of F_Complex such that
A12:
rbn = { y where y is Element of the carrier of (MultGroup F_Complex) : ord y = n }
and
A13:
cyclotomic_poly n = poly_with_roots ((rbn,1) -bag)
by Def5;
set bn = (rbn,1) -bag ;
ni -roots_of_1 misses rbn
then A16:
(((ni -roots_of_1),1) -bag) + ((rbn,1) -bag) = (((ni -roots_of_1) \/ rbn),1) -bag
by UPROOTS:10;
set rbibn = (ni -roots_of_1) \/ rbn;
reconsider rbibn = (ni -roots_of_1) \/ rbn as finite Subset of F_Complex ;
A17:
ni -roots_of_1 c= n -roots_of_1
by A2, Th28;
then A21:
n -roots_of_1 = rbibn \/ rbp
by TARSKI:2;
set bibn = (rbibn,1) -bag ;
A22:
unital_poly (F_Complex,ni) = poly_with_roots (((ni -roots_of_1),1) -bag)
by Th46;
rbibn misses rbp
then A26:
((n -roots_of_1),1) -bag = ((rbibn,1) -bag) + ((rbp,1) -bag)
by A21, UPROOTS:10;
unital_poly (F_Complex,n) =
poly_with_roots (((n -roots_of_1),1) -bag)
by Th46
.=
(poly_with_roots ((rbibn,1) -bag)) *' (poly_with_roots ((rbp,1) -bag))
by A26, UPROOTS:64
.=
((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)) *' (poly_with_roots ((rbp,1) -bag))
by A13, A16, A22, UPROOTS:64
;
hence
unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)) *' p
by A9, A11, Th53; verum