deffunc H1( 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 S1[ non zero Element of NAT ] means ( ( H1($1) . 0 = 1 or H1($1) . 0 = - 1 ) & ( for i being Element of NAT holds H1($1) . i is integer ) );
A1:
- (1_ F_Complex) = - 1
by COMPLFLD:2, COMPLFLD:8;
A2:
now for k being non zero Element of NAT st ( for n being non zero Element of NAT st n < k holds
S1[n] ) holds
S1[k]let k be non
zero Element of
NAT ;
( ( for n being non zero Element of NAT st n < k holds
S1[n] ) implies S1[b1] )assume A3:
for
n being non
zero Element of
NAT st
n < k holds
S1[
n]
;
S1[b1]A4:
1
<= k
by Lm1;
per cases
( k = 1 or k > 1 )
by A4, XXREAL_0:1;
suppose A6:
k > 1
;
S1[b1]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 = H1(
i) ) )
and A10:
unital_poly (
F_Complex,
k)
= (cyclotomic_poly k) *' p
by Th50;
defpred S2[
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 S3[
Nat]
means ( $1
in Seg (len f) implies ex
x being
object st
S2[$1,
x] );
A11:
k = len f
by A8, FINSEQ_1:def 3;
A12:
for
l being
Nat st
S3[
l] holds
S3[
l + 1]
proof
let l be
Nat;
( S3[l] implies S3[l + 1] )
assume A13:
S3[
l]
;
S3[l + 1]
assume A14:
l + 1
in Seg (len f)
;
ex x being object st S2[l + 1,x]
per cases
( l = 0 or 0 < l )
;
suppose A15:
l = 0
;
ex x being object st S2[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
;
S2[l + 1,p]take
g
;
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
;
( 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 )
;
( ( 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
= H1(1)
by A6, A9, A11, A14, A15;
hence
(
p . 0 = 1 or
p . 0 = - 1 )
by A1, A15, A16, Th48, POLYNOM5:38;
for j being Element of NAT holds p . j is integer let j be
Element of
NAT ;
p . j is integer thus
p . j is
integer
verum end; suppose A18:
0 < l
;
ex x being object st S2[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:
S2[
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
;
S2[l + 1,p1]take
g1
;
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
;
( 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 )
;
( ( 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 ) )
verumproof
per cases
( not l + 1 divides k or l + 1 = k or ( l + 1 divides k & l + 1 <> k ) )
;
suppose
( not
l + 1
divides k or
l + 1
= k )
;
( ( 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 )
for j being Element of NAT holds p1 . j is integer let j be
Element of
NAT ;
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
hence
p1 . j is
integer
by A32, Th4;
verum end; suppose A35:
(
l + 1
divides k &
l + 1
<> k )
;
( ( 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 = H1(
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 )
for j being Element of NAT holds p1 . j is integer let j be
Element of
NAT ;
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
hence
p1 . j is
integer
by A45, Th4;
verum end; end;
end; end; end;
end; defpred S4[
Nat]
means H1(
k)
. $1 is
integer ;
A47:
(0 + 1) -' 1
= 0
by NAT_D:34;
A48:
S3[
0 ]
by FINSEQ_1:1;
for
l being
Nat holds
S3[
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
S2[
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
S2[
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;
A55:
now for m being Nat st ( for n being Nat st n < m holds
S4[n] ) holds
S4[m]let m be
Nat;
( ( for n being Nat st n < m holds
S4[n] ) implies S4[b1] )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)) * (H1(k) . ((m1 + 1) -' l))
by A10, POLYNOM3:def 9;
reconsider Src =
Sum r as
Element of
COMPLEX by COMPLFLD:def 1;
then reconsider Sr =
Src as
Integer ;
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
S4[
n]
;
S4[b1]now 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 let i be
Element of
NAT ;
( i in dom (((1 + 1),(len r)) -cut r) implies (((1 + 1),(len r)) -cut r) . b1 is integer )assume A61:
i in dom (((1 + 1),(len r)) -cut r)
;
(((1 + 1),(len r)) -cut r) . b1 is integer per cases
( len r < 2 or 1 + 1 <= len r )
;
suppose A62:
1
+ 1
<= len r
;
(((1 + 1),(len r)) -cut r) . b1 is integer then A63:
(len (((1 + 1),(len r)) -cut r)) + (1 + 1) = (len r) + 1
by FINSEQ_6:def 4;
per cases
( m = 0 or m > 0 )
;
suppose A64:
m > 0
;
(((1 + 1),(len r)) -cut r) . b1 is integer
i <> 0
by A61, FINSEQ_3:25;
then reconsider cpkmi =
H1(
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)) * (H1(k) . ((m + 1) -' (1 + i)))
by A58
.=
(p . ((i + 1) -' 1)) * (H1(k) . (((m + 1) -' 1) -' i))
by NAT_2:30
.=
(p . i) * (H1(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;
verum end; end; end; end; end; then reconsider Ss =
Ssc as
Integer by Th4;
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)) * (H1(k) . ((m + 1) -' 1))
by A58, A69
.=
(p . 0) * (H1(k) . m1)
by A47, NAT_D:34
;
end; A71:
for
i being
Nat holds
S4[
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)) * (H1(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) * (H1(k) . 0)
by A74, A47, A75
;
(
H1(
k)
. 0 = 1 or
H1(
k)
. 0 = - 1 )
hence
S1[
k]
by A71;
verum end; end; end;
for d being non zero Element of NAT holds S1[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 )
; verum