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 ; :: 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 object ; :: 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 Th34; :: 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 Th32;
set bp = (rbp,1) -bag ;
defpred S₁[ 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 ) );

A4: now :: thesis:

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

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 10;
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 zero Element of NAT by A5, FINSEQ_1:1;
cyclotomic_poly i9 is Element of the carrier of (Polynom-Ring F_Complex) by POLYNOM3:def 10;
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 :: thesis:

let i be non zero Element of NAT ; :: thesis:
assume i in Seg n ; :: thesis:
then ex d being non zero 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, Th53;
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 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; :: 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 object 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 Th36;
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: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;

now :: thesis:

let x be object ; :: 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, Th34;

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 Th34;
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 Th34; :: 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 Th34; :: 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 Th46;
rbibn misses rbp

proof

assume rbibn /\ rbp <> {} ; :: according to XBOOLE_0:def 7 :: thesis:
then consider x being object 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 Th36;
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: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; :: thesis: