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

A3: now

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

per cases ;

suppose A6: ( 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 A5, A6; :: thesis:

end;

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

reconsider i' = i as non empty Element of NAT by A4, FINSEQ_1:3;
cyclotomic_poly i' 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 A7; :: thesis:

end;

consider f being FinSequence of the carrier of (Polynom-Ring F_Complex ) such that
A8: dom f = Seg n and
A9: for i being Nat st i in Seg n holds
S₁[i,f . i] from FINSEQ_1:sch 5(A3);

A10: 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 A9;
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;

take f ; :: 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 ) } ;
A11: { 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;

A12: ni -roots_of_1 c= n -roots_of_1 by A2, Th31;
A13: n -roots_of_1 c= the carrier of (MultGroup F_Complex ) by Th35;
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 A11, XBOOLE_1:1;
set bp = rbp,1 -bag ;
Product f = poly_with_roots (rbp,1 -bag ) by A8, A10, Th57;
then reconsider p = Product f as Polynomial of F_Complex ;
take p ; :: thesis:
thus p = Product f ; :: thesis:
thus dom f = Seg n by A8; :: 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 A10; :: 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
A14: rbn = { y where y is Element of the carrier of (MultGroup F_Complex ) : ord y = n } and
A15: cyclotomic_poly n = poly_with_roots (rbn,1 -bag ) by Def5;
set bn = rbn,1 -bag ;
set rbibn = (ni -roots_of_1 ) \/ rbn;
reconsider rbibn = (ni -roots_of_1 ) \/ rbn as finite Subset of F_Complex ;
set bibn = rbibn,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
A16: x in (ni -roots_of_1 ) /\ rbn by XBOOLE_0:def 1;
A17: ( x in ni -roots_of_1 & x in rbn ) by A16, XBOOLE_0:def 4;
then consider y being Element of the carrier of (MultGroup F_Complex ) such that
A18: x = y and
A19: ord y divides ni by Th39;
consider y1 being Element of the carrier of (MultGroup F_Complex ) such that
A20: x = y1 and
A21: ord y1 = n by A14, A17;
thus contradiction by A1, A18, A19, A20, A21, NAT_D:7; :: thesis:

end;

then A22: ((ni -roots_of_1 ),1 -bag ) + (rbn,1 -bag ) = ((ni -roots_of_1 ) \/ rbn),1 -bag by UPROOTS:12;
A23: unital_poly F_Complex ,ni = poly_with_roots ((ni -roots_of_1 ),1 -bag ) by Th50;

now

let x be set ; :: thesis:

hereby :: thesis:

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

per cases ;

suppose ord y = n ; :: thesis:

then y in rbn by A14;
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 A25;
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 A26: ( x in rbibn or x in rbp ) by XBOOLE_0:def 3;

per cases by A26, XBOOLE_0:def 3;

suppose x in ni -roots_of_1 ; :: thesis:

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

end;

suppose x in rbn ; :: thesis:

then consider y being Element of the carrier of (MultGroup F_Complex ) such that
A27: ( x = y & ord y = n ) by A14;
thus x in n -roots_of_1 by A27, Th37; :: thesis:

end;

suppose x in rbp ; :: thesis:

then consider y being Element of the carrier of (MultGroup F_Complex ) such that
A28: ( x = y & ord y divides n & not ord y divides ni & ord y <> n ) ;
thus x in n -roots_of_1 by A28, Th37; :: thesis:

end;

then A29: n -roots_of_1 = rbibn \/ rbp by TARSKI:2;
rbibn misses rbp

proof

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

per cases by A31, 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 A32, A33; :: 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 A14;
hence contradiction by A32, A33; :: thesis:

end;

then A34: (n -roots_of_1 ),1 -bag = (rbibn,1 -bag ) + (rbp,1 -bag ) by A29, 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 A34, UPROOTS:66
.= ((unital_poly F_Complex ,ni) *' (cyclotomic_poly n)) *' (poly_with_roots (rbp,1 -bag )) by A15, A22, A23, UPROOTS:66 ;
hence unital_poly F_Complex ,n = ((unital_poly F_Complex ,ni) *' (cyclotomic_poly n)) *' p by A8, A10, Th57; :: thesis: