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: ( 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 ; :: thesis: 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

A3: n -roots_of_1 c= the carrier of (MultGroup F_Complex) by Th32;

set bp = (rbp,1) -bag ;

defpred S_{1}[ 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 ) );

A9: dom f = Seg n and

A10: for i being Nat st i in Seg n holds

S_{1}[i,f . i]
from FINSEQ_1:sch 5(A4);

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 = <%(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 ; :: 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 = <%(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 ; :: 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 = <%(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; :: 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 = <%(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; :: thesis: 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

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;

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

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: verum

set cPRFC = the carrier of (Polynom-Ring F_Complex);

let n, ni be non zero Element of NAT ; :: thesis: ( 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 ; :: thesis: 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

proof

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;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not 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 ) } or x in n -roots_of_1 )

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: x in n -roots_of_1

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: verum

end;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: x in n -roots_of_1

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: verum

A3: n -roots_of_1 c= the carrier of (MultGroup F_Complex) by Th32;

set bp = (rbp,1) -bag ;

defpred S

( $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: for i being Nat st i in Seg n holds

ex x being Element of the carrier of (Polynom-Ring F_Complex) st S_{1}[i,x]

consider f being FinSequence of the carrier of (Polynom-Ring F_Complex) such that ex x being Element of the carrier of (Polynom-Ring F_Complex) st S

let i be Nat; :: thesis: ( i in Seg n implies ex x being Element of the carrier of (Polynom-Ring F_Complex) st S_{1}[x,b_{2}] )

assume A5: i in Seg n ; :: thesis: ex x being Element of the carrier of (Polynom-Ring F_Complex) st S_{1}[x,b_{2}]

then A6: not i is zero by FINSEQ_1:1;

end;assume A5: i in Seg n ; :: thesis: ex x being Element of the carrier of (Polynom-Ring F_Complex) st S

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 ) )
;

end;

suppose A7:
( not i divides n or i divides ni or i = n )
; :: thesis: ex x being Element of the carrier of (Polynom-Ring F_Complex) st S_{1}[x,b_{2}]

<%(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_{1}[i,x]
by A6, A7; :: thesis: verum

end;hence ex x being Element of the carrier of (Polynom-Ring F_Complex) st S

suppose A8:
( i divides n & not i divides ni & i <> n )
; :: thesis: ex x being Element of the carrier of (Polynom-Ring F_Complex) st S_{1}[x,b_{2}]

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_{1}[i,x]
by A8; :: thesis: verum

end;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

A9: dom f = Seg n and

A10: for i being Nat st i in Seg n holds

S

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 = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) )

then
Product f = poly_with_roots ((rbp,1) -bag)
by A9, Th53;( ( ( 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 ) )

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 = <%(1_ F_Complex)%> ) & ( 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 = <%(1_ F_Complex)%> ) & ( 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 = <%(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: verum

end;assume i in Seg n ; :: thesis: ( ( ( 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 ) )

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: verum

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 = <%(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 ; :: 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 = <%(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 ; :: 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 = <%(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; :: 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 = <%(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; :: thesis: 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

proof

then A16:
(((ni -roots_of_1),1) -bag) + ((rbn,1) -bag) = (((ni -roots_of_1) \/ rbn),1) -bag
by UPROOTS:10;
assume
(ni -roots_of_1) /\ rbn <> {}
; :: according to XBOOLE_0:def 7 :: thesis: contradiction

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: verum

end;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: verum

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: 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 ) )

then A21:
n -roots_of_1 = rbibn \/ rbp
by TARSKI:2;( ( 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 b_{1} in n -roots_of_1 ) )

_{1} in n -roots_of_1

then A20: ( x in rbibn or x in rbp ) by XBOOLE_0:def 3;

end;hereby :: thesis: ( x in rbibn \/ rbp implies b_{1} in n -roots_of_1 )

assume
x in rbibn \/ rbp
; :: thesis: bassume A18:
x in n -roots_of_1
; :: thesis: x in rbibn \/ rbp

then reconsider y = x as Element of the carrier of (MultGroup F_Complex) by A3;

A19: ord y divides n by A18, Th34;

end;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
( ord y = n or ( ord y <> n & not ord y divides ni ) or ( ord y <> n & ord y divides ni ) )
;

end;

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;then y in rbibn by XBOOLE_0:def 3;

hence x in rbibn \/ rbp by XBOOLE_0:def 3; :: thesis: verum

suppose
( ord y <> n & ord y divides ni )
; :: thesis: x in rbibn \/ rbp

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: verum

end;then x in rbibn by XBOOLE_0:def 3;

hence x in rbibn \/ rbp by XBOOLE_0:def 3; :: thesis: verum

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 A20, XBOOLE_0:def 3;

end;

suppose
x in rbn
; :: thesis: b_{1} in n -roots_of_1

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: verum

end;( x = y & ord y = n ) by A12;

hence x in n -roots_of_1 by Th34; :: thesis: verum

suppose
x in rbp
; :: thesis: b_{1} in n -roots_of_1

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: verum

end;( 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

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

then A26:
((n -roots_of_1),1) -bag = ((rbibn,1) -bag) + ((rbp,1) -bag)
by A21, UPROOTS:10;
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 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;

end;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
( x in ni -roots_of_1 or x in rbn )
by A25, XBOOLE_0:def 3;

end;

suppose
x in ni -roots_of_1
; :: thesis: contradiction

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: verum

end;( x = y & ord y divides ni ) by Th36;

hence contradiction by A24; :: thesis: verum

suppose
x in rbn
; :: thesis: contradiction

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: verum

end;( x = y & ord y = n ) by A12;

hence contradiction by A24; :: thesis: verum

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: verum