deffunc H_{1}( non zero Nat) -> Polynomial of F_Complex = cyclotomic_poly $1;

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

set cFC = the carrier of F_Complex;

defpred S_{1}[ non zero Element of NAT ] means ( ( H_{1}($1) . 0 = 1 or H_{1}($1) . 0 = - 1 ) & ( for i being Element of NAT holds H_{1}($1) . i is integer ) );

A1: - (1_ F_Complex) = - 1 by COMPLFLD:2, COMPLFLD:8;

_{1}[d]
from UNIROOTS:sch 1(A2);

hence for d being non zero Element of NAT

for i being Element of NAT holds

( ( (cyclotomic_poly d) . 0 = 1 or (cyclotomic_poly d) . 0 = - 1 ) & (cyclotomic_poly d) . i is integer ) ; :: thesis: verum

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

set cFC = the carrier of F_Complex;

defpred S

A1: - (1_ F_Complex) = - 1 by COMPLFLD:2, COMPLFLD:8;

A2: now :: thesis: for k being non zero Element of NAT st ( for n being non zero Element of NAT st n < k holds

S_{1}[n] ) holds

S_{1}[k]

for d being non zero Element of NAT holds SS

S

let k be non zero Element of NAT ; :: thesis: ( ( for n being non zero Element of NAT st n < k holds

S_{1}[n] ) implies S_{1}[b_{1}] )

assume A3: for n being non zero Element of NAT st n < k holds

S_{1}[n]
; :: thesis: S_{1}[b_{1}]

A4: 1 <= k by Lm1;

end;S

assume A3: for n being non zero Element of NAT st n < k holds

S

A4: 1 <= k by Lm1;

per cases
( k = 1 or k > 1 )
by A4, XXREAL_0:1;

end;

suppose A5:
k = 1
; :: thesis: S_{1}[b_{1}]

_{1}[k]
by A1, A5, Th48, POLYNOM5:38; :: thesis: verum

end;

now :: thesis: for i being Element of NAT holds H_{1}(k) . i is integer

hence
Slet i be Element of NAT ; :: thesis: H_{1}(k) . b_{1} is integer

end;suppose A6:
k > 1
; :: thesis: S_{1}[b_{1}]

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

A7: p = Product f and

A8: dom f = Seg k and

A9: for i being non zero Element of NAT st i in Seg k holds

( ( ( not i divides k or i = k ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides k & i <> k implies f . i = H_{1}(i) ) )
and

A10: unital_poly (F_Complex,k) = (cyclotomic_poly k) *' p by Th50;

defpred S_{2}[ Nat, object ] means ex g being FinSequence of the carrier of (Polynom-Ring F_Complex) ex p being Polynomial of F_Complex st

( g = f | (Seg $1) & p = Product g & $2 = p & ( p . 0 = 1 or p . 0 = - 1 ) & ( for j being Element of NAT holds p . j is integer ) );

defpred S_{3}[ Nat] means ( $1 in Seg (len f) implies ex x being object st S_{2}[$1,x] );

A11: k = len f by A8, FINSEQ_1:def 3;

A12: for l being Nat st S_{3}[l] holds

S_{3}[l + 1]
_{4}[ Nat] means H_{1}(k) . $1 is integer ;

A47: (0 + 1) -' 1 = 0 by NAT_D:34;

A48: S_{3}[ 0 ]
by FINSEQ_1:1;

for l being Nat holds S_{3}[l]
from NAT_1:sch 2(A48, A12);

then A49: for l being Nat st l in Seg (len f) holds

ex x being object st S_{2}[l,x]
;

consider F being FinSequence such that

dom F = Seg (len f) and

A50: for i being Nat st i in Seg (len f) holds

S_{2}[i,F . i]
from FINSEQ_1:sch 1(A49);

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

A51: ( g = f | (Seg k) & p1 = Product g ) and

F . k = p1 and

A52: ( p1 . 0 = 1 or p1 . 0 = - 1 ) and

A53: for j being Element of NAT holds p1 . j is integer by A11, A50, FINSEQ_1:3;

A54: p = p1 by A7, A11, A51, FINSEQ_3:49;

_{4}[i]
from NAT_1:sch 4(A55);

consider r being FinSequence of the carrier of F_Complex such that

A72: len r = 0 + 1 and

A73: (unital_poly (F_Complex,k)) . 0 = Sum r and

A74: for l being Element of NAT st l in dom r holds

r . l = (p . (l -' 1)) * (H_{1}(k) . ((0 + 1) -' l))
by A10, POLYNOM3:def 9;

A75: 1 in dom r by A72, FINSEQ_3:25;

then reconsider r1 = r . 1 as Element of the carrier of F_Complex by FINSEQ_2:11;

r = <*r1*> by A72, FINSEQ_1:40;

then A76: Sum r = r . 1 by RLVECT_1:44

.= (p . 0) * (H_{1}(k) . 0)
by A74, A47, A75
;

( H_{1}(k) . 0 = 1 or H_{1}(k) . 0 = - 1 )
_{1}[k]
by A71; :: thesis: verum

end;A7: p = Product f and

A8: dom f = Seg k and

A9: for i being non zero Element of NAT st i in Seg k holds

( ( ( not i divides k or i = k ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides k & i <> k implies f . i = H

A10: unital_poly (F_Complex,k) = (cyclotomic_poly k) *' p by Th50;

defpred S

( g = f | (Seg $1) & p = Product g & $2 = p & ( p . 0 = 1 or p . 0 = - 1 ) & ( for j being Element of NAT holds p . j is integer ) );

defpred S

A11: k = len f by A8, FINSEQ_1:def 3;

A12: for l being Nat st S

S

proof

defpred S
let l be Nat; :: thesis: ( S_{3}[l] implies S_{3}[l + 1] )

assume A13: S_{3}[l]
; :: thesis: S_{3}[l + 1]

assume A14: l + 1 in Seg (len f) ; :: thesis: ex x being object st S_{2}[l + 1,x]

end;assume A13: S

assume A14: l + 1 in Seg (len f) ; :: thesis: ex x being object st S

per cases
( l = 0 or 0 < l )
;

end;

suppose A15:
l = 0
; :: thesis: ex x being object st S_{2}[l + 1,x]

reconsider fl1 = f . (l + 1) as Element of the carrier of (Polynom-Ring F_Complex) by A8, A11, A14, FINSEQ_2:11;

reconsider g = f | (Seg (l + 1)) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;

reconsider p = Product g as Polynomial of F_Complex by POLYNOM3:def 10;

<*> the carrier of (Polynom-Ring F_Complex) = f | (Seg 0) ;

then g = (<*> the carrier of (Polynom-Ring F_Complex)) ^ <*(f . (l + 1))*> by A8, A11, A14, A15, FINSEQ_5:10

.= <*(f . (l + 1))*> by FINSEQ_1:34 ;

then A16: p = fl1 by FINSOP_1:11;

take p ; :: thesis: S_{2}[l + 1,p]

take g ; :: thesis: ex p being Polynomial of F_Complex st

( g = f | (Seg (l + 1)) & p = Product g & p = p & ( p . 0 = 1 or p . 0 = - 1 ) & ( for j being Element of NAT holds p . j is integer ) )

take p ; :: thesis: ( g = f | (Seg (l + 1)) & p = Product g & p = p & ( p . 0 = 1 or p . 0 = - 1 ) & ( for j being Element of NAT holds p . j is integer ) )

thus ( g = f | (Seg (l + 1)) & p = Product g & p = p ) ; :: thesis: ( ( p . 0 = 1 or p . 0 = - 1 ) & ( for j being Element of NAT holds p . j is integer ) )

1 divides k by NAT_D:6;

then A17: f . 1 = H_{1}(1)
by A6, A9, A11, A14, A15;

hence ( p . 0 = 1 or p . 0 = - 1 ) by A1, A15, A16, Th48, POLYNOM5:38; :: thesis: for j being Element of NAT holds p . j is integer

let j be Element of NAT ; :: thesis: p . j is integer

thus p . j is integer :: thesis: verum

end;reconsider g = f | (Seg (l + 1)) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;

reconsider p = Product g as Polynomial of F_Complex by POLYNOM3:def 10;

<*> the carrier of (Polynom-Ring F_Complex) = f | (Seg 0) ;

then g = (<*> the carrier of (Polynom-Ring F_Complex)) ^ <*(f . (l + 1))*> by A8, A11, A14, A15, FINSEQ_5:10

.= <*(f . (l + 1))*> by FINSEQ_1:34 ;

then A16: p = fl1 by FINSOP_1:11;

take p ; :: thesis: S

take g ; :: thesis: ex p being Polynomial of F_Complex st

( g = f | (Seg (l + 1)) & p = Product g & p = p & ( p . 0 = 1 or p . 0 = - 1 ) & ( for j being Element of NAT holds p . j is integer ) )

take p ; :: thesis: ( g = f | (Seg (l + 1)) & p = Product g & p = p & ( p . 0 = 1 or p . 0 = - 1 ) & ( for j being Element of NAT holds p . j is integer ) )

thus ( g = f | (Seg (l + 1)) & p = Product g & p = p ) ; :: thesis: ( ( p . 0 = 1 or p . 0 = - 1 ) & ( for j being Element of NAT holds p . j is integer ) )

1 divides k by NAT_D:6;

then A17: f . 1 = H

hence ( p . 0 = 1 or p . 0 = - 1 ) by A1, A15, A16, Th48, POLYNOM5:38; :: thesis: for j being Element of NAT holds p . j is integer

let j be Element of NAT ; :: thesis: p . j is integer

thus p . j is integer :: thesis: verum

suppose A18:
0 < l
; :: thesis: ex x being object st S_{2}[l + 1,x]

( l + 1 <= len f & l <= l + 1 )
by A14, FINSEQ_1:1, NAT_1:12;

then A19: l <= len f by XXREAL_0:2;

0 + 1 <= l by A18, NAT_1:13;

then consider x being set such that

A20: S_{2}[l,x]
by A13, A19, FINSEQ_1:1;

reconsider fl1 = f . (l + 1) as Element of the carrier of (Polynom-Ring F_Complex) by A8, A11, A14, FINSEQ_2:11;

reconsider g1 = f | (Seg (l + 1)) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;

reconsider p1 = Product g1 as Polynomial of F_Complex by POLYNOM3:def 10;

take p1 ; :: thesis: S_{2}[l + 1,p1]

take g1 ; :: thesis: ex p being Polynomial of F_Complex st

( g1 = f | (Seg (l + 1)) & p = Product g1 & p1 = p & ( p . 0 = 1 or p . 0 = - 1 ) & ( for j being Element of NAT holds p . j is integer ) )

take p1 ; :: thesis: ( g1 = f | (Seg (l + 1)) & p1 = Product g1 & p1 = p1 & ( p1 . 0 = 1 or p1 . 0 = - 1 ) & ( for j being Element of NAT holds p1 . j is integer ) )

thus ( g1 = f | (Seg (l + 1)) & p1 = Product g1 & p1 = p1 ) ; :: thesis: ( ( p1 . 0 = 1 or p1 . 0 = - 1 ) & ( for j being Element of NAT holds p1 . j is integer ) )

reconsider fl1p = fl1 as Polynomial of F_Complex by POLYNOM3:def 10;

reconsider m1 = - 1 as Element of COMPLEX by XCMPLX_0:def 2;

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

A21: g = f | (Seg l) and

A22: p = Product g and

x = p and

A23: ( p . 0 = 1 or p . 0 = - 1 ) and

A24: for j being Element of NAT holds p . j is integer by A20;

g1 = g ^ <*fl1*> by A8, A11, A14, A21, FINSEQ_5:10;

then Product g1 = (Product g) * fl1 by GROUP_4:6;

then A25: p1 = p *' fl1p by A22, POLYNOM3:def 10;

thus ( ( p1 . 0 = 1 or p1 . 0 = - 1 ) & ( for j being Element of NAT holds p1 . j is integer ) ) :: thesis: verum

end;then A19: l <= len f by XXREAL_0:2;

0 + 1 <= l by A18, NAT_1:13;

then consider x being set such that

A20: S

reconsider fl1 = f . (l + 1) as Element of the carrier of (Polynom-Ring F_Complex) by A8, A11, A14, FINSEQ_2:11;

reconsider g1 = f | (Seg (l + 1)) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;

reconsider p1 = Product g1 as Polynomial of F_Complex by POLYNOM3:def 10;

take p1 ; :: thesis: S

take g1 ; :: thesis: ex p being Polynomial of F_Complex st

( g1 = f | (Seg (l + 1)) & p = Product g1 & p1 = p & ( p . 0 = 1 or p . 0 = - 1 ) & ( for j being Element of NAT holds p . j is integer ) )

take p1 ; :: thesis: ( g1 = f | (Seg (l + 1)) & p1 = Product g1 & p1 = p1 & ( p1 . 0 = 1 or p1 . 0 = - 1 ) & ( for j being Element of NAT holds p1 . j is integer ) )

thus ( g1 = f | (Seg (l + 1)) & p1 = Product g1 & p1 = p1 ) ; :: thesis: ( ( p1 . 0 = 1 or p1 . 0 = - 1 ) & ( for j being Element of NAT holds p1 . j is integer ) )

reconsider fl1p = fl1 as Polynomial of F_Complex by POLYNOM3:def 10;

reconsider m1 = - 1 as Element of COMPLEX by XCMPLX_0:def 2;

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

A21: g = f | (Seg l) and

A22: p = Product g and

x = p and

A23: ( p . 0 = 1 or p . 0 = - 1 ) and

A24: for j being Element of NAT holds p . j is integer by A20;

g1 = g ^ <*fl1*> by A8, A11, A14, A21, FINSEQ_5:10;

then Product g1 = (Product g) * fl1 by GROUP_4:6;

then A25: p1 = p *' fl1p by A22, POLYNOM3:def 10;

thus ( ( p1 . 0 = 1 or p1 . 0 = - 1 ) & ( for j being Element of NAT holds p1 . j is integer ) ) :: thesis: verum

proof
end;

per cases
( not l + 1 divides k or l + 1 = k or ( l + 1 divides k & l + 1 <> k ) )
;

end;

suppose
( not l + 1 divides k or l + 1 = k )
; :: thesis: ( ( p1 . 0 = 1 or p1 . 0 = - 1 ) & ( for j being Element of NAT holds p1 . j is integer ) )

then A26:
fl1p = <%(1_ F_Complex)%>
by A9, A11, A14;

consider r being FinSequence of F_Complex such that

A27: len r = 0 + 1 and

A28: p1 . 0 = Sum r and

A29: for m being Element of NAT st m in dom r holds

r . m = (p . (m -' 1)) * (fl1p . ((0 + 1) -' m)) by A25, POLYNOM3:def 9;

1 in dom r by A27, FINSEQ_3:25;

then reconsider r1 = r . 1 as Element of F_Complex by FINSEQ_2:11;

r = <*r1*> by A27, FINSEQ_1:40;

then A30: p1 . 0 = r1 by A28, RLVECT_1:44;

1 in dom r by A27, FINSEQ_3:25;

then A31: p1 . 0 = (p . (1 -' 1)) * (fl1p . ((0 + 1) -' 1)) by A29, A30

.= (p . ((0 + 1) -' 1)) * (fl1p . 0) by NAT_D:34

.= (p . 0) * (fl1p . 0) by NAT_D:34

.= (p . 0) * (1_ F_Complex) by A26, POLYNOM5:32 ;

thus ( p1 . 0 = 1 or p1 . 0 = - 1 ) :: thesis: for j being Element of NAT holds p1 . j is integer

consider r being FinSequence of F_Complex such that

len r = j + 1 and

A32: p1 . j = Sum r and

A33: for m being Element of NAT st m in dom r holds

r . m = (p . (m -' 1)) * (fl1p . ((j + 1) -' m)) by A25, POLYNOM3:def 9;

for i being Element of NAT st i in dom r holds

r . i is integer

end;consider r being FinSequence of F_Complex such that

A27: len r = 0 + 1 and

A28: p1 . 0 = Sum r and

A29: for m being Element of NAT st m in dom r holds

r . m = (p . (m -' 1)) * (fl1p . ((0 + 1) -' m)) by A25, POLYNOM3:def 9;

1 in dom r by A27, FINSEQ_3:25;

then reconsider r1 = r . 1 as Element of F_Complex by FINSEQ_2:11;

r = <*r1*> by A27, FINSEQ_1:40;

then A30: p1 . 0 = r1 by A28, RLVECT_1:44;

1 in dom r by A27, FINSEQ_3:25;

then A31: p1 . 0 = (p . (1 -' 1)) * (fl1p . ((0 + 1) -' 1)) by A29, A30

.= (p . ((0 + 1) -' 1)) * (fl1p . 0) by NAT_D:34

.= (p . 0) * (fl1p . 0) by NAT_D:34

.= (p . 0) * (1_ F_Complex) by A26, POLYNOM5:32 ;

thus ( p1 . 0 = 1 or p1 . 0 = - 1 ) :: thesis: for j being Element of NAT holds p1 . j is integer

proof
end;

let j be Element of NAT ; :: thesis: p1 . j is integer consider r being FinSequence of F_Complex such that

len r = j + 1 and

A32: p1 . j = Sum r and

A33: for m being Element of NAT st m in dom r holds

r . m = (p . (m -' 1)) * (fl1p . ((j + 1) -' m)) by A25, POLYNOM3:def 9;

for i being Element of NAT st i in dom r holds

r . i is integer

proof

hence
p1 . j is integer
by A32, Th4; :: thesis: verum
let i be Element of NAT ; :: thesis: ( i in dom r implies r . i is integer )

reconsider pi1 = p . (i -' 1) as Integer by A24;

set j1i = (j + 1) -' i;

assume i in dom r ; :: thesis: r . i is integer

then r . i = (p . (i -' 1)) * (fl1p . ((j + 1) -' i)) by A33

.= pi1 * fl1pj1i ;

hence r . i is integer ; :: thesis: verum

end;reconsider pi1 = p . (i -' 1) as Integer by A24;

set j1i = (j + 1) -' i;

now :: thesis: ( ( (j + 1) -' i = 0 & fl1p . ((j + 1) -' i) = 1 ) or ( (j + 1) -' i >= 1 & fl1p . ((j + 1) -' i) = 0 ) )

then reconsider fl1pj1i = fl1p . ((j + 1) -' i) as Integer ;A34:
( (j + 1) -' i = 0 or (j + 1) -' i >= 0 + 1 )
by NAT_1:13;

end;assume i in dom r ; :: thesis: r . i is integer

then r . i = (p . (i -' 1)) * (fl1p . ((j + 1) -' i)) by A33

.= pi1 * fl1pj1i ;

hence r . i is integer ; :: thesis: verum

suppose A35:
( l + 1 divides k & l + 1 <> k )
; :: thesis: ( ( p1 . 0 = 1 or p1 . 0 = - 1 ) & ( for j being Element of NAT holds p1 . j is integer ) )

consider r being FinSequence of F_Complex such that

A36: len r = 0 + 1 and

A37: p1 . 0 = Sum r and

A38: for m being Element of NAT st m in dom r holds

r . m = (p . (m -' 1)) * (fl1p . ((0 + 1) -' m)) by A25, POLYNOM3:def 9;

1 in dom r by A36, FINSEQ_3:25;

then reconsider r1 = r . 1 as Element of F_Complex by FINSEQ_2:11;

r = <*r1*> by A36, FINSEQ_1:40;

then A39: p1 . 0 = r1 by A37, RLVECT_1:44;

1 in dom r by A36, FINSEQ_3:25;

then A40: p1 . 0 = (p . (1 -' 1)) * (fl1p . ((0 + 1) -' 1)) by A38, A39

.= (p . ((0 + 1) -' 1)) * (fl1p . 0) by NAT_D:34

.= (p . 0) * (fl1p . 0) by NAT_D:34 ;

l + 1 <= k by A35, NAT_D:7;

then A41: l + 1 < k by A35, XXREAL_0:1;

A42: l + 1 in NAT by ORDINAL1:def 12;

A43: fl1p = H_{1}(l + 1)
by A9, A11, A14, A35;

then reconsider fl1p0 = fl1p . 0 as Integer by A3, A41, A42;

A44: ( fl1p0 = 1 or fl1p0 = m1 ) by A3, A43, A41, A42;

thus ( p1 . 0 = 1 or p1 . 0 = - 1 ) :: thesis: for j being Element of NAT holds p1 . j is integer

consider r being FinSequence of F_Complex such that

len r = j + 1 and

A45: p1 . j = Sum r and

A46: for m being Element of NAT st m in dom r holds

r . m = (p . (m -' 1)) * (fl1p . ((j + 1) -' m)) by A25, POLYNOM3:def 9;

for i being Element of NAT st i in dom r holds

r . i is integer

end;A36: len r = 0 + 1 and

A37: p1 . 0 = Sum r and

A38: for m being Element of NAT st m in dom r holds

r . m = (p . (m -' 1)) * (fl1p . ((0 + 1) -' m)) by A25, POLYNOM3:def 9;

1 in dom r by A36, FINSEQ_3:25;

then reconsider r1 = r . 1 as Element of F_Complex by FINSEQ_2:11;

r = <*r1*> by A36, FINSEQ_1:40;

then A39: p1 . 0 = r1 by A37, RLVECT_1:44;

1 in dom r by A36, FINSEQ_3:25;

then A40: p1 . 0 = (p . (1 -' 1)) * (fl1p . ((0 + 1) -' 1)) by A38, A39

.= (p . ((0 + 1) -' 1)) * (fl1p . 0) by NAT_D:34

.= (p . 0) * (fl1p . 0) by NAT_D:34 ;

l + 1 <= k by A35, NAT_D:7;

then A41: l + 1 < k by A35, XXREAL_0:1;

A42: l + 1 in NAT by ORDINAL1:def 12;

A43: fl1p = H

then reconsider fl1p0 = fl1p . 0 as Integer by A3, A41, A42;

A44: ( fl1p0 = 1 or fl1p0 = m1 ) by A3, A43, A41, A42;

thus ( p1 . 0 = 1 or p1 . 0 = - 1 ) :: thesis: for j being Element of NAT holds p1 . j is integer

proof
end;

let j be Element of NAT ; :: thesis: p1 . j is integer consider r being FinSequence of F_Complex such that

len r = j + 1 and

A45: p1 . j = Sum r and

A46: for m being Element of NAT st m in dom r holds

r . m = (p . (m -' 1)) * (fl1p . ((j + 1) -' m)) by A25, POLYNOM3:def 9;

for i being Element of NAT st i in dom r holds

r . i is integer

proof

hence
p1 . j is integer
by A45, Th4; :: thesis: verum
let i be Element of NAT ; :: thesis: ( i in dom r implies r . i is integer )

l + 1 in NAT by ORDINAL1:def 12;

then reconsider fl1pj1i = fl1p . ((j + 1) -' i) as Integer by A3, A43, A41;

reconsider pi1 = p . (i -' 1) as Integer by A24;

assume i in dom r ; :: thesis: r . i is integer

then r . i = (p . (i -' 1)) * (fl1p . ((j + 1) -' i)) by A46

.= pi1 * fl1pj1i ;

hence r . i is integer ; :: thesis: verum

end;l + 1 in NAT by ORDINAL1:def 12;

then reconsider fl1pj1i = fl1p . ((j + 1) -' i) as Integer by A3, A43, A41;

reconsider pi1 = p . (i -' 1) as Integer by A24;

assume i in dom r ; :: thesis: r . i is integer

then r . i = (p . (i -' 1)) * (fl1p . ((j + 1) -' i)) by A46

.= pi1 * fl1pj1i ;

hence r . i is integer ; :: thesis: verum

A47: (0 + 1) -' 1 = 0 by NAT_D:34;

A48: S

for l being Nat holds S

then A49: for l being Nat st l in Seg (len f) holds

ex x being object st S

consider F being FinSequence such that

dom F = Seg (len f) and

A50: for i being Nat st i in Seg (len f) holds

S

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

A51: ( g = f | (Seg k) & p1 = Product g ) and

F . k = p1 and

A52: ( p1 . 0 = 1 or p1 . 0 = - 1 ) and

A53: for j being Element of NAT holds p1 . j is integer by A11, A50, FINSEQ_1:3;

A54: p = p1 by A7, A11, A51, FINSEQ_3:49;

A55: now :: thesis: for m being Nat st ( for n being Nat st n < m holds

S_{4}[n] ) holds

S_{4}[m]

A71:
for i being Nat holds SS

S

let m be Nat; :: thesis: ( ( for n being Nat st n < m holds

S_{4}[n] ) implies S_{4}[b_{1}] )

reconsider m1 = m as Element of NAT by ORDINAL1:def 12;

consider r being FinSequence of the carrier of F_Complex such that

A56: len r = m + 1 and

A57: (unital_poly (F_Complex,k)) . m = Sum r and

A58: for l being Element of NAT st l in dom r holds

r . l = (p . (l -' 1)) * (H_{1}(k) . ((m1 + 1) -' l))
by A10, POLYNOM3:def 9;

reconsider Src = Sum r as Element of COMPLEX by COMPLFLD:def 1;

A59: ((1,1) -cut r) ^ (((1 + 1),(len r)) -cut r) = r by A56, FINSEQ_6:135, NAT_1:11;

set s = ((1 + 1),(len r)) -cut r;

reconsider Ssc = Sum (((1 + 1),(len r)) -cut r) as Element of COMPLEX by COMPLFLD:def 1;

assume A60: for n being Nat st n < m holds

S_{4}[n]
; :: thesis: S_{4}[b_{1}]

A68: 1 <= len r by A56, NAT_1:11;

then A69: 1 in dom r by FINSEQ_3:25;

then reconsider r1 = r . 1 as Element of the carrier of F_Complex by FINSEQ_2:11;

reconsider r1c = r1 as Element of COMPLEX by COMPLFLD:def 1;

(1,1) -cut r = <*r1*> by A68, FINSEQ_6:132;

then Sum r = r1 + (Sum (((1 + 1),(len r)) -cut r)) by A59, FVSUM_1:72;

then r1c = Sr - Ss ;

then reconsider r1i = r1 as Integer ;

A70: r1i = (p . (1 -' 1)) * (H_{1}(k) . ((m + 1) -' 1))
by A58, A69

.= (p . 0) * (H_{1}(k) . m1)
by A47, NAT_D:34
;

end;S

reconsider m1 = m as Element of NAT by ORDINAL1:def 12;

consider r being FinSequence of the carrier of F_Complex such that

A56: len r = m + 1 and

A57: (unital_poly (F_Complex,k)) . m = Sum r and

A58: for l being Element of NAT st l in dom r holds

r . l = (p . (l -' 1)) * (H

reconsider Src = Sum r as Element of COMPLEX by COMPLFLD:def 1;

now :: thesis: Src is integer

then reconsider Sr = Src as Integer ;end;

A59: ((1,1) -cut r) ^ (((1 + 1),(len r)) -cut r) = r by A56, FINSEQ_6:135, NAT_1:11;

set s = ((1 + 1),(len r)) -cut r;

reconsider Ssc = Sum (((1 + 1),(len r)) -cut r) as Element of COMPLEX by COMPLFLD:def 1;

assume A60: for n being Nat st n < m holds

S

now :: thesis: for i being Element of NAT st i in dom (((1 + 1),(len r)) -cut r) holds

(((1 + 1),(len r)) -cut r) . i is integer

then reconsider Ss = Ssc as Integer by Th4;(((1 + 1),(len r)) -cut r) . i is integer

let i be Element of NAT ; :: thesis: ( i in dom (((1 + 1),(len r)) -cut r) implies (((1 + 1),(len r)) -cut r) . b_{1} is integer )

assume A61: i in dom (((1 + 1),(len r)) -cut r) ; :: thesis: (((1 + 1),(len r)) -cut r) . b_{1} is integer

end;assume A61: i in dom (((1 + 1),(len r)) -cut r) ; :: thesis: (((1 + 1),(len r)) -cut r) . b

per cases
( len r < 2 or 1 + 1 <= len r )
;

end;

suppose
len r < 2
; :: thesis: (((1 + 1),(len r)) -cut r) . b_{1} is integer

then
((1 + 1),(len r)) -cut r = {}
by FINSEQ_6:def 4;

hence (((1 + 1),(len r)) -cut r) . i is integer ; :: thesis: verum

end;hence (((1 + 1),(len r)) -cut r) . i is integer ; :: thesis: verum

suppose A62:
1 + 1 <= len r
; :: thesis: (((1 + 1),(len r)) -cut r) . b_{1} is integer

then A63:
(len (((1 + 1),(len r)) -cut r)) + (1 + 1) = (len r) + 1
by FINSEQ_6:def 4;

end;per cases
( m = 0 or m > 0 )
;

end;

suppose A64:
m > 0
; :: thesis: (((1 + 1),(len r)) -cut r) . b_{1} is integer

i <> 0
by A61, FINSEQ_3:25;

then reconsider cpkmi = H_{1}(k) . (m -' i) as Integer by A60, A64, NAT_2:9;

reconsider ppi = p . i as Integer by A53, A54;

i <> 0 by A61, FINSEQ_3:25;

then consider i1 being Nat such that

A65: i = i1 + 1 by NAT_1:6;

A66: i <= len (((1 + 1),(len r)) -cut r) by A61, FINSEQ_3:25;

then ( 1 <= i + 1 & i + 1 <= (len (((1 + 1),(len r)) -cut r)) + 1 ) by NAT_1:11, XREAL_1:6;

then 1 + i in dom r by A63, FINSEQ_3:25;

then A67: r . (1 + i) = (p . ((1 + i) -' 1)) * (H_{1}(k) . ((m + 1) -' (1 + i)))
by A58

.= (p . ((i + 1) -' 1)) * (H_{1}(k) . (((m + 1) -' 1) -' i))
by NAT_2:30

.= (p . i) * (H_{1}(k) . (((m + 1) -' 1) -' i))
by NAT_D:34

.= ppi * cpkmi by NAT_D:34 ;

i1 < len (((1 + 1),(len r)) -cut r) by A66, A65, NAT_1:13;

then (((1 + 1),(len r)) -cut r) . i = r . ((1 + 1) + i1) by A62, A65, FINSEQ_6:def 4

.= r . (1 + i) by A65 ;

hence (((1 + 1),(len r)) -cut r) . i is integer by A67; :: thesis: verum

end;then reconsider cpkmi = H

reconsider ppi = p . i as Integer by A53, A54;

i <> 0 by A61, FINSEQ_3:25;

then consider i1 being Nat such that

A65: i = i1 + 1 by NAT_1:6;

A66: i <= len (((1 + 1),(len r)) -cut r) by A61, FINSEQ_3:25;

then ( 1 <= i + 1 & i + 1 <= (len (((1 + 1),(len r)) -cut r)) + 1 ) by NAT_1:11, XREAL_1:6;

then 1 + i in dom r by A63, FINSEQ_3:25;

then A67: r . (1 + i) = (p . ((1 + i) -' 1)) * (H

.= (p . ((i + 1) -' 1)) * (H

.= (p . i) * (H

.= ppi * cpkmi by NAT_D:34 ;

i1 < len (((1 + 1),(len r)) -cut r) by A66, A65, NAT_1:13;

then (((1 + 1),(len r)) -cut r) . i = r . ((1 + 1) + i1) by A62, A65, FINSEQ_6:def 4

.= r . (1 + i) by A65 ;

hence (((1 + 1),(len r)) -cut r) . i is integer by A67; :: thesis: verum

A68: 1 <= len r by A56, NAT_1:11;

then A69: 1 in dom r by FINSEQ_3:25;

then reconsider r1 = r . 1 as Element of the carrier of F_Complex by FINSEQ_2:11;

reconsider r1c = r1 as Element of COMPLEX by COMPLFLD:def 1;

(1,1) -cut r = <*r1*> by A68, FINSEQ_6:132;

then Sum r = r1 + (Sum (((1 + 1),(len r)) -cut r)) by A59, FVSUM_1:72;

then r1c = Sr - Ss ;

then reconsider r1i = r1 as Integer ;

A70: r1i = (p . (1 -' 1)) * (H

.= (p . 0) * (H

per cases
( p . 0 = 1 or p . 0 = - 1 )
by A7, A11, A51, A52, FINSEQ_3:49;

end;

suppose
p . 0 = - 1
; :: thesis: S_{4}[b_{1}]

then r1 =
(- (1_ F_Complex)) * (H_{1}(k) . m1)
by A70, COMPLFLD:2, COMPLFLD:8

.= - ((1_ F_Complex) * (H_{1}(k) . m1))
by VECTSP_1:9

.= - (H_{1}(k) . m1)
;

then 0. F_Complex = (- (H_{1}(k) . m1)) + (- r1)
by RLVECT_1:def 10

.= (- r1) - (H_{1}(k) . m1)
;

then - r1 = H_{1}(k) . m
by VECTSP_1:19;

then - r1i = H_{1}(k) . m
by COMPLFLD:2;

hence S_{4}[m]
; :: thesis: verum

end;.= - ((1_ F_Complex) * (H

.= - (H

then 0. F_Complex = (- (H

.= (- r1) - (H

then - r1 = H

then - r1i = H

hence S

consider r being FinSequence of the carrier of F_Complex such that

A72: len r = 0 + 1 and

A73: (unital_poly (F_Complex,k)) . 0 = Sum r and

A74: for l being Element of NAT st l in dom r holds

r . l = (p . (l -' 1)) * (H

A75: 1 in dom r by A72, FINSEQ_3:25;

then reconsider r1 = r . 1 as Element of the carrier of F_Complex by FINSEQ_2:11;

r = <*r1*> by A72, FINSEQ_1:40;

then A76: Sum r = r . 1 by RLVECT_1:44

.= (p . 0) * (H

( H

proof
end;

hence
Sper cases
( p . 0 = 1 or p . 0 = - 1 )
by A7, A11, A51, A52, FINSEQ_3:49;

end;

suppose
p . 0 = - 1
; :: thesis: ( H_{1}(k) . 0 = 1 or H_{1}(k) . 0 = - 1 )

then - (1_ F_Complex) =
(- (1_ F_Complex)) * (H_{1}(k) . 0)
by A1, A73, A76, Th38

.= - ((1_ F_Complex) * (H_{1}(k) . 0))
by VECTSP_1:9

.= - (H_{1}(k) . 0)
;

hence ( H_{1}(k) . 0 = 1 or H_{1}(k) . 0 = - 1 )
by COMPLFLD:8, RLVECT_1:18; :: thesis: verum

end;.= - ((1_ F_Complex) * (H

.= - (H

hence ( H

hence for d being non zero Element of NAT

for i being Element of NAT holds

( ( (cyclotomic_poly d) . 0 = 1 or (cyclotomic_poly d) . 0 = - 1 ) & (cyclotomic_poly d) . i is integer ) ; :: thesis: verum