let n, ni be non zero Element of NAT ; :: thesis: for q being Integer st ni < n & ni divides n holds

for qc being Element of F_Complex st qc = q holds

for j, k, l being Integer st j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) holds

j divides k div l

let q be Integer; :: thesis: ( ni < n & ni divides n implies for qc being Element of F_Complex st qc = q holds

for j, k, l being Integer st j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) holds

j divides k div l )

assume A1: ( ni < n & ni divides n ) ; :: thesis: for qc being Element of F_Complex st qc = q holds

for j, k, l being Integer st j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) holds

j divides k div l

set ttt = (unital_poly (F_Complex,ni)) *' (cyclotomic_poly n);

consider f being FinSequence of the carrier of (Polynom-Ring F_Complex), p being Polynomial of F_Complex such that

A2: p = Product f and

A3: ( 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 ) ) ) ) and

A4: unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)) *' p by A1, Th54;

j divides k div l )

assume qc = q ; :: thesis: for j, k, l being Integer st j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) holds

j divides k div l

then eval (p,qc) is integer by A2, A5, Th55;

then consider m being Integer such that

A7: m = eval (p,qc) ;

let j, k, l be Integer; :: thesis: ( j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) implies j divides k div l )

assume A8: ( j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) ) ; :: thesis: j divides k div l

reconsider jc = j, lc = l, mc = m as Element of COMPLEX by XCMPLX_0:def 2;

reconsider jcf = jc, lcf = lc, mcf = mc as Element of F_Complex by COMPLFLD:def 1;

eval ((unital_poly (F_Complex,n)),qc) = (eval (((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)),qc)) * (eval (p,qc)) by A4, POLYNOM4:24;

then A9: k = (lcf * jcf) * mcf by A8, A7, POLYNOM4:24

.= (l * j) * m ;

for qc being Element of F_Complex st qc = q holds

for j, k, l being Integer st j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) holds

j divides k div l

let q be Integer; :: thesis: ( ni < n & ni divides n implies for qc being Element of F_Complex st qc = q holds

for j, k, l being Integer st j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) holds

j divides k div l )

assume A1: ( ni < n & ni divides n ) ; :: thesis: for qc being Element of F_Complex st qc = q holds

for j, k, l being Integer st j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) holds

j divides k div l

set ttt = (unital_poly (F_Complex,ni)) *' (cyclotomic_poly n);

consider f being FinSequence of the carrier of (Polynom-Ring F_Complex), p being Polynomial of F_Complex such that

A2: p = Product f and

A3: ( 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 ) ) ) ) and

A4: unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)) *' p by A1, Th54;

A5: now :: thesis: for i being non zero Element of NAT holds

( not i in dom f or f . i = <%(1_ F_Complex)%> or f . i = cyclotomic_poly i )

let qc be Element of F_Complex; :: thesis: ( qc = q implies for j, k, l being Integer st j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) holds ( not i in dom f or f . i = <%(1_ F_Complex)%> or f . i = cyclotomic_poly i )

let i be non zero Element of NAT ; :: thesis: ( not i in dom f or f . b_{1} = <%(1_ F_Complex)%> or f . b_{1} = cyclotomic_poly b_{1} )

assume A6: i in dom f ; :: thesis: ( f . b_{1} = <%(1_ F_Complex)%> or f . b_{1} = cyclotomic_poly b_{1} )

end;assume A6: i in dom f ; :: thesis: ( f . b

j divides k div l )

assume qc = q ; :: thesis: for j, k, l being Integer st j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) holds

j divides k div l

then eval (p,qc) is integer by A2, A5, Th55;

then consider m being Integer such that

A7: m = eval (p,qc) ;

let j, k, l be Integer; :: thesis: ( j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) implies j divides k div l )

assume A8: ( j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) ) ; :: thesis: j divides k div l

reconsider jc = j, lc = l, mc = m as Element of COMPLEX by XCMPLX_0:def 2;

reconsider jcf = jc, lcf = lc, mcf = mc as Element of F_Complex by COMPLFLD:def 1;

eval ((unital_poly (F_Complex,n)),qc) = (eval (((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)),qc)) * (eval (p,qc)) by A4, POLYNOM4:24;

then A9: k = (lcf * jcf) * mcf by A8, A7, POLYNOM4:24

.= (l * j) * m ;

now :: thesis: j divides k div lend;

hence
j divides k div l
; :: thesis: verumper cases
( l <> 0 or l = 0 )
;

end;

suppose A10:
l <> 0
; :: thesis: j divides k div l

k = l * (j * m)
by A9;

then l divides k by INT_1:def 3;

then k / l is integer by A10, WSIERP_1:17;

then [\(k / l)/] = k / l by INT_1:25;

then k div l = ((j * m) * l) / l by A9, INT_1:def 9;

then k div l = j * m by A10, XCMPLX_1:89;

hence j divides k div l by INT_1:def 3; :: thesis: verum

end;then l divides k by INT_1:def 3;

then k / l is integer by A10, WSIERP_1:17;

then [\(k / l)/] = k / l by INT_1:25;

then k div l = ((j * m) * l) / l by A9, INT_1:def 9;

then k div l = j * m by A10, XCMPLX_1:89;

hence j divides k div l by INT_1:def 3; :: thesis: verum