set cMGFC = the carrier of (MultGroup F_Complex );
set cPRFC = the carrier of (Polynom-Ring F_Complex );
let n, ni be non empty Element of NAT ; :: thesis:
assume that
A1: ni < n and
A2: ni divides n ; :: thesis:
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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { y where y is Element of the carrier of (MultGroup F_Complex ) : ( ord y divides n & not ord y divides ni & ord y <> n ) } ; :: thesis:
then ex y being Element of the carrier of (MultGroup F_Complex ) st
( x = y & ord y divides n & not ord y divides ni & ord y <> n ) ;
hence x in n -roots_of_1 by Th37; :: thesis:

end;

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 Th35;
set bp = rbp,1 -bag ;
defpred S₁[ set , set ] means ex d being non empty 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 ) );

A4: now

let i be Nat; :: thesis:
assume A5: i in Seg n ; :: thesis:
then A6: not i is empty by FINSEQ_1:3;

per cases ;

suppose A7: ( not i divides n or i divides ni or i = n ) ; :: thesis:

<%(1_ F_Complex )%> is Element of the carrier of (Polynom-Ring F_Complex ) by POLYNOM3:def 12;
hence ex x being Element of the carrier of (Polynom-Ring F_Complex ) st S₁[i,x] by A6, A7; :: thesis:

end;

suppose A8: ( i divides n & not i divides ni & i <> n ) ; :: thesis:

reconsider i9 = i as non empty Element of NAT by A5, FINSEQ_1:3;
cyclotomic_poly i9 is Element of the carrier of (Polynom-Ring F_Complex ) by POLYNOM3:def 12;
hence ex x being Element of the carrier of (Polynom-Ring F_Complex ) st S₁[i,x] by A8; :: thesis:

end;

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
S₁[i,f . i] from FINSEQ_1:sch 5(A4);

A11: now

let i be non empty Element of NAT ; :: thesis:
assume i in Seg n ; :: thesis:
then ex d being non empty Nat st
( i = d & ( ( not d divides n or d divides ni or d = n ) implies f . i = <%(1_ F_Complex )%> ) & ( 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 = <%(1_ F_Complex )%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ; :: thesis:

end;

then Product f = poly_with_roots (rbp,1 -bag ) by A9, Th57;
then reconsider p = Product f as Polynomial of F_Complex ;
take f ; :: thesis:
take p ; :: thesis:
thus p = Product f ; :: thesis:
thus dom f = Seg n by A9; :: thesis:
thus for i being non empty 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; :: thesis:
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

proof

assume (ni -roots_of_1 ) /\ rbn <> {} ; :: according to XBOOLE_0:def 7 :: thesis:
then consider x being set such that
A14: x in (ni -roots_of_1 ) /\ rbn by XBOOLE_0:def 1;
x in rbn by A14, XBOOLE_0:def 4;
then A15: ex y1 being Element of the carrier of (MultGroup F_Complex ) st
( x = y1 & ord y1 = n ) by A12;
x in ni -roots_of_1 by A14, XBOOLE_0:def 4;
then ex y being Element of the carrier of (MultGroup F_Complex ) st
( x = y & ord y divides ni ) by Th39;
hence contradiction by A1, A15, NAT_D:7; :: thesis:

end;

then A16: ((ni -roots_of_1 ),1 -bag ) + (rbn,1 -bag ) = ((ni -roots_of_1 ) \/ rbn),1 -bag by UPROOTS:12;
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, Th31;

now

let x be set ; :: thesis:

hereby :: thesis:

assume A18: x in n -roots_of_1 ; :: thesis:
then reconsider y = x as Element of the carrier of (MultGroup F_Complex ) by A3;
A19: ord y divides n by A18, Th37;

per cases ;

suppose ord y = n ; :: thesis:

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:

end;

suppose ( ord y <> n & not ord y divides ni ) ; :: thesis:

then y in rbp by A19;
hence x in rbibn \/ rbp by XBOOLE_0:def 3; :: thesis:

end;

suppose ( ord y <> n & ord y divides ni ) ; :: thesis:

then x in ni -roots_of_1 by Th37;
then x in rbibn by XBOOLE_0:def 3;
hence x in rbibn \/ rbp by XBOOLE_0:def 3; :: thesis:

end;

assume x in rbibn \/ rbp ; :: thesis:
then A20: ( x in rbibn or x in rbp ) by XBOOLE_0:def 3;

per cases by A20, XBOOLE_0:def 3;

suppose x in ni -roots_of_1 ; :: thesis:

hence x in n -roots_of_1 by A17; :: thesis:

end;

suppose x in rbn ; :: thesis:

then ex y being Element of the carrier of (MultGroup F_Complex ) st
( x = y & ord y = n ) by A12;
hence x in n -roots_of_1 by Th37; :: thesis:

end;

suppose x in rbp ; :: thesis:

then ex y being Element of the carrier of (MultGroup F_Complex ) st
( x = y & ord y divides n & not ord y divides ni & ord y <> n ) ;
hence x in n -roots_of_1 by Th37; :: thesis:

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 ((ni -roots_of_1 ),1 -bag ) by Th50;
rbibn misses rbp

proof

assume rbibn /\ rbp <> {} ; :: according to XBOOLE_0:def 7 :: thesis:
then consider x being set such that
A23: x in rbibn /\ rbp by XBOOLE_0:def 1;
x in rbp by A23, XBOOLE_0:def 4;
then A24: ex y being Element of the carrier of (MultGroup F_Complex ) st
( x = y & ord y divides n & not ord y divides ni & ord y <> n ) ;
A25: x in rbibn by A23, XBOOLE_0:def 4;

per cases by A25, XBOOLE_0:def 3;

suppose x in ni -roots_of_1 ; :: thesis:

then ex y being Element of the carrier of (MultGroup F_Complex ) st
( x = y & ord y divides ni ) by Th39;
hence contradiction by A24; :: thesis:

end;

suppose x in rbn ; :: thesis:

then ex y being Element of the carrier of (MultGroup F_Complex ) st
( x = y & ord y = n ) by A12;
hence contradiction by A24; :: thesis:

end;

then A26: (n -roots_of_1 ),1 -bag = (rbibn,1 -bag ) + (rbp,1 -bag ) by A21, UPROOTS:12;
unital_poly F_Complex ,n = poly_with_roots ((n -roots_of_1 ),1 -bag ) by Th50
.= (poly_with_roots (rbibn,1 -bag )) *' (poly_with_roots (rbp,1 -bag )) by A26, UPROOTS:66
.= ((unital_poly F_Complex ,ni) *' (cyclotomic_poly n)) *' (poly_with_roots (rbp,1 -bag )) by A13, A16, A22, UPROOTS:66 ;
hence unital_poly F_Complex ,n = ((unital_poly F_Complex ,ni) *' (cyclotomic_poly n)) *' p by A9, A11, Th57; :: thesis: