set cMGFC = the carrier of ;
set cPRFC = the carrier of ;
let n, ni be non zero Element of NAT ; :: thesis: ( ni < n & ni divides n implies ex f being FinSequence of the carrier of 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 = ) & ( 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)) *' ()) *' p ) )

assume that
A1: ni < n and
A2: ni divides n ; :: thesis: ex f being FinSequence of the carrier of 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 = ) & ( 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)) *' ()) *' p )

set rbp = { y where y is Element of the carrier of : ( ord y divides n & not ord y divides ni & ord y <> n ) } ;
{ y where y is Element of the carrier of : ( ord y divides n & not ord y divides ni & ord y <> n ) } c= n -roots_of_1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { y where y is Element of the carrier of : ( ord y divides n & not ord y divides ni & ord y <> n ) } or x in n -roots_of_1 )
assume x in { y where y is Element of the carrier of : ( ord y divides n & not ord y divides ni & ord y <> n ) } ; :: thesis:
then ex y being Element of the carrier of st
( x = y & ord y divides n & not ord y divides ni & ord y <> n ) ;
hence x in n -roots_of_1 by Th34; :: thesis: verum
end;
then reconsider rbp = { y where y is Element of the carrier of : ( 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 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 = ) & ( d divides n & not d divides ni & d <> n implies \$2 = cyclotomic_poly d ) );
A4: now :: thesis: for i being Nat st i in Seg n holds
ex x being Element of the carrier of st S1[i,x]
let i be Nat; :: thesis: ( i in Seg n implies ex x being Element of the carrier of st S1[x,b2] )
assume A5: i in Seg n ; :: thesis: ex x being Element of the carrier of st S1[x,b2]
then A6: not i is zero by FINSEQ_1:1;
per cases ( not i divides n or i divides ni or i = n or ( i divides n & not i divides ni & i <> n ) ) ;
suppose A7: ( not i divides n or i divides ni or i = n ) ; :: thesis: ex x being Element of the carrier of st S1[x,b2]
<%()%> is Element of the carrier of by POLYNOM3:def 10;
hence ex x being Element of the carrier of st S1[i,x] by A6, A7; :: thesis: verum
end;
suppose A8: ( i divides n & not i divides ni & i <> n ) ; :: thesis: ex x being Element of the carrier of st S1[x,b2]
reconsider i9 = i as non zero Element of NAT by ;
cyclotomic_poly i9 is Element of the carrier of by POLYNOM3:def 10;
hence ex x being Element of the carrier of st S1[i,x] by A8; :: thesis: verum
end;
end;
end;
consider f being FinSequence of the carrier of such that
A9: dom f = Seg n and
A10: for i being Nat st i in Seg n holds
S1[i,f . i] from
A11: now :: thesis: 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 = ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) )
let i be non zero Element of NAT ; :: thesis: ( i in Seg n implies ( ( ( not i divides n or i divides ni or i = n ) implies f . i = ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) )
assume i in Seg n ; :: thesis: ( ( ( not i divides n or i divides ni or i = n ) implies f . i = ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) )
then ex d being non zero Nat st
( i = d & ( ( not d divides n or d divides ni or d = n ) implies f . i = ) & ( d divides n & not d divides ni & d <> n implies f . i = cyclotomic_poly d ) ) by A10;
hence ( ( ( not i divides n or i divides ni or i = n ) implies f . i = ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ; :: thesis: verum
end;
then Product f = poly_with_roots ((rbp,1) -bag) by ;
then reconsider p = Product f as Polynomial of F_Complex ;
take f ; :: thesis: 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 = ) & ( 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)) *' ()) *' p )

take p ; :: thesis: ( 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 = ) & ( 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)) *' ()) *' p )

thus p = Product f ; :: thesis: ( 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 = ) & ( 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)) *' ()) *' p )

thus dom f = Seg n by A9; :: thesis: ( ( 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 = ) & ( 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)) *' ()) *' 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 = ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) by A11; :: thesis: unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' ()) *' p
set b = ((),1) -bag ;
set bi = ((),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 : 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
proof
assume (ni -roots_of_1) /\ rbn <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider x being object such that
A14: x in () /\ rbn by XBOOLE_0:def 1;
x in rbn by ;
then A15: ex y1 being Element of the carrier of st
( x = y1 & ord y1 = n ) by A12;
x in ni -roots_of_1 by ;
then ex y being Element of the carrier of st
( x = y & ord y divides ni ) by Th36;
hence contradiction by A1, A15, NAT_D:7; :: thesis: verum
end;
then A16: (((ni -roots_of_1),1) -bag) + ((rbn,1) -bag) = ((() \/ rbn),1) -bag by UPROOTS:10;
set rbibn = () \/ rbn;
reconsider rbibn = () \/ rbn as finite Subset of F_Complex ;
A17: ni -roots_of_1 c= n -roots_of_1 by ;
now :: thesis: for x being object holds
( ( x in n -roots_of_1 implies x in rbibn \/ rbp ) & ( x in rbibn \/ rbp implies x in n -roots_of_1 ) )
let x be object ; :: thesis: ( ( x in n -roots_of_1 implies x in rbibn \/ rbp ) & ( x in rbibn \/ rbp implies b1 in n -roots_of_1 ) )
hereby :: thesis: ( x in rbibn \/ rbp implies b1 in n -roots_of_1 )
assume A18: x in n -roots_of_1 ; :: thesis: x in rbibn \/ rbp
then reconsider y = x as Element of the carrier of by A3;
A19: ord y divides n by ;
per cases ( ord y = n or ( ord y <> n & not ord y divides ni ) or ( ord y <> n & ord y divides ni ) ) ;
suppose ord y = n ; :: thesis: x in rbibn \/ rbp
then y in rbn by A12;
then y in rbibn by XBOOLE_0:def 3;
hence x in rbibn \/ rbp by XBOOLE_0:def 3; :: thesis: verum
end;
suppose ( ord y <> n & not ord y divides ni ) ; :: thesis: x in rbibn \/ rbp
then y in rbp by A19;
hence x in rbibn \/ rbp by XBOOLE_0:def 3; :: thesis: verum
end;
suppose ( ord y <> n & ord y divides ni ) ; :: thesis: x in rbibn \/ rbp
end;
end;
end;
assume x in rbibn \/ rbp ; :: thesis:
then A20: ( x in rbibn or x in rbp ) by XBOOLE_0:def 3;
per cases ( x in ni -roots_of_1 or x in rbn or x in rbp ) by ;
end;
end;
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 (((),1) -bag) by Th46;
rbibn misses rbp
proof
assume rbibn /\ rbp <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider x being object such that
A23: x in rbibn /\ rbp by XBOOLE_0:def 1;
x in rbp by ;
then A24: ex y being Element of the carrier of st
( x = y & ord y divides n & not ord y divides ni & ord y <> n ) ;
A25: x in rbibn by ;
per cases ( x in ni -roots_of_1 or x in rbn ) by ;
suppose x in rbn ; :: thesis: contradiction
then ex y being Element of the carrier of st
( x = y & ord y = n ) by A12;
hence contradiction by A24; :: thesis: verum
end;
end;
end;
then A26: ((n -roots_of_1),1) -bag = ((rbibn,1) -bag) + ((rbp,1) -bag) by ;
unital_poly (F_Complex,n) = poly_with_roots (((),1) -bag) by Th46
.= (poly_with_roots ((rbibn,1) -bag)) *' (poly_with_roots ((rbp,1) -bag)) by
.= ((unital_poly (F_Complex,ni)) *' ()) *' (poly_with_roots ((rbp,1) -bag)) by ;
hence unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' ()) *' p by ; :: thesis: verum