:: Primitive Roots of Unity and Cyclotomic Polynomials
:: by Broderick Arneson and Piotr Rudnicki
::
:: Received December 30, 2003
:: Copyright (c) 2003-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, XBOOLE_0, XXREAL_0, CARD_1, ARYTM_3, NAT_1,
FINSEQ_1, RELAT_1, FUNCT_1, TARSKI, COMPLFLD, COMPLEX1, PARTFUN1, CARD_3,
STRUCT_0, REAL_1, ORDINAL4, FINSET_1, UPROOTS, ARYTM_1, POLYNOM2,
AFINSQ_1, GROUP_1, INT_1, HAHNBAN1, SQUARE_1, POWER, SIN_COS, BINOP_1,
ALGSTR_0, FINSEQ_2, MOD_2, VECTSP_1, VECTSP_2, REALSET1, ZFMISC_1,
SUPINF_2, COMPTRIG, RAT_1, PREPOWER, NEWTON, XCMPLX_0, INT_2, BINOP_2,
GROUP_2, POLYNOM1, POLYNOM3, FUNCT_4, ALGSEQ_1, VALUED_0, POLYNOM5,
SGRAPH1, PRE_POLY, GRAPH_2, MESFUNC1, UNIROOTS;
notations TARSKI, XBOOLE_0, SUBSET_1, REALSET1, CARD_1, ORDINAL1, NUMBERS,
XREAL_0, ZFMISC_1, XXREAL_0, XCMPLX_0, COMPLEX1, REAL_1, SQUARE_1, INT_1,
INT_2, NAT_D, PREPOWER, POWER, BINOP_1, RELAT_1, FUNCT_1, PARTFUN1,
FUNCT_2, FINSEQ_1, RAT_1, DOMAIN_1, FINSET_1, BINOP_2, RVSUM_1, STRUCT_0,
ALGSTR_0, VECTSP_2, VECTSP_1, GROUP_4, ALGSEQ_1, COMPLFLD, HAHNBAN1,
POLYNOM3, POLYNOM4, POLYNOM5, COMPTRIG, GROUP_2, NEWTON, GROUP_1, MOD_2,
GRAPH_2, PRE_POLY, FVSUM_1, UPROOTS, SIN_COS, FUNCT_7, FINSEQ_2,
FINSEQ_6;
constructors WELLORD2, BINOP_1, REAL_1, SQUARE_1, NAT_D, FINSEQOP, FINSOP_1,
RVSUM_1, PREPOWER, POWER, REALSET1, SIN_COS, GROUP_4, MOD_2, MATRIX_1,
HAHNBAN1, GRAPH_2, POLYNOM4, POLYNOM5, UPROOTS, RECDEF_1, BINOP_2,
RELSET_1, PBOOLE, FUNCT_7, NEWTON, FVSUM_1, ALGSEQ_1, FINSEQ_6;
registrations RELAT_1, FUNCT_1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, NAT_1, INT_1, BINOP_2, CARD_1, MEMBERED, FINSEQ_1, FINSEQ_2,
REALSET1, WSIERP_1, STRUCT_0, GROUP_1, VECTSP_1, COMPLFLD, QUOFIELD,
POLYNOM3, POLYNOM5, VALUED_0, ALGSTR_0, POWER, RELSET_1, PRE_POLY,
PREPOWER, SQUARE_1, NEWTON, SIN_COS, ORDINAL1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions TARSKI, GROUP_1, XBOOLE_0;
equalities GROUP_1, XBOOLE_0, BINOP_1, REALSET1, SQUARE_1, HAHNBAN1, POLYNOM3,
FINSEQ_2, COMPLEX1, GROUP_4, ALGSTR_0, STRUCT_0, POLYNOM5;
expansions TARSKI, GROUP_1, XBOOLE_0;
theorems GROUP_1, CARD_1, FINSEQ_1, ZFMISC_1, NAT_1, FUNCT_1, FUNCT_2,
RELAT_1, TARSKI, XBOOLE_0, XBOOLE_1, VECTSP_1, PREPOWER, COMPTRIG,
COMPLFLD, BINOP_1, XCMPLX_1, COMPLEX1, HAHNBAN1, SIN_COS, POWER,
SIN_COS2, POLYNOM5, INT_1, COMPLEX2, XCMPLX_0, XREAL_0, SQUARE_1,
RVSUM_1, FVSUM_1, FINSEQ_3, FINSEQ_2, FINSEQ_4, POLYNOM4, INT_2,
WSIERP_1, NAT_2, PEPIN, POLYNOM3, COMPUT_1, NORMSP_1, FUNCT_7, ALGSEQ_1,
RLVECT_1, NEWTON, POLYNOM2, MATRIX_3, VECTSP_2, MOD_2, CARD_2, GRAPH_2,
FINSEQ_5, UPROOTS, GROUP_2, BINOP_2, XREAL_1, XXREAL_0, GROUP_4,
FUNCOP_1, ORDINAL1, FINSOP_1, NAT_D, PARTFUN1, PRE_POLY, FINSEQ_6;
schemes NAT_1, FUNCT_2, FINSEQ_1, INT_1, RECDEF_1;
begin :: Preliminaries
Lm1: for k being Element of NAT holds k is non zero iff 1 <= k
proof
let k be Element of NAT;
hereby
assume k is non zero;
then 0+1 <= k by NAT_1:13;
hence 1 <= k;
end;
assume 1 <= k;
hence thesis;
end;
scheme
CompIndNE { P[non zero Nat] } : for k being non zero Element of NAT holds
P[k]
provided
A1: for k being non zero Element of NAT st for n being non zero
Element of NAT st n < k holds P[n] holds P[k]
proof
let k be non zero Element of NAT;
defpred R[Nat] means ex m being non zero Element of NAT st m = $1 & P[m];
A2: now
let k be Nat such that
A3: k>=1 and
A4: for n being Nat st n>=1 & n<k holds R[n];
reconsider m = k as non zero Element of NAT by A3,ORDINAL1:def 12;
now
let n be non zero Element of NAT such that
A5: n < m;
n >= 1 by Lm1;
then R[n] by A4,A5;
hence P[n];
end;
then P[m] by A1;
hence R[k];
end;
A6: for k being Nat st k>=1 holds R[k] from NAT_1:sch 9(A2);
k >= 1 by Lm1;
then ex m being non zero Element of NAT st m = k & P[m] by A6;
hence thesis;
end;
theorem Th1:
for f being FinSequence st 1 <= len f holds f | Seg 1 = <*f.1*>
proof
let f be FinSequence;
assume 1 <= len f;
then Seg 1 c= Seg len f by FINSEQ_1:5;
then
A1: Seg 1 c= dom f by FINSEQ_1:def 3;
reconsider f1 = f | Seg 1 as FinSequence by FINSEQ_1:15;
0+1 in Seg 1 by FINSEQ_1:4;
then
A2: (f | Seg 1).1 = f.1 by FUNCT_1:49;
dom f1 = Seg 1 by A1,RELAT_1:62;
then len f1 = 1 by FINSEQ_1:def 3;
hence thesis by A2,FINSEQ_1:40;
end;
Lm2: for f being FinSequence, n, i being Element of NAT st i <= n holds
(f|Seg n)|Seg i = f|Seg i by FINSEQ_1:5,RELAT_1:74;
theorem Th2:
for f being FinSequence of F_Complex, g being FinSequence of REAL
st len f = len g & for i being Element of NAT st i in dom f holds |. f/.i .| =
g.i holds |. Product f .| = Product g
proof
defpred P[Nat] means for f being FinSequence of F_Complex, g
being FinSequence of REAL st len f = len g & (for i being Element of NAT st
i in dom f holds |. f/.i .| = g.i) & $1 = len f holds
|. Product f .| = Product g;
set FC = F_Complex;
set cFC = the carrier of FC;
A1: for i being Nat st P[i] holds P[i+1]
proof
let i being Nat such that
A2: P[i];
let f be FinSequence of FC, g be FinSequence of REAL such that
A3: len f = len g and
A4: for i being Element of NAT st i in dom f holds |. f/.i .| = g.i and
A5: i+1 = len f;
consider g1 being FinSequence of REAL, r being Element of REAL such that
A6: g = g1^<*r*> by A3,A5,FINSEQ_2:19;
A7: len g = len g1 + len <*r*> by A6,FINSEQ_1:22
.= len g1 + 1 by FINSEQ_1:39;
then
A8: g.len f = r by A3,A6,FINSEQ_1:42;
consider f1 being FinSequence of FC, c being Element of cFC such that
A9: f = f1^<*c*> by A5,FINSEQ_2:19;
A10: len f = len f1 + len <*c*> by A9,FINSEQ_1:22
.= len f1 + 1 by FINSEQ_1:39;
then
A11: dom f1 = dom g1 by A3,A7,FINSEQ_3:29;
A12: now
let i be Element of NAT;
A13: dom f1 c= dom f by A9,FINSEQ_1:26;
assume
A14: i in dom f1;
then f1/.i = f1.i by PARTFUN1:def 6
.= f.i by A9,A14,FINSEQ_1:def 7
.= f/.i by A14,A13,PARTFUN1:def 6;
hence |. f1/.i .| = g.i by A4,A14,A13
.= g1.i by A6,A11,A14,FINSEQ_1:def 7;
end;
reconsider Pf1 = Product f1 as Element of COMPLEX by COMPLFLD:def 1;
A15: Product g = Product g1 * r by A6,RVSUM_1:96;
reconsider cc = c as Element of COMPLEX by COMPLFLD:def 1;
f <> {} by A5;
then
A16: len f in dom f by FINSEQ_5:6;
then f/.len f = f.len f by PARTFUN1:def 6
.= c by A9,A10,FINSEQ_1:42;
then
A17: |.cc.| = r by A4,A16,A8;
Product f = Product f1 * c by A9,GROUP_4:6;
hence |. Product f .| = |. Pf1 .|*|.cc.| by COMPLEX1:65
.= Product g by A2,A3,A5,A15,A10,A7,A12,A17;
end;
A18: P[0]
proof
let f be FinSequence of F_Complex, g be FinSequence of REAL such that
A19: len f = len g and
for i being Element of NAT st i in dom f holds |. f/.i .| = g.i and
A20: 0 = len f;
A21: f = <*>(the carrier of F_Complex) by A20;
then
A22: g = <*>(the carrier of F_Complex) by A19;
Product f = 1r by A21,COMPLFLD:8,GROUP_4:8;
hence thesis by A22,COMPLEX1:48,RVSUM_1:94;
end;
A23: for i being Nat holds P[i] from NAT_1:sch 2(A18,A1);
let f be FinSequence of F_Complex, g be FinSequence of REAL;
assume len f = len g & for i being Element of NAT st i in dom f holds |. f
/.i .| = g.i;
hence thesis by A23;
end;
theorem Th3:
for s being non empty finite Subset of F_Complex, x being Element
of F_Complex, r being FinSequence of REAL st len r = card s & for i being
Element of NAT, c being Element of F_Complex st i in dom r & c = (canFS(s)).i
holds r.i = |.x-c.| holds |.eval(poly_with_roots((s,1)-bag),x).| = Product(r)
proof
set FC = F_Complex;
let s be non empty finite Subset of FC, x being Element of FC, r being
FinSequence of REAL such that
A1: len r = card s and
A2: for i being Element of NAT, c being Element of FC st i in dom r & c
= (canFS(s)).i holds r.i = |.x-c.|;
defpred P[set,set] means ex c being Element of FC st c = (canFS(s)).$1 & $2
= eval(<% -c, 1_F_Complex %>,x);
len canFS(s) = card s by FINSEQ_1:93;
then
A3: dom canFS(s) = Seg card s by FINSEQ_1:def 3;
A4: for k being Nat st k in Seg card s ex y being Element of FC
st P[k,y]
proof
let k be Nat such that
A5: k in Seg card s;
set c = (canFS(s)).k;
c in s by A3,A5,FINSEQ_2:11;
then reconsider c as Element of FC;
reconsider fi = eval(<% -c, 1_F_Complex %>,x) as Element of FC;
take fi, c;
thus thesis;
end;
consider f being FinSequence of FC such that
A6: dom f = Seg card s and
A7: for k being Nat st k in Seg card s holds P[k,f/.k] from
RECDEF_1:sch 17(A4);
A8: now
let i being Element of NAT, c be Element of FC such that
A9: i in dom f and
A10: c = (canFS(s)).i;
ex c1 being Element of FC st c1 = (canFS(s)).i & f/.i = eval(<% -c1,
1_F_Complex %>,x) by A6,A7,A9;
hence f.i = eval(<% -c, 1_F_Complex %>,x) by A9,A10,PARTFUN1:def 6;
end;
A11: dom r = Seg card s by A1,FINSEQ_1:def 3;
A12: for i being Element of NAT st i in dom f holds |. f/.i .| = r.i
proof
let i be Element of NAT;
set c = (canFS(s)).i;
assume
A13: i in dom f;
then c in s by A3,A6,FINSEQ_2:11;
then reconsider c = (canFS(s)).i as Element of FC;
A14: f.i = eval(<% -c, 1_F_Complex %>,x) by A8,A13;
f/.i = f.i by A13,PARTFUN1:def 6
.= -c + x by A14,POLYNOM5:47
.= x-c;
hence thesis by A2,A11,A6,A13;
end;
A15: len f = len r by A1,A6,FINSEQ_1:def 3;
then eval(poly_with_roots((s,1)-bag),x) = Product(f) by A1,A8,UPROOTS:67;
hence thesis by A15,A12,Th2;
end;
theorem Th4:
for f being FinSequence of F_Complex st for i being Element of
NAT st i in dom f holds f.i is integer holds Sum f is integer
proof
set FC = F_Complex;
let f be FinSequence of FC;
assume
A1: for i being Element of NAT st i in dom f holds f.i is integer;
defpred P[Nat] means for f being FinSequence of FC st len f = $1
& for i being Element of NAT st i in dom f holds f.i is integer holds Sum f is
integer;
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
A3: P[n];
let f being FinSequence of FC;
assume that
A4: len f = n+1 and
A5: for i being Element of NAT st i in dom f holds f.i is integer;
consider g being FinSequence of FC, c being Element of FC such that
A6: f = g^<*c*> by A4,FINSEQ_2:19;
A7: now
let i be Element of NAT;
A8: dom g c= dom f by A6,FINSEQ_1:26;
assume
A9: i in dom g;
then f.i = g.i by A6,FINSEQ_1:def 7;
hence g.i is integer by A5,A9,A8;
end;
0+1 <= len f by A4,NAT_1:13;
then len f in dom f by FINSEQ_3:25;
then
A10: f.(len f) is integer by A5;
reconsider Sgc = Sum g, cc = c as Element of COMPLEX by COMPLFLD:def 1;
len f = len g + len <*c*> by A6,FINSEQ_1:22
.= len g +1 by FINSEQ_1:40;
then reconsider Sgi = Sgc, ci = cc as Integer by A3,A4,A6,A7,A10,
FINSEQ_1:42;
Sum f = Sum g + Sum <*c*> by A6,RLVECT_1:41
.= Sgi + ci by RLVECT_1:44;
hence thesis;
end;
A11: len f is Element of NAT;
A12: P[0]
proof
let f be FinSequence of FC;
assume len f = 0;
then f = <*>(the carrier of F_Complex);
hence thesis by COMPLFLD:7,RLVECT_1:43;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A12,A2);
hence thesis by A1,A11;
end;
theorem
for x, y being Element of F_Complex, r1, r2 being Real st r1=x & r2=y
holds r1*r2 = x*y & r1+r2=x+y;
theorem Th6:
for q being Real st q > 0 for r being Element of F_Complex st |.r
.| = 1 & r <> [**1,0**] holds |.[**q, 0**] - r.| > q - 1
proof
let q be Real such that
A1: q > 0;
let r be Element of F_Complex such that
A2: |.r.| = 1 and
A3: r <> [**1,0**];
set b = Im r;
set a = Re r;
A4: a^2 + b^2 = 1^2 by A2,COMPTRIG:3;
A5: now
assume
A6: a = 1;
then b = 0 by A4;
hence contradiction by A3,A6,COMPLEX1:13;
end;
a <= 1 by A2,COMPLEX1:54;
then a < 1 by A5,XXREAL_0:1;
then 2*q > 2*q*a by A1,XREAL_1:157;
then -2*q*a > -2*q by XREAL_1:24;
then -2*q + q^2 < -2*q*a + q^2 by XREAL_1:8;
then
A7: q^2 - 2*q*a + 1 > q^2 - 2*q + 1 by XREAL_1:8;
reconsider qc = [**q, 0**] as Element of F_Complex;
A8: Re[**q-a,-b**] = q-a & Im[**q-a,-b**] = -b by COMPLEX1:12;
(|.qc - r.|)^2 = |.[**q, 0**] - [**a, b**].|^2 by COMPLEX1:13
.= |.[**q - a, 0-b**].|^2
.= (q-a)^2 + b^2 by A8,COMPTRIG:3
.= q^2 - 2*q*a + 1 by A4;
then |.qc - r.| >= 0 & (|.qc - r.|)^2 > (q - 1)^2 by A7,COMPLEX1:46;
hence thesis by SQUARE_1:48;
end;
theorem Th7:
for ps being non empty FinSequence of REAL, x being Real st x >=
1 & for i being Element of NAT st i in dom ps holds ps.i > x holds Product(ps)
> x
proof
let ps be non empty FinSequence of REAL, x be Real such that
A1: x >= 1 and
A2: for j being Element of NAT st j in dom ps holds ps.j > x;
consider ps1 being FinSequence, y being object such that
A3: ps = ps1^<*y*> by FINSEQ_1:46;
<*y*> is FinSequence of REAL by A3,FINSEQ_1:36;
then rng <*y*> c= REAL by FINSEQ_1:def 4;
then {y} c= REAL by FINSEQ_1:38;
then reconsider y2=y as Element of REAL by ZFMISC_1:31;
defpred P[Nat] means for f being FinSequence of REAL st len f =
$1 & for j being Element of NAT st j in dom f holds f.j > x holds Product(f)*y2
> x;
A4: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A5: P[k];
let f be FinSequence of REAL such that
A6: len f = k+1 and
A7: for j being Element of NAT st j in dom f holds f.j > x;
f <> {} by A6;
then consider v being FinSequence, w being object such that
A8: f=v^<*w*> by FINSEQ_1:46;
reconsider f1=v, f2=<*w*> as FinSequence of REAL by A8,FINSEQ_1:36;
rng f2 c= REAL;
then {w} c= REAL by FINSEQ_1:38;
then reconsider m=w as Element of REAL by ZFMISC_1:31;
k + 1 = len f1 + len f2 by A6,A8,FINSEQ_1:22;
then
A9: k + 1 = len f1 + 1 by FINSEQ_1:39;
then
A10: f.(len f) = m by A6,A8,FINSEQ_1:42;
len f in Seg len f by A6,FINSEQ_1:3;
then
A11: len f in dom f by FINSEQ_1:def 3;
then m > 1 by A1,A7,A10,XXREAL_0:2;
then
A12: x*m > x by A1,XREAL_1:155;
A13: for j being Element of NAT st j in dom f1 holds f1.j > x
proof
A14: dom f1 c= dom f by A8,FINSEQ_1:26;
let j be Element of NAT such that
A15: j in dom f1;
f.j = f1.j by A8,A15,FINSEQ_1:def 7;
hence thesis by A7,A15,A14;
end;
Product f = Product f1 * m by A8,RVSUM_1:96;
then
A16: Product f*y2 = (Product f1 * y2) * m;
m > x by A7,A10,A11;
then Product f*y2 > x*m by A1,A5,A9,A13,A16,XREAL_1:68;
hence thesis by A12,XXREAL_0:2;
end;
len ps in Seg len ps by FINSEQ_1:3;
then
A17: len ps in dom ps by FINSEQ_1:def 3;
reconsider q=ps1 as FinSequence of REAL by A3,FINSEQ_1:36;
A18: for j being Element of NAT st j in dom q holds q.j > x
proof
A19: dom q c= dom ps by A3,FINSEQ_1:26;
let j be Element of NAT such that
A20: j in dom q;
ps.j = q.j by A3,A20,FINSEQ_1:def 7;
hence thesis by A2,A20,A19;
end;
A21: len q = len q;
len ps = len ps1 + len <*y*> by A3,FINSEQ_1:22;
then len ps = len ps1 + 1 by FINSEQ_1:39;
then
A22: ps.(len ps) = y2 by A3,FINSEQ_1:42;
A23: P[0]
proof
let f be FinSequence of REAL such that
A24: len f = 0 and
for j being Element of NAT st j in dom f holds f.j > x;
f = <*>REAL by A24;
then Product f = 1 by RVSUM_1:94;
hence thesis by A2,A22,A17;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A23,A4);
then Product(q)*y2 > x by A18,A21;
hence thesis by A3,RVSUM_1:96;
end;
theorem Th8:
for n being Element of NAT holds 1_F_Complex = (power F_Complex)
.(1_F_Complex,n)
proof
let n be Element of NAT;
1_F_Complex = [** 1, 0 **] by COMPLFLD:8;
then (power F_Complex).(1_F_Complex,n) = [** 1 to_power n,0 **] by
HAHNBAN1:29
.= 1_F_Complex by COMPLFLD:8;
hence thesis;
end;
theorem Th9:
for n, i being Nat holds cos((2*PI*i)/n) = cos((2*PI*
(i mod n))/n) & sin((2*PI*i)/n) = sin((2*PI*(i mod n))/n)
proof
let n, i be Nat;
set j = i div n;
per cases;
suppose
A1: n <> 0;
then i = n*j + (i mod n) by NAT_D:2;
then
A2: (2*PI*i)/n = (2*PI*(n*j) + 2*PI*(i mod n))/n
.= (2*PI*(n*j))/(n*1) + (2*PI*(i mod n))/n by XCMPLX_1:62
.= (2*PI)/n*(n*j)/1 + (2*PI*(i mod n))/n by XCMPLX_1:83
.= (2*PI)*(1/n)*(n*j) + (2*PI*(i mod n))/n by XCMPLX_1:99
.= (2*PI)*((1/n)*(j*n)) + (2*PI*(i mod n))/n
.= (2*PI)*(j*1) + (2*PI*(i mod n))/n by A1,XCMPLX_1:90
.= 2*PI*j + (2*PI*(i mod n))/n;
then
A3: sin((2*PI*i)/n) = (sin(2*PI*j + 0)) * (cos((2*PI*(i mod n))/n)) + (cos
(2*PI*j + 0)) * (sin((2*PI*(i mod n))/n)) by SIN_COS:75
.= (sin.(2*PI*j + 0)) * (cos((2*PI*(i mod n))/n)) + (cos(2*PI*j + 0))
* (sin((2*PI*(i mod n))/n)) by SIN_COS:def 17
.= (sin.(2*PI*j + 0)) * (cos((2*PI*(i mod n))/n)) + (cos.(2*PI*j + 0))
* (sin((2*PI*(i mod n))/n)) by SIN_COS:def 19
.= (sin.0) * (cos((2*PI*(i mod n))/n)) + (cos.(2*PI*j + 0)) * (sin((2*
PI*(i mod n))/n)) by SIN_COS2:10
.= (sin.0) * (cos((2*PI*(i mod n))/n)) + (cos.0) * (sin((2*PI*(i mod n
))/n)) by SIN_COS2:11
.= sin((2*PI*(i mod n))/n) by SIN_COS:30;
cos((2*PI*i)/n) = (cos(2*PI*j + 0)) * (cos((2*PI*(i mod n))/n)) - (sin
(2*PI*j + 0)) * (sin((2*PI*(i mod n))/n)) by A2,SIN_COS:75
.= (cos.(2*PI*j + 0)) * (cos((2*PI*(i mod n))/n)) - (sin(2*PI*j + 0))
* (sin((2*PI*(i mod n))/n)) by SIN_COS:def 19
.= (cos.(2*PI*j + 0)) * (cos((2*PI*(i mod n))/n)) - (sin.(2*PI*j + 0))
* (sin((2*PI*(i mod n))/n)) by SIN_COS:def 17
.= (cos.0) * (cos((2*PI*(i mod n))/n)) - (sin.(2*PI*j + 0)) * (sin((2*
PI*(i mod n))/n)) by SIN_COS2:11
.= (cos.0) * (cos((2*PI*(i mod n))/n)) - (sin.0) * (sin((2*PI*(i mod n
))/n)) by SIN_COS2:10
.= cos((2*PI*(i mod n))/n) by SIN_COS:30;
hence thesis by A3;
end;
suppose
A4: n = 0;
then (2*PI*i)/n = 0 by XCMPLX_1:49;
hence thesis by A4,XCMPLX_1:49;
end;
end;
theorem Th10:
for n, i being Nat holds [** cos((2*PI*i)/n), sin((2*
PI*i)/n)**] = [** cos((2*PI*(i mod n))/n), sin((2*PI*(i mod n))/n) **]
proof
let n, i be Nat;
[** cos((2*PI*i)/n), sin((2*PI*i)/n)**] = [** cos((2*PI*(i mod n))/n),
sin((2*PI*i)/n)**] by Th9
.= [** cos((2*PI*(i mod n))/n), sin((2*PI*(i mod n))/n) **] by Th9;
hence thesis;
end;
theorem Th11:
for n, i, j being Element of NAT holds [** cos((2*PI*i)/n),sin((
2*PI*i)/n) **]*[** cos((2*PI*j)/n),sin((2*PI*j)/n) **] = [** cos((2*PI*((i+j)
mod n))/n), sin((2*PI*((i+j)mod n))/n)**]
proof
let n, i, j be Element of NAT;
(2*PI*i)/n + (2*PI*j)/n = (2*PI*i + 2*PI*j)/n by XCMPLX_1:62
.= (2*PI*(i+j))/n;
then
cos((2*PI*i)/n) * cos((2*PI*j)/n) - sin((2*PI*i)/n) * sin((2*PI*j)/n ) =
cos( (2*PI*(i+j))/n) & cos((2*PI*i)/n) * sin((2*PI*j)/n) + cos((2*PI*j)/n) *
sin((2 *PI*i)/n) = sin((2*PI*(i+j))/n) by SIN_COS:75;
then
[** cos((2*PI*i)/n), sin((2*PI*i)/n) **] * [** cos((2*PI*j)/n), sin((2*
PI*j)/n) **] = [** cos((2*PI*(i+j))/n), sin((2*PI*(i+j))/n) **]
.= [** cos((2*PI*((i+j) mod n))/n), sin((2*PI*((i+j) mod n))/n)**] by Th10;
hence thesis;
end;
theorem Th12:
for L being unital associative non empty multMagma, x being
Element of L, n,m being Nat holds (power L).(x,n*m) = (power L).((
power L).(x,n),m)
proof
let L be unital associative non empty multMagma, x be Element of L,
n be Nat;
defpred P[Nat] means (power L).(x,n*$1) = (power L).((power L).(x,n),$1);
set pL = power L;
reconsider nn= n as Element of NAT by ORDINAL1:def 12;
A1: for m being Nat st P[m] holds P[m+1]
proof
let m be Nat such that
A2: P[m];
reconsider nm= n*m, mm = m as Element of NAT by ORDINAL1:def 12;
pL.(x,n*(m+1)) = pL.(x,n*m+n*1) .= pL.(x,nm)*pL.(x,nn) by POLYNOM2:1
.= pL.(pL.(x,nn),mm+1) by A2,GROUP_1:def 7;
hence thesis;
end;
pL.(x,n*(0 qua Nat)) = 1_L by GROUP_1:def 7
.= pL.(pL.(x,nn),0) by GROUP_1:def 7;
then
A3: P[0];
thus for m being Nat holds P[m] from NAT_1:sch 2(A3,A1);
end;
theorem Th13:
for n being Element of NAT, x being Element of F_Complex st x is
Integer holds (power F_Complex).(x,n) is Integer
proof
let n be Element of NAT, x be Element of F_Complex such that
A1: x is Integer;
defpred P[Nat] means (power F_Complex).(x,$1) is Integer;
A2: now
reconsider i1=x as Integer by A1;
let k be Nat;
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
assume P[k];
then reconsider i2=(power F_Complex).(x,k) as Integer;
(power F_Complex).(x,kk)*x = i1*i2;
hence P[k+1] by GROUP_1:def 7;
end;
A3: P[0] by COMPLFLD:8,GROUP_1:def 7;
for k being Nat holds P[k] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
theorem Th14:
for F being FinSequence of F_Complex st for i being Element of
NAT st i in dom F holds F.i is Integer holds Sum F is Integer
proof
defpred P[Nat] means for F being FinSequence of F_Complex st len
F = $1 & for i being Element of NAT st i in dom F holds F.i is Integer holds
Sum F is Integer;
let G be FinSequence of F_Complex such that
A1: for i being Element of NAT st i in dom G holds G.i is Integer;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A3: P[k];
let F be FinSequence of F_Complex such that
A4: len F = k+1 and
A5: for i being Element of NAT st i in dom F holds F.i is Integer;
F <> {} by A4;
then consider G being FinSequence, x being object such that
A6: F = G^<*x*> by FINSEQ_1:46;
len F in Seg len F by A4,FINSEQ_1:3;
then
A7: len F in dom F by FINSEQ_1:def 3;
reconsider f2=<*x*> as FinSequence of F_Complex by A6,FINSEQ_1:36;
reconsider f1=G as FinSequence of F_Complex by A6,FINSEQ_1:36;
rng f2 c= the carrier of F_Complex by FINSEQ_1:def 4;
then {x} c= the carrier of F_Complex by FINSEQ_1:38;
then reconsider m=x as Element of F_Complex by ZFMISC_1:31;
k + 1 = len f1 + len f2 by A4,A6,FINSEQ_1:22;
then
A8: k + 1 = len f1 + 1 by FINSEQ_1:39;
then F.(len F) = m by A4,A6,FINSEQ_1:42;
then reconsider i2 = m as Integer by A5,A7;
for j being Element of NAT st j in dom f1 holds f1.j is Integer
proof
A9: dom f1 c= dom F by A6,FINSEQ_1:26;
let j be Element of NAT such that
A10: j in dom f1;
F.j = f1.j by A6,A10,FINSEQ_1:def 7;
hence thesis by A5,A10,A9;
end;
then reconsider i1 = Sum f1 as Integer by A3,A8;
Sum F = Sum f1 + m by A6,FVSUM_1:71;
then Sum F = i1 + i2;
hence thesis;
end;
A11: P[0]
proof
let F be FinSequence of F_Complex such that
A12: len F = 0 and
for i being Element of NAT st i in dom F holds F.i is Integer;
0-tuples_on the carrier of F_Complex = {{}} & F = {} by A12,COMPUT_1:5;
then F is Element of 0-tuples_on the carrier of F_Complex by TARSKI:def 1;
hence thesis by COMPLFLD:7,FVSUM_1:74;
end;
A13: for k being Nat holds P[k] from NAT_1:sch 2(A11,A2);
len G = len G;
hence thesis by A1,A13;
end;
Lm3: Z_3 is finite by MOD_2:def 20;
registration
cluster finite for Field;
existence by Lm3,MOD_2:27;
cluster finite for Skew-Field;
existence by Lm3,MOD_2:27;
end;
begin :: Multiplicative group of a skew field
definition
let R be Skew-Field;
func MultGroup R -> strict Group means
:Def1:
the carrier of it = NonZero R
& the multF of it = (the multF of R)||the carrier of it;
existence
proof
set ccs = NonZero R;
set cR = the carrier of R;
reconsider ccs as non empty set;
set mcs = (the multF of R)||ccs;
[:ccs,ccs:] c= [:cR,cR:]
proof
let x be object;
assume x in [:ccs,ccs:];
then ex a,b being object st a in ccs & b in ccs & x =[a,b]
by ZFMISC_1:def 2;
hence thesis by ZFMISC_1:def 2;
end;
then reconsider mcs as Function of [:ccs,ccs:],cR by FUNCT_2:32;
rng mcs c= ccs
proof
let y be object;
assume y in rng mcs;
then consider x being object such that
A1: x in dom mcs and
A2: y = mcs.x by FUNCT_1:def 3;
A3: dom mcs = [:ccs,ccs:] by FUNCT_2:def 1;
then consider a,b being object such that
A4: a in ccs and
A5: b in ccs and
A6: x = [a,b] by A1,ZFMISC_1:def 2;
reconsider a,b as Element of cR by A4,A5;
not b in {0.R} by A5,XBOOLE_0:def 5;
then
A7: b <> 0.R by TARSKI:def 1;
not a in {0.R} by A4,XBOOLE_0:def 5;
then a <> 0.R by TARSKI:def 1;
then a*b <> 0.R by A7,VECTSP_2:12;
then
A8: not a*b in {0.R} by TARSKI:def 1;
mcs.x = a*b by A1,A3,A6,FUNCT_1:49;
hence thesis by A2,A8,XBOOLE_0:def 5;
end;
then reconsider mcs as BinOp of ccs by FUNCT_2:6;
reconsider cs = multMagma (# ccs, mcs #) as non empty multMagma;
set ccs1 = the carrier of cs;
A9: now
let a,b be Element of cR, c,d be Element of ccs1 such that
A10: a=c & b=d;
[c,d] in [:ccs,ccs:] by ZFMISC_1:def 2;
hence a*b= c*d by A10,FUNCT_1:49;
end;
A11: not 1_R in {0.R} by TARSKI:def 1;
A12: cs is Group-like
proof
reconsider e = 1_R as Element of ccs1 by A11,XBOOLE_0:def 5;
take e;
let h be Element of ccs1;
h in ccs;
then reconsider h9=h as Scalar of R;
thus h * e = h9*(1_R) by A9
.= h;
thus e * h = (1_R)*h9 by A9
.= h;
not h in {0.R} by XBOOLE_0:def 5;
then
A13: h <> 0.R by TARSKI:def 1;
then h9" <> 0.R by VECTSP_2:13;
then not h9" in {0.R} by TARSKI:def 1;
then reconsider g=h9" as Element of ccs1 by XBOOLE_0:def 5;
take g;
thus h * g = h9*h9" by A9
.= e by A13,VECTSP_2:9;
thus g * h = h9"*h9 by A9
.= e by A13,VECTSP_2:9;
end;
cs is associative
proof
let x,y,z be Element of ccs1;
A14: z in ccs1;
x in ccs1 & y in ccs1;
then reconsider x9=x,y9=y,z9=z as Element of cR by A14;
A15: y9*z9=y*z by A9;
x9*y9=x*y by A9;
hence (x*y)*z = (x9*y9)*z9 by A9
.= x9*(y9*z9) by GROUP_1:def 3
.= x*(y*z) by A9,A15;
end;
hence thesis by A12;
end;
uniqueness;
end;
theorem :: WEDDWITT
for R being Skew-Field holds the carrier of R = (the carrier of
MultGroup R) \/ {0.R}
proof
let R being Skew-Field;
NonZero R = the carrier of MultGroup R by Def1;
hence thesis by XBOOLE_1:45;
end;
theorem Th16:
for R being Skew-Field, a, b being Element of R, c, d being
Element of MultGroup R st a = c & b = d holds c*d = a*b
proof
let R be Skew-Field, a, b be Element of R, c,d be Element of MultGroup R
such that
A1: a = c & b = d;
set cMGR = the carrier of MultGroup R;
A2: [c,d] in [:cMGR,cMGR:] by ZFMISC_1:def 2;
thus c*d = ((the multF of R)||cMGR).(c,d) by Def1
.= a*b by A1,A2,FUNCT_1:49;
end;
theorem Th17:
for R being Skew-Field holds 1_R = 1_MultGroup R
proof
let R be Skew-Field;
A1: the carrier of MultGroup R = NonZero R by Def1;
not 1_R in {0.R} by TARSKI:def 1;
then reconsider uR = 1_R as Element of MultGroup R by A1,XBOOLE_0:def 5;
now
let h be Element of MultGroup R;
reconsider g = h as Element of R by A1,XBOOLE_0:def 5;
g * 1_R = g;
hence h * uR = h by Th16;
1_R * g = g;
hence uR * h = h by Th16;
end;
hence thesis by GROUP_1:def 4;
end;
registration
let R be finite Skew-Field;
cluster MultGroup R -> finite;
correctness
proof
the carrier of MultGroup R = NonZero R by Def1;
hence thesis;
end;
end;
theorem :: WEDDWITT
for R being finite Skew-Field holds card MultGroup R = card R - 1
proof
let R be finite Skew-Field;
set G = MultGroup R;
the carrier of G = NonZero R by Def1;
then card the carrier of G = card R - card {0.R} by CARD_2:44;
hence thesis by CARD_1:30;
end;
theorem Th19:
for R being Skew-Field, s being set st s in the carrier of
MultGroup R holds s in the carrier of R
proof
let R be Skew-Field, s be set;
assume s in the carrier of MultGroup R;
then s in NonZero R by Def1;
hence thesis;
end;
theorem
for R being Skew-Field holds the carrier of MultGroup R c= the carrier of R
proof
let R be Skew-Field, s be object;
assume s in the carrier of MultGroup R;
then s in NonZero R by Def1;
hence thesis;
end;
begin :: Roots of 1
definition
let n be non zero Element of NAT;
func n-roots_of_1 -> Subset of F_Complex equals
{ x where x is Element of
F_Complex : x is CRoot of n,1_F_Complex };
coherence
proof
set H = { x where x is Element of F_Complex : x is CRoot of n,1_F_Complex
};
for x being object st x in H holds x in the carrier of F_Complex
proof
let x be object;
assume x in H;
then
ex y being Element of F_Complex st y=x & y is CRoot of n,1_F_Complex;
hence thesis;
end;
hence thesis by TARSKI:def 3;
end;
end;
theorem Th21:
for n being non zero Element of NAT, x being Element of
F_Complex holds x in n-roots_of_1 iff x is CRoot of n,1_F_Complex
proof
let n be non zero Element of NAT, x be Element of F_Complex;
hereby
assume x in n-roots_of_1;
then ex y being Element of F_Complex st y=x & y is CRoot of n, 1_F_Complex;
hence x is CRoot of n,1_F_Complex;
end;
thus thesis;
end;
theorem Th22:
for n being non zero Element of NAT holds 1_F_Complex in n -roots_of_1
proof
let n be non zero Element of NAT;
1_F_Complex = (power F_Complex).(1_F_Complex,n) by Th8;
then 1_F_Complex is CRoot of n,1_F_Complex by COMPLFLD:def 2;
hence thesis;
end;
theorem Th23:
for n being non zero Element of NAT, x being Element of
F_Complex st x in n-roots_of_1 holds |.x.| = 1
proof
let n be non zero Element of NAT, x be Element of F_Complex such that
A1: x in n-roots_of_1;
A2: now
assume x = 0.F_Complex;
then (power F_Complex).(x,n) <> 1_F_Complex by VECTSP_1:36;
then not x is CRoot of n, 1_F_Complex by COMPLFLD:def 2;
hence contradiction by A1,Th21;
end;
then
A3: |.x.| > 0 by COMPLFLD:59;
x is CRoot of n,(1_F_Complex) by A1,Th21;
then power(x,n) = 1_F_Complex by COMPLFLD:def 2;
then
A4: 1 = |.x.| to_power n by A2,COMPLFLD:60,POLYNOM5:7;
assume
A5: |.x.| <> 1;
per cases by A5,XXREAL_0:1;
suppose
A6: |.x.| < 1;
reconsider n9 = n as Rational;
|.x.| #Q n9 < 1 by A3,A6,PREPOWER:65;
hence contradiction by A4,A3,PREPOWER:49;
end;
suppose
|.x.| > 1;
hence contradiction by A4,POWER:35;
end;
end;
theorem Th24:
for n being non zero Element of NAT for x being Element of
F_Complex holds x in n-roots_of_1 iff ex k being Element of NAT st x = [** cos(
(2*PI*k)/n), sin((2*PI*k)/n) **]
proof
let n be non zero Element of NAT, x be Element of F_Complex;
hereby
assume
A1: x in n-roots_of_1;
A2: now
assume x = 0.F_Complex;
then (power F_Complex).(x,n) <> 1_F_Complex by VECTSP_1:36;
then not x is CRoot of n, 1_F_Complex by COMPLFLD:def 2;
hence contradiction by A1,Th21;
end;
then 0 <= Arg x & Arg x < 2*PI by COMPLFLD:7,COMPTRIG:def 1;
then
A3: 0+-1 <= (n*Arg x)/(2*PI) +-1 by XREAL_1:7;
x is CRoot of n,(1_F_Complex) by A1,Th21;
then power(x,n) = 1_F_Complex by COMPLFLD:def 2;
then
A4: 1 = |.x.| to_power n by A2,COMPLFLD:60,POLYNOM5:7;
A5: now
A6: |.x.| > 0 by A2,COMPLFLD:59;
assume
A7: |.x.| <> 1;
per cases by A7,XXREAL_0:1;
suppose
A8: |.x.| < 1;
reconsider n9 = n as Rational;
|.x.| #Q n9 < 1 by A6,A8,PREPOWER:65;
hence contradiction by A4,A6,PREPOWER:49;
end;
suppose
|.x.| > 1;
hence contradiction by A4,POWER:35;
end;
end;
set m2 = [\ ((n*Arg x)/(2*PI))/];
reconsider z = x as Element of COMPLEX by XCMPLX_0:def 2;
consider r being Real such that
A9: r = (2*PI) * (-[\ ((n*Arg x)/(2*PI)) /]) + (n*Arg x) and
A10: 0 <= r & r < (2*PI) by COMPLEX2:1,COMPTRIG:5;
(n*Arg x)/(2*PI)-1 < m2 by INT_1:def 6;
then not m2 <= -1 by A3,XXREAL_0:2;
then -1+1 <= m2 by INT_1:7;
then reconsider m = [\ ((n*Arg x)/(2*PI)) /] as Element of NAT by INT_1:3;
A11: cos(n*Arg x) = cos.(2*PI*m + r) by A9,SIN_COS:def 19
.= cos.(r) by SIN_COS2:11
.= cos(r) by SIN_COS:def 19;
A12: sin(n*Arg x) = sin.(2*PI*m + r) by A9,SIN_COS:def 17
.= sin.(r) by SIN_COS2:10
.= sin(r) by SIN_COS:def 17;
x is CRoot of n,(1_F_Complex) by A1,Th21;
then (power F_Complex).(x,n) = [** 1, 0 **] by COMPLFLD:8,def 2;
then
A13: z|^n = (|.z.| |^ n)*cos (n*Arg z)+(|.z.| |^ n)*sin (n*Arg z)*<i> & z
|^n = [** 1, 0 **] by COMPLFLD:74,COMPTRIG:54;
then sin(n*Arg x) = 0 by A4,COMPLEX1:77;
then r = 0 or r = PI by A10,A12,COMPTRIG:17;
then (n*Arg x)/(n *1) = (2*PI*m)/n by A4,A13,A9,A11,COMPLEX1:77,SIN_COS:77;
then ((n/n)*Arg x)/1 = (2*PI*m)/n by XCMPLX_1:83;
then
A14: (Arg x)/1 = (2*PI*m)/n by XCMPLX_1:88;
x = [**|.x.|*cos (Arg x),|.x.|*sin (Arg x)**] by A2,COMPLFLD:7
,COMPTRIG:def 1;
hence ex k being Element of NAT st x=[**cos((2*PI*k)/n),sin((2*PI*k)/n)**]
by A5,A14;
end;
now
reconsider z = 1_F_Complex as Element of COMPLEX by XCMPLX_0:def 2;
set 1F = Arg 1_F_Complex;
given k being Element of NAT such that
A15: x = [**cos((2*PI*k)/n),sin((2*PI*k)/n)**];
x = (n-root |.z.|) * cos((1F + 2*PI*k)/n) + (n-root |.z.|) * sin((1F
+ 2*PI*k)/n) *<i> by A15,COMPLFLD:8,60,COMPTRIG:39;
then x is CRoot of n,z by COMPTRIG:57;
hence x in n-roots_of_1;
end;
hence thesis;
end;
theorem Th25:
for n being non zero Element of NAT for x,y being Element of
COMPLEX st x in n-roots_of_1 & y in n-roots_of_1 holds x*y in n-roots_of_1
proof
let n be non zero Element of NAT;
let x,y be Element of COMPLEX such that
A1: x in n-roots_of_1 and
A2: y in n-roots_of_1;
reconsider a=x as Element of F_Complex by COMPLFLD:def 1;
consider i being Element of NAT such that
A3: a = [** cos((2*PI*i)/n), sin((2*PI*i)/n) **] by A1,Th24;
reconsider b=y as Element of F_Complex by COMPLFLD:def 1;
consider j being Element of NAT such that
A4: b = [** cos((2*PI*j)/n), sin((2*PI*j)/n) **] by A2,Th24;
a*b=[** cos((2*PI*((i+j) mod n))/n),sin((2*PI*((i+j)mod n))/n)**] by A3,A4
,Th11;
hence thesis by Th24;
end;
theorem Th26:
for n being non zero Element of NAT holds n-roots_of_1 = {[**
cos((2*PI*k)/n),sin((2*PI*k)/n)**] where k is Element of NAT: k < n }
proof
let n be non zero Element of NAT;
set X={[**cos((2*PI*k)/n),sin((2*PI*k)/n)**] where k is Element of NAT: k <
n };
now
let x be object;
hereby
assume
A1: x in n-roots_of_1;
then reconsider a=x as Element of F_Complex;
consider k being Element of NAT such that
A2: a = [** cos((2*PI*k)/n), sin((2*PI*k)/n) **] by A1,Th24;
A3: k mod n < n by NAT_D:1;
a = [** cos((2*PI*(k mod n))/n), sin((2*PI*(k mod n))/n) **] by A2,Th10;
hence x in X by A3;
end;
assume x in X;
then
ex k being Element of NAT st x = [**cos((2*PI*k)/n),sin((2*PI*k)/n)**]
& k < n;
hence x in n-roots_of_1 by Th24;
end;
hence thesis by TARSKI:2;
end;
theorem Th27:
for n being non zero Element of NAT holds card (n-roots_of_1) = n
proof
let n be non zero Element of NAT;
set X = {[**cos((2*PI*k)/n),sin((2*PI*k)/n)**] where k is Element of NAT: k
< n };
defpred P[object, object] means
ex j being Element of NAT st j=$1 & $2=[**cos((2*
PI*(j-'1))/n),sin((2*PI*(j-'1))/n)**];
A1: X = n-roots_of_1 by Th26;
[**cos((2*PI*(0 qua Nat))/n),sin((2*PI*(0 qua Nat))/n)**] in X;
then reconsider Y = X as non empty set;
A2: for x being object st x in Seg n ex y being object st y in Y & P[x,y]
proof
let x be object such that
A3: x in Seg n;
reconsider a=x as Element of NAT by A3;
a <= n by A3,FINSEQ_1:1;
then a < n+1 by NAT_1:13;
then
A4: a-1 < n+1-1 by XREAL_1:14;
consider b being Element of NAT such that
A5: b = a-'1;
1 <= a by A3,FINSEQ_1:1;
then a-'1 < n by A4,XREAL_1:233;
then [**cos((2*PI*b)/n),sin((2*PI*b)/n)**] in X by A5;
hence thesis by A5;
end;
consider F being Function of Seg n, Y such that
A6: for x being object st x in Seg n holds P[x,F.x] from FUNCT_2:sch 1(A2);
for c being object st c in X ex x being object st x in Seg n & c = F.x
proof
let c be object;
assume c in X;
then consider k being Element of NAT such that
A7: c = [**cos((2*PI*k)/n),sin((2*PI*k)/n)**] and
A8: k < n;
A9: k+1-'1 = k by NAT_D:34;
0+1<=k+1 & k+1 <= n by A8,INT_1:7;
then
A10: k+1 in Seg n by FINSEQ_1:1;
then
ex j being Element of NAT st j=k+1 & F.(k+1) = [**cos((2 *PI*(j-'1))/n
),sin((2*PI*(j-'1))/n)**] by A6;
hence thesis by A7,A10,A9;
end;
then
A11: rng F = X by FUNCT_2:10;
A12: dom F = Seg n by FUNCT_2:def 1;
for x1,x2 being object st x1 in dom F & x2 in dom F & F.x1=F.x2 holds x1= x2
proof
let x1,x2 be object such that
A13: x1 in dom F and
A14: x2 in dom F and
A15: F.x1 = F.x2;
A16: x1 in Seg n by A13,FUNCT_2:def 1;
then consider j being Element of NAT such that
A17: j=x1 and
A18: F.x1 = [**cos((2*PI*(j-'1))/n),sin((2*PI*(j-'1))/n)**] by A6;
set a1 = (2*PI*(j-'1))/n;
A19: 1 <= j by A16,A17,FINSEQ_1:1;
j <= n by A16,A17,FINSEQ_1:1;
then j-1 < n by XREAL_1:146,XXREAL_0:2;
then j-'1 < n by A19,XREAL_1:233;
then (j-'1)/n < n/n by XREAL_1:74;
then (j-'1)/n < 1 by XCMPLX_1:60;
then (j-'1)/n*(2*PI) < 1*(2*PI) by COMPTRIG:5,XREAL_1:68;
then
A20: a1 < 2*PI by XCMPLX_1:74;
A21: x2 in Seg n by A14,FUNCT_2:def 1;
then consider k being Element of NAT such that
A22: k=x2 and
A23: F.x2 = [**cos((2*PI*(k-'1))/n),sin((2*PI*(k-'1))/n)**] by A6;
set a2 = (2*PI*(k-'1))/n;
A24: 1 <= k by A21,A22,FINSEQ_1:1;
k <= n by A21,A22,FINSEQ_1:1;
then k-1 < n by XREAL_1:146,XXREAL_0:2;
then k-'1 < n by A24,XREAL_1:233;
then (k-'1)/n < n/n by XREAL_1:74;
then (k-'1)/n < 1 by XCMPLX_1:60;
then (k-'1)/n*(2*PI) < 1*(2*PI) by COMPTRIG:5,XREAL_1:68;
then
A25: a2 < 2*PI by XCMPLX_1:74;
cos((2*PI*(j-'1))/n) = cos((2*PI*(k-'1))/n) by A15,A18,A23,COMPLEX1:77;
then a1 = a2 by A15,A18,A23,A20,A25,COMPLEX2:11,COMPTRIG:5;
then (2*PI*(j-'1))/n*n = 2*PI*(k-'1) by XCMPLX_1:87;
then j-'1 = k-'1 by COMPTRIG:5,XCMPLX_1:5,87;
then j = k-'1+1 by A19,XREAL_1:235;
hence thesis by A17,A22,A24,XREAL_1:235;
end;
then F is one-to-one by FUNCT_1:def 4;
then Seg n, F.:(Seg n) are_equipotent by A12,CARD_1:33;
then Seg n, rng F are_equipotent by A12,RELAT_1:113;
then card (Seg n) = card X by A11,CARD_1:5;
hence thesis by A1,FINSEQ_1:57;
end;
registration
let n be non zero Element of NAT;
cluster n-roots_of_1 -> non empty;
correctness by Th22;
cluster n-roots_of_1 -> finite;
correctness
proof
card (n-roots_of_1) = n by Th27;
hence thesis;
end;
end;
theorem Th28:
for n, ni being non zero Element of NAT st ni divides n holds
ni-roots_of_1 c= n-roots_of_1
proof
let n,ni be non zero Element of NAT;
assume ni divides n;
then consider k being Nat such that
A1: n = ni*k by NAT_D:def 3;
reconsider k as Element of NAT by ORDINAL1:def 12;
for x being object st x in ni-roots_of_1 holds x in n-roots_of_1
proof
let x be object such that
A2: x in ni-roots_of_1;
reconsider y=x as Element of F_Complex by A2;
y is CRoot of ni,1_F_Complex by A2,Th21;
then 1_F_Complex = (power F_Complex).(y, ni) by COMPLFLD:def 2;
then 1_F_Complex=(power F_Complex).((power F_Complex).(y,ni),k) by Th8;
then 1_F_Complex = (power F_Complex).(y,n) by A1,Th12;
then y is CRoot of n,1_F_Complex by COMPLFLD:def 2;
hence thesis;
end;
hence thesis;
end;
theorem Th29:
for R being Skew-Field, x being Element of MultGroup R, y being
Element of R st y = x for k being Nat holds (power (MultGroup R)).(x
,k) = (power R).(y,k)
proof
let R be Skew-Field, x be Element of MultGroup R, y be Element of R such
that
A1: y = x;
defpred P[Nat] means (power (MultGroup R)).(x,$1) = (power R).(y,$1);
A2: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A3: P[k];
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
thus (power (MultGroup R)).(x,k+1) = (power (MultGroup R)).(x,kk) * x
by GROUP_1:def 7
.= (power R).(y,kk) * y by A1,A3,Th16
.= (power R).(y,k+1) by GROUP_1:def 7;
end;
(power (MultGroup R)).(x,0) = 1_MultGroup R & (power R).(y,0) = 1_R by
GROUP_1:def 7;
then
A4: P[0] by Th17;
thus for k be Nat holds P[k] from NAT_1:sch 2(A4,A2);
end;
theorem Th30:
for n being non zero Element of NAT, x being Element of
MultGroup F_Complex st x in n-roots_of_1 holds x is not being_of_order_0
proof
set MGFC = MultGroup F_Complex;
set cMGFC = the carrier of MultGroup F_Complex;
set FC = F_Complex;
let n be non zero Element of NAT, x be Element of cMGFC;
assume x in n-roots_of_1;
then consider c being Element of FC such that
A1: c = x and
A2: c is CRoot of n,1_FC;
A3: 1_MGFC = 1_FC by Th17;
(power FC).(c,n) = 1_FC by A2,COMPLFLD:def 2;
then x |^ n = 1_MGFC by A1,A3,Th29;
hence thesis;
end;
theorem Th31:
for n being non zero Element of NAT, k being Element of NAT, x
being Element of MultGroup F_Complex st x = [** cos((2*PI*k)/n), sin((2*PI*k)/n
) **] holds ord x = n div (k gcd n)
proof
let n be non zero Element of NAT, k be Element of NAT;
reconsider kgn=(k gcd n) as Element of NAT;
A1: (k gcd n) divides n by INT_2:21;
then consider vn being Nat such that
A2: n = kgn * vn by NAT_D:def 3;
k gcd n divides k by INT_2:21;
then consider i being Nat such that
A3: k = kgn * i by NAT_D:def 3;
let x be Element of MultGroup F_Complex such that
A4: x = [** cos((2*PI*k)/n), sin((2*PI*k)/n) **];
x in n-roots_of_1 by A4,Th24;
then
A5: x is not being_of_order_0 by Th30;
A6: n gcd k > 0 by NEWTON:58;
A7: now
assume n div kgn = 0;
then n = kgn * (0 qua Nat) + (n mod kgn) by NAT_D:2,NEWTON:58;
hence contradiction by A1,A6,NAT_D:1,7;
end;
reconsider y=x as Element of F_Complex by Th19;
reconsider vn as Element of NAT by ORDINAL1:def 12;
A9: n = kgn * vn + 0 by A2;
then
A10: n div kgn = vn by A6,NAT_D:def 1;
A11: for m being Nat st x |^ m = 1_MultGroup F_Complex & m <> 0 holds n div
kgn <= m
proof
let m be Nat such that
A12: x |^ m = 1_MultGroup F_Complex and
A13: m <> 0;
reconsider m as Element of NAT by ORDINAL1:def 12;
now
assume
A14: m < vn;
A15: now
assume k*m mod n = 0;
then n divides k*m by PEPIN:6;
then consider j being Nat such that
A16: k*m = n*j by NAT_D:def 3;
consider a,b being Integer such that
A17: k = kgn*a and
A18: n = kgn*b and
A19: a,b are_coprime by INT_2:23;
0 <= a by A6,A17;
then reconsider ai=a as Element of NAT by INT_1:3;
0 <= b by A18;
then reconsider bi=b as Element of NAT by INT_1:3;
m*a*kgn = j*(b*kgn) by A17,A18,A16;
then m*a = ((j*b)*kgn)/kgn by A6,XCMPLX_1:89;
then m*a = j*b by A6,XCMPLX_1:89;
then
A20: bi divides m*ai by NAT_D:def 3;
m < bi by A6,A10,A14,A18,NAT_D:18;
hence contradiction by A13,A19,A20,INT_2:25,NAT_D:7;
end;
A21: 2*PI*k/n*m = (2*PI*k)/(n / m) by XCMPLX_1:82
.= (2*PI*k*m)/n by XCMPLX_1:77;
2*PI*(k*m mod n) < 2*PI*n by COMPTRIG:5,NAT_D:1,XREAL_1:68;
then 2*PI*(k*m mod n)/n < 2*PI*n/n by XREAL_1:74;
then
A22: 2*PI*(k*m mod n)/n < 2*PI by XCMPLX_1:89;
A23: 1_MultGroup F_Complex = [**1, 0**] by Th17,COMPLFLD:8;
x |^ m = (power F_Complex).(y, m) by Th29
.= y |^ m by COMPLFLD:74
.= [**cos((2*PI*(k*m))/n), sin((2*PI*k*m)/n) **] by A4,A21,COMPTRIG:53
.= [**cos((2*PI*(k*m mod n))/n), sin((2*PI*(k*m mod n))/n)**] by Th10;
then cos((2*PI*(k*m mod n))/n) = 1 by A12,A23,COMPLEX1:77;
hence contradiction by A15,A22,COMPTRIG:5,61;
end;
hence thesis by A6,A9,NAT_D:def 1;
end;
reconsider i as Element of NAT by ORDINAL1:def 12;
A24: 2*PI*k/n*vn = (2*PI*(kgn * i))/(n / vn) by A3,XCMPLX_1:82
.= (2*PI*(kgn * i)*vn)/n by XCMPLX_1:77
.= (2*PI*i)*n/n by A2
.= 2*PI*i + 0 by XCMPLX_1:89;
x |^ (n div kgn) = (power F_Complex).(y, vn) by A10,Th29
.= y |^ vn by COMPLFLD:74
.= [**cos((2*PI*k)/n*vn), sin((2*PI*k)/n*vn) **] by A4,COMPTRIG:53
.= [**cos(0), sin(2*PI*i + 0)**] by A24,COMPLEX2:9
.= 1+0*<i> by COMPLEX2:8,SIN_COS:31
.= 1_MultGroup F_Complex by Th17,COMPLFLD:8;
hence thesis by A7,A5,A11,GROUP_1:def 11;
end;
theorem Th32:
for n being non zero Element of NAT holds n-roots_of_1 c= the
carrier of MultGroup F_Complex
proof
let n be non zero Element of NAT;
set cMGFC = the carrier of MultGroup F_Complex;
set FC = F_Complex;
let a be object;
assume a in n-roots_of_1;
then consider x being Element of F_Complex such that
A1: a = x and
A2: x is CRoot of n,1_F_Complex;
(power FC).(x,n) = 1_FC by A2,COMPLFLD:def 2;
then x <> 0.FC by VECTSP_1:36;
then
A3: not x in {0.FC} by TARSKI:def 1;
cMGFC = NonZero FC by Def1;
hence thesis by A1,A3,XBOOLE_0:def 5;
end;
theorem
for n being non zero Element of NAT holds ex x being Element of
MultGroup F_Complex st ord x = n
proof
let n be non zero Element of NAT;
set x = [** cos((2*PI*1)/n), sin((2*PI*1)/n) **];
n-roots_of_1 c= the carrier of MultGroup F_Complex & x in n-roots_of_1
by Th24,Th32;
then reconsider y=x as Element of MultGroup F_Complex;
ord y = n div (1 gcd n) & 1 gcd n = 1 by Th31,WSIERP_1:8;
hence thesis;
end;
theorem Th34:
for n being non zero Element of NAT, x being Element of
MultGroup F_Complex holds ord x divides n iff x in n-roots_of_1
proof
set FC = F_Complex;
let n be non zero Element of NAT, x be Element of MultGroup F_Complex;
reconsider c = x as Element of FC by Th19;
set MGFC = MultGroup F_Complex;
A1: 1_MGFC = 1_FC by Th17;
hereby
assume ord x divides n;
then consider k being Nat such that
A2: n = (ord x)*k by NAT_D:def 3;
x |^ ord x = 1_MGFC by GROUP_1:41;
then (x |^ (ord x)) |^ k = 1_MGFC by GROUP_1:31;
then x |^ n = 1_MGFC by A2,GROUP_1:35;
then (power FC).(c, n) = 1_FC by A1,Th29;
then c is CRoot of n,1_FC by COMPLFLD:def 2;
hence x in n-roots_of_1;
end;
assume x in n-roots_of_1;
then consider c being Element of FC such that
A3: c = x and
A4: c is CRoot of n,1_FC;
(power FC).(c,n) = 1_FC by A4,COMPLFLD:def 2;
then x |^ n = 1_MGFC by A1,A3,Th29;
hence thesis by GROUP_1:44;
end;
theorem Th35:
for n being non zero Element of NAT holds n-roots_of_1 = { x
where x is Element of MultGroup F_Complex : ord x divides n}
proof
set cMGFC = the carrier of MultGroup F_Complex;
set MGFC = MultGroup F_Complex;
let n be non zero Element of NAT;
set R = { a where a is Element of F_Complex : a is CRoot of n,1_F_Complex };
set S = {x where x is Element of MultGroup F_Complex : ord x divides n};
A1: n-roots_of_1 = R;
then
A2: R c= cMGFC by Th32;
now
let a be object;
hereby
assume
A3: a in R;
then reconsider x = a as Element of MGFC by A2;
ord x divides n by A1,A3,Th34;
hence a in S;
end;
assume a in S;
then ex x being Element of MGFC st a = x & ord x divides n;
hence a in R by A1,Th34;
end;
hence thesis by TARSKI:2;
end;
theorem Th36:
for n being non zero Element of NAT, x being set holds x in n
-roots_of_1 iff ex y being Element of MultGroup F_Complex st x = y & ord y
divides n
proof
set MGFC = MultGroup F_Complex;
set cMGFC = the carrier of MultGroup F_Complex;
let n be non zero Element of NAT, x be set;
A1: n-roots_of_1 c= cMGFC by Th32;
hereby
assume
A2: x in n-roots_of_1;
then reconsider a = x as Element of MGFC by A1;
ord a divides n by A2,Th34;
hence ex y being Element of MultGroup F_Complex st x = y & ord y divides n;
end;
thus thesis by Th34;
end;
definition
let n be non zero Element of NAT;
func n-th_roots_of_1 -> strict Group means
:Def3:
the carrier of it = n
-roots_of_1 & the multF of it = (the multF of F_Complex)||(n-roots_of_1);
existence
proof
set X = [: n-roots_of_1, n-roots_of_1:];
set mru = (the multF of F_Complex)||(n-roots_of_1);
n-roots_of_1 c= the carrier of F_Complex;
then n-roots_of_1 c= COMPLEX by COMPLFLD:def 1;
then X c= [:COMPLEX, COMPLEX:] by ZFMISC_1:96;
then
A1: X c= dom multcomplex by FUNCT_2:def 1;
A2: multcomplex = the multF of F_Complex by COMPLFLD:def 1;
then
A3: dom mru = dom multcomplex /\ X by RELAT_1:61;
then
A4: dom mru = X by A1,XBOOLE_1:28;
for x being object st x in X holds mru.x in n-roots_of_1
proof
let x be object such that
A5: x in X;
consider a,b being object such that
A6: [a,b] = x by A5,RELAT_1:def 1;
A7: b in n-roots_of_1 by A5,A6,ZFMISC_1:87;
A8: a in n-roots_of_1 by A5,A6,ZFMISC_1:87;
reconsider b as Element of COMPLEX by A7,COMPLFLD:def 1;
reconsider a as Element of COMPLEX by A8,COMPLFLD:def 1;
multcomplex.(a,b) = a*b & mru.[a,b] = multcomplex.[a,b] by A2,A4,A5,A6,
BINOP_2:def 5,FUNCT_1:47;
hence thesis by A6,A8,A7,Th25;
end;
then reconsider uM = mru as BinOp of n-roots_of_1 by A1,A3,FUNCT_2:3
,XBOOLE_1:28;
set H = multMagma(# n-roots_of_1, uM #);
reconsider 1F = 1_F_Complex as Element of H by Th22;
A9: 1_F_Complex = [** cos((2*PI*(0 qua Nat))/n), sin((2*PI*(0 qua Nat))/n) **]
by COMPLFLD:8,SIN_COS:31;
A10: for s1 being Element of H holds s1*1F = s1 & 1F*s1 = s1 & ex s2 being
Element of H st s1 * s2 = 1_F_Complex & s2 * s1 = 1_F_Complex
proof
let s1 be Element of H;
A11: ex s2 being Element of H st s1 * s2 = 1_F_Complex & s2 * s1 = 1_F_Complex
proof
s1 in the carrier of F_Complex by TARSKI:def 3;
then consider k being Element of NAT such that
A12: s1 = [** cos((2*PI*k)/n), sin((2*PI*k)/n) **] by Th24;
reconsider e1=[**cos((2*PI*k)/n),sin((2*PI*k)/n)**] as Element of
F_Complex;
ex j being Element of NAT st (k+j) mod n = 0
proof
set r = (k mod n);
r < n by NAT_D:1;
then consider j being Nat such that
A13: r+j = n by NAT_1:10;
k = n*(k div n) + r by NAT_D:2;
then j in NAT & (k+j) mod n = (((k div n)+1)*n) mod n by A13,
ORDINAL1:def 12;
hence thesis by NAT_D:13;
end;
then consider j being Element of NAT such that
A14: (k+j) mod n = 0;
set ss2 = [**cos((2*PI*j)/n),sin((2*PI*j)/n)**];
reconsider s2=ss2 as Element of H by Th24;
reconsider e2=s2 as Element of F_Complex;
e2*e1 = [** cos((2*PI*((j+k) mod n))/n), sin((2*PI*((j+k) mod n))
/n) **] & [ s2,s1] in dom mru by A4,Th11,ZFMISC_1:87;
then
A15: s2*s1 = 1_F_Complex by A12,A14,COMPLFLD:8,FUNCT_1:47,SIN_COS:31;
e1*e2 = [** cos((2*PI*((j+k) mod n))/n), sin((2*PI*((j+k) mod n))
/n) **] & [ s1,s2] in dom mru by A4,Th11,ZFMISC_1:87;
then s1*s2 = 1_F_Complex by A12,A14,COMPLFLD:8,FUNCT_1:47,SIN_COS:31;
hence thesis by A15;
end;
s1*1F = s1 & 1F*s1 = s1
proof
A16: [s1,1F] in dom mru & [1F,s1] in dom mru by A4,ZFMISC_1:87;
reconsider e1=s1 as Element of F_Complex by TARSKI:def 3;
consider k being Element of NAT such that
A17: e1 = [** cos((2*PI*k)/n), sin((2*PI*k)/n) **] by Th24;
A18: 1_F_Complex*e1 = [** cos((2*PI*((k+0) mod n))/n), sin((2*PI*((k+0
) mod n))/n) **] by A9,A17,Th11
.= s1 by A17,Th10;
e1*1_F_Complex = [** cos((2*PI*((k+0) mod n))/n), sin((2*PI*((k+0
) mod n))/n) **] by A9,A17,Th11
.= s1 by A17,Th10;
hence thesis by A18,A16,FUNCT_1:47;
end;
hence thesis by A11;
end;
A19: rng uM c= n-roots_of_1 by RELAT_1:def 19;
for r,s,t being Element of H holds (r * s) * t = r * (s * t)
proof
set mc = multcomplex;
let r,s,t be Element of H;
r in the carrier of F_Complex by TARSKI:def 3;
then
A20: r is Element of COMPLEX by COMPLFLD:def 1;
s in the carrier of F_Complex by TARSKI:def 3;
then
A21: s is Element of COMPLEX by COMPLFLD:def 1;
A22: [r,s] in dom mru by A4,ZFMISC_1:87;
then mru.[r,s] in rng mru by FUNCT_1:3;
then
A23: [mru.[r,s],t] in dom mru by A4,A19,ZFMISC_1:87;
A24: [s,t] in dom mru by A4,ZFMISC_1:87;
then mru.[s,t] in rng mru by FUNCT_1:3;
then
A25: [r,mru.[s,t]] in dom mru by A4,A19,ZFMISC_1:87;
mru.[s,t] = mc.[s,t] by A2,A24,FUNCT_1:47;
then
A26: mru.[r,mru.[s,t]] = mc.(r,mc.(s,t)) by A2,A25,FUNCT_1:47;
t in the carrier of F_Complex by TARSKI:def 3;
then
A27: t is Element of COMPLEX by COMPLFLD:def 1;
mru.[r,s] = mc.[r,s] by A2,A22,FUNCT_1:47;
then mru.[mru.[r,s],t] = mc.(mc.(r,s),t) by A2,A23,FUNCT_1:47;
hence thesis by A20,A21,A27,A26,BINOP_1:def 3;
end;
then H is Group by A10,GROUP_1:1;
hence thesis;
end;
uniqueness;
end;
theorem
for n being non zero Element of NAT holds n-th_roots_of_1 is Subgroup
of MultGroup F_Complex
proof
set MGFC = MultGroup F_Complex;
set cMGFC = the carrier of MultGroup F_Complex;
set FC = F_Complex;
let n be non zero Element of NAT;
set nth = n-th_roots_of_1;
set cnth = the carrier of nth;
A1: the carrier of nth = n-roots_of_1 by Def3;
then
A2: the carrier of nth c= the carrier of MGFC by Th32;
the multF of nth = (the multF of FC)||(n-roots_of_1) & the multF of MGFC
= ( the multF of FC)||cMGFC by Def1,Def3;
then the multF of nth = (the multF of MGFC)||cnth by A1,A2,RELAT_1:74
,ZFMISC_1:96;
hence thesis by A2,GROUP_2:def 5;
end;
begin :: The unital polynomial x^n -1
definition
let n be non zero Nat, L be left_unital non empty doubleLoopStr;
func unital_poly(L,n) -> Polynomial of L equals
0_.(L)+*(0,-(1_L))+*(n,1_L);
coherence
proof
set p = 0_.(L)+*(0,-(1_L))+*(n,1_L);
A1: for i being Nat st i <> 0 & i <> n holds p.i = 0.L
proof
set q = 0_.(L)+*(0,-(1_L));
let i be Nat such that
A2: i <> 0 and
A3: i <> n;
A4: i in NAT by ORDINAL1:def 12;
q+*(n,1_L).i = q.i by A3,FUNCT_7:32
.= (0_.(L)).i by A2,FUNCT_7:32
.= 0.L by A4,FUNCOP_1:7;
hence thesis;
end;
for i being Nat st i >= n+1 holds p.i = 0.L
proof
let i be Nat such that
A5: i >= n+1;
now
A6: n + 0 < n + 1 by XREAL_1:8;
assume i = n;
hence contradiction by A5,A6;
end;
hence thesis by A1,A5;
end;
hence thesis by ALGSEQ_1:def 1;
end;
end;
Lm4: unital_poly (F_Complex,1) = <%-1_F_Complex, 1_F_Complex %>;
theorem Th38:
for L being left_unital non empty doubleLoopStr for n being
non zero Element of NAT holds unital_poly(L,n).0 = -1_L & unital_poly(L,n).n =
1_L
proof
let L be left_unital non empty doubleLoopStr, n be non zero Element of
NAT;
set p = 0_.(L)+*(0,-(1_L));
set q = 0_.(L)+*(n,1_L);
0 in NAT;
then
A1: unital_poly(L,n) = q+*(0,-(1_L)) & 0 in dom q by FUNCT_7:33,NORMSP_1:12;
n in NAT;
then n in dom p by NORMSP_1:12;
hence thesis by A1,FUNCT_7:31;
end;
theorem Th39:
for L being left_unital non empty doubleLoopStr for n being
non zero Nat, i being Nat st i <> 0 & i <> n holds unital_poly(L,n).i = 0.L
proof
let L be left_unital non empty doubleLoopStr, n be non zero Nat;
let i be Nat such that
A1: i <> 0 and
A2: i <> n;
set p = 0_.(L)+*(0,-(1_L));
A3: i in NAT by ORDINAL1:def 12;
p+*(n,1_L).i = p.i by A2,FUNCT_7:32
.= (0_.(L)).i by A1,FUNCT_7:32
.= 0.L by A3,FUNCOP_1:7;
hence thesis;
end;
theorem Th40:
for L being non degenerated well-unital non empty doubleLoopStr
, n being non zero Element of NAT holds len unital_poly(L,n) = n+1
proof
let L be non degenerated well-unital non empty doubleLoopStr;
let n be non zero Element of NAT;
A1: for m being Nat st m is_at_least_length_of unital_poly(L,n) holds n+1 <= m
proof
let m be Nat such that
A2: m is_at_least_length_of unital_poly(L,n);
now
assume m < n+1;
then m <= n by NAT_1:13;
then unital_poly(L,n).(n) = 0.L by A2,ALGSEQ_1:def 2;
hence contradiction by Th38;
end;
hence thesis;
end;
A3: n+1 in NAT by ORDINAL1:def 12;
for i being Nat st i >= n+1 holds unital_poly(L,n).i=0.L
proof
let i be Nat such that
A4: i >= n+1;
now
A5: n + 0 < n + 1 by XREAL_1:8;
assume i = n;
hence contradiction by A4,A5;
end;
hence thesis by A4,Th39;
end;
then n+1 is_at_least_length_of unital_poly(L,n) by ALGSEQ_1:def 2;
hence thesis by A1,ALGSEQ_1:def 3,A3;
end;
registration
let L be non degenerated well-unital non empty doubleLoopStr, n be non
zero Element of NAT;
cluster unital_poly(L,n) -> non-zero;
correctness
proof
len unital_poly(L,n) = n+1 by Th40;
hence thesis by UPROOTS:17;
end;
end;
theorem Th41:
for n being non zero Element of NAT for x being Element of
F_Complex holds eval(unital_poly(F_Complex,n), x) = (power F_Complex).(x,n) - 1
proof
1 - 1 = 0;
then
A1: 1 -'1 = 0 by XREAL_1:233;
reconsider z2=1_F_Complex as Element of COMPLEX by COMPLFLD:def 1;
let n be non zero Element of NAT, x be Element of F_Complex;
set p = unital_poly(F_Complex,n);
consider F being FinSequence of F_Complex such that
A2: eval(p,x) = Sum F and
A3: len F = len p and
A4: for i being Element of NAT st i in dom F holds F.i = p.(i-'1) * (
power F_Complex).(x,i-'1) by POLYNOM4:def 2;
A5: 0+1 < n+1 by XREAL_1:8;
then
A6: 1 < len F by A3,Th40;
A7: len F=n+1 by A3,Th40;
then len F -1=n;
then
A8: len F -'1 = n by A5,XREAL_1:233;
len F - 1 + 1 = len F;
then
A9: len F-'1+1 = len F by A6,XREAL_1:233;
A10: p.0 = -1_F_Complex by Th38;
set xn = (power F_Complex).(x,n);
set null = (len F-'1) |-> (0.F_Complex);
A11: len null = len F -'1 by CARD_1:def 7;
set tR2 = null^<*xn*>;
set tR1 = <*-1_F_Complex*>^null;
A12: dom F = Seg len F by FINSEQ_1:def 3;
reconsider R1=tR1 as Tuple of len F, the carrier of F_Complex
by A9;
reconsider R1 as Element of (len F)-tuples_on the carrier of F_Complex
by FINSEQ_2:131;
reconsider R2=tR2 as Tuple of len F, the carrier of F_Complex
by A9;
reconsider R2 as Element of (len F)-tuples_on the carrier of F_Complex
by FINSEQ_2:131;
A13: for i being Element of NAT st i in dom null holds null.i = 0.F_Complex
proof
let i be Element of NAT;
assume i in dom null;
then i in Seg (len F-'1) by FUNCOP_1:13;
hence thesis by FUNCOP_1:7;
end;
A14: for i being Nat st i <> 1 & i in dom R1 holds R1.i = 0.F_Complex
proof
let i be Nat such that
A15: i <> 1 and
A16: i in dom R1;
A17: dom <*-1_F_Complex*> = Seg 1 by FINSEQ_1:def 8;
now
assume i in dom <*-1_F_Complex*>;
then 1<=i & i<=1 by A17,FINSEQ_1:1;
hence contradiction by A15,XXREAL_0:1;
end;
then consider j being Nat such that
A18: j in dom null and
A19: i = len <*-1_F_Complex*> + j by A16,FINSEQ_1:25;
null.j = 0.F_Complex by A13,A18;
hence thesis by A18,A19,FINSEQ_1:def 7;
end;
len tR2 = len null + len <*xn*> by FINSEQ_1:22;
then
A20: len tR2 = len F by A11,A9,FINSEQ_1:39;
A21: for i being Element of NAT st i in dom R2 & i <> len F holds R2.i = 0.
F_Complex
proof
let i be Element of NAT such that
A22: i in dom R2 and
A23: i <> len F;
A24: dom R2 = Seg len F by A20,FINSEQ_1:def 3;
then i <= len F by A22,FINSEQ_1:1;
then i < len F-'1+1 by A9,A23,XXREAL_0:1;
then
A25: i <= len F-'1 by NAT_1:13;
1 <= i by A22,A24,FINSEQ_1:1;
then i in Seg (len F-'1) by A25,FINSEQ_1:1;
then
A26: i in dom null by A11,FINSEQ_1:def 3;
then R2.i = null.i by FINSEQ_1:def 7;
hence thesis by A13,A26;
end;
len R1 = len F by CARD_1:def 7;
then
A27: dom R1 = Seg len F by FINSEQ_1:def 3;
len R2 = len F by CARD_1:def 7;
then
A28: dom R2 = Seg len F by FINSEQ_1:def 3;
A29: R1.1 = -1_F_Complex by FINSEQ_1:41;
A30: len (R1+R2) = len F by CARD_1:def 7;
then
A31: dom (R1+R2) = Seg len F by FINSEQ_1:def 3;
A32: R2.(len F) = (power F_Complex).(x,n) by A11,A9,FINSEQ_1:42;
for k being Nat st k in dom (R1+R2) holds (R1+R2).k = F.k
proof
let k be Nat such that
A33: k in dom (R1+R2);
A34: k in Seg len F by A30,A33,FINSEQ_1:def 3;
A35: k in dom F by A31,A33,FINSEQ_1:def 3;
A36: 1 <= k by A31,A33,FINSEQ_1:1;
A37: (-1_F_Complex)*(1_F_Complex) = -1_F_Complex;
now
per cases;
suppose
A38: k = 1;
then R2.k = 0.F_Complex by A6,A21,A28,A34;
then
A39: (R1+R2).1 = (-1_F_Complex)+0.F_Complex by A29,A33,A38,FVSUM_1:17;
F.1 = p.0 * (power F_Complex).(x,0) by A4,A1,A35,A38
.= -1_F_Complex by A10,A37,GROUP_1:def 7;
hence thesis by A38,A39,COMPLFLD:7;
end;
suppose
A40: k <> 1;
now
per cases;
suppose
A41: k = len F;
len F <> 0 by A3,A5,Th40;
then
A42: F.(len F) = p.(len F-'1)*(power F_Complex).(x,len F-'1) by A4,A12,
FINSEQ_1:3
.= 1_F_Complex*(power F_Complex).(x,n) by A8,Th38
.= (power F_Complex).(x,n);
R1.(len F) = 0.F_Complex by A6,A14,A27,A34,A41;
then (R1+R2).(len F) = 0.F_Complex + (power F_Complex).(x, n) by
A32,A33,A41,FVSUM_1:17
.= (power F_Complex).(x,n) by COMPLFLD:7;
hence thesis by A41,A42;
end;
suppose
A43: k <> len F;
A44: now
assume k-'1 = n;
then k - 1 = n by A36,XREAL_1:233;
hence contradiction by A7,A43;
end;
1 < k by A36,A40,XXREAL_0:1;
then 1+-1 < k+-1 by XREAL_1:8;
then 1-1 < k-1;
then 0 < k-'1 by A36,XREAL_1:233;
then p.(k-'1) = 0.F_Complex by A44,Th39;
then
A45: F.k = 0.F_Complex * (power F_Complex).(x,k-'1) by A4,A35;
A46: R2.k = 0.F_Complex by A21,A28,A34,A43;
R1.k = 0.F_Complex by A14,A27,A34,A40;
then (R1+R2).k = 0.F_Complex + 0.F_Complex by A33,A46,FVSUM_1:17;
hence thesis by A45,COMPLFLD:7;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
then
A47: (R1+R2) = F by A12,A31,FINSEQ_1:13;
Sum null = 0.F_Complex by MATRIX_3:11;
then Sum R1 = -1_F_Complex + 0.F_Complex & Sum R2 = 0.F_Complex + xn by
FVSUM_1:71,72;
then -z2 = -1_F_Complex & Sum F = -1_F_Complex+(power F_Complex).(x,n) by A47
,COMPLFLD:7,FVSUM_1:76;
hence thesis by A2,COMPLFLD:8;
end;
theorem Th42:
for n being non zero Element of NAT holds Roots unital_poly(
F_Complex, n) = n-roots_of_1
proof
let n be non zero Element of NAT;
now
set p = unital_poly(F_Complex,n);
let x be object;
hereby
assume
A1: x in Roots p;
then reconsider x9 = x as Element of F_Complex;
x9 is_a_root_of p by A1,POLYNOM5:def 10;
then 0.F_Complex = eval(p,x9) by POLYNOM5:def 7
.= (power F_Complex).(x9,n) - 1 by Th41;
then x9 is CRoot of n, 1_F_Complex by COMPLFLD:7,8,def 2;
hence x in n-roots_of_1;
end;
assume
A2: x in n-roots_of_1;
then reconsider x9 = x as Element of F_Complex;
x9 is CRoot of n, 1_F_Complex by A2,Th21;
then (power F_Complex).(x9,n) = 1 by COMPLFLD:8,def 2;
then (power F_Complex).(x9,n) - 1 = 0c;
then eval(p,x9) = 0.F_Complex by Th41,COMPLFLD:7;
then x9 is_a_root_of p by POLYNOM5:def 7;
hence x in Roots unital_poly(F_Complex,n) by POLYNOM5:def 10;
end;
hence thesis by TARSKI:2;
end;
theorem Th43:
for n being Element of NAT, z being Element of F_Complex st z is
Real ex x being Real st x = z & (power F_Complex).(z,n) = x |^ n
proof
let n be Element of NAT;
let z be Element of F_Complex;
assume z is Real;
then reconsider x=z as Real;
per cases;
suppose
A1: x = 0;
then
A2: z = 0.F_Complex by COMPLFLD:def 1;
thus thesis
proof
per cases;
suppose
A3: n = 0;
then (power F_Complex).(z,n) = 1 by COMPLFLD:8,GROUP_1:def 7
.= x |^ n by A3,NEWTON:4;
hence thesis;
end;
suppose
A4: n > 0;
then
A5: n >= 0+1 by NAT_1:13;
(power F_Complex).(z,n) = 0.F_Complex by A2,A4,VECTSP_1:36
.= x|^n by A1,A5,COMPLFLD:7,NEWTON:11;
hence thesis;
end;
end;
end;
suppose
A6: x <> 0;
defpred P[Nat] means (power F_Complex).(z,$1) = x |^ $1;
A7: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
A8: P[n];
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
(power F_Complex).(z,n+1) = (power F_Complex).(z,nn)*z by GROUP_1:def 7
.= (x #Z n) * x by A8,PREPOWER:36
.= (x#Z n) * (x #Z 1) by PREPOWER:35
.= (x #Z (n+1)) by A6,PREPOWER:44
.= (x |^ (n+1)) by PREPOWER:36;
hence thesis;
end;
(power F_Complex).(z,0) = 1r by COMPLFLD:8,GROUP_1:def 7
.= x #Z 0 by PREPOWER:34
.= x |^ 0 by PREPOWER:36;
then
A9: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A9,A7);
then (power F_Complex).(z,n) = x |^ n;
hence thesis;
end;
end;
theorem Th44:
for n being non zero Element of NAT for x being Real ex y being
Element of F_Complex st y = x & eval(unital_poly(F_Complex,n),y) = (x |^ n) - 1
proof
let n be non zero Element of NAT, x be Real;
x in COMPLEX by XCMPLX_0:def 2;
then reconsider y=x as Element of F_Complex by COMPLFLD:def 1;
ex x2 being Real st x2 = y & (power F_Complex).(y,n) = x2 |^ n by Th43;
then eval(unital_poly(F_Complex,n),y) = (x |^ n) - 1 by Th41;
hence thesis;
end;
theorem Th45:
for n being non zero Element of NAT holds BRoots unital_poly(
F_Complex, n) = (n-roots_of_1, 1)-bag
proof
let n being non zero Element of NAT;
set p = unital_poly(F_Complex, n);
A1: degree BRoots p = len p -' 1 by UPROOTS:59
.= n+1 -'1 by Th40
.= n by NAT_D:34;
A2: card (n-roots_of_1) = n by Th27;
Roots p = n-roots_of_1 & support BRoots p = Roots p by Th42,UPROOTS:def 9;
hence thesis by A1,A2,UPROOTS:13;
end;
theorem Th46:
for n being non zero Element of NAT holds unital_poly(F_Complex
, n) = poly_with_roots((n-roots_of_1, 1)-bag)
proof
let n be non zero Element of NAT;
set p = unital_poly(F_Complex, n);
len p = n+1 by Th40;
then p.(len p-'1) = p.n by NAT_D:34
.= 1_F_Complex by Th38;
hence unital_poly(F_Complex, n) = poly_with_roots BRoots unital_poly(
F_Complex, n) by UPROOTS:65
.= poly_with_roots((n-roots_of_1, 1)-bag) by Th45;
end;
theorem Th47:
for n being non zero Element of NAT, i being Element of
F_Complex st i is Integer holds eval(unital_poly(F_Complex, n), i) is Integer
proof
let n be non zero Element of NAT;
let i be Element of F_Complex such that
A1: i is Integer;
reconsider j = i as Integer by A1;
ex y being Element of F_Complex st y = i & eval( unital_poly(F_Complex,n)
,y) = (j |^ n) - 1 by Th44;
hence thesis;
end;
begin :: Cyclotomic Polynomials
definition
let d be non zero Nat;
func cyclotomic_poly d -> Polynomial of F_Complex means
:Def5:
ex s being
non empty finite Subset of F_Complex st s = { y where y is Element of MultGroup
F_Complex : ord y = d } & it = poly_with_roots((s,1)-bag);
existence
proof
set cMGFC = the carrier of MultGroup F_Complex;
reconsider d as non zero Element of NAT by ORDINAL1:def 12;
defpred P[Element of cMGFC] means ord $1 = d;
set s = { y where y is Element of cMGFC : P[y]};
set x = [** cos((2*PI*1)/d), sin((2*PI*1)/d) **];
reconsider i = d as Integer;
x <> 0.F_Complex
proof
assume
A1: x = 0.F_Complex;
then 0+0*<i> = cos((2*PI*1)/d)+(sin((2*PI*1)/d))*<i> by COMPLFLD:7;
then cos((2*PI*1)/d) = 0 by COMPLEX1:77;
hence contradiction by A1,COMPLEX2:10,COMPLFLD:7;
end;
then
A2: not x in {0.F_Complex} by TARSKI:def 1;
cMGFC = NonZero F_Complex by Def1;
then reconsider x as Element of cMGFC by A2,XBOOLE_0:def 5;
A3: d-roots_of_1 = {y where y is Element of cMGFC : ord y divides d} by Th35;
A4: s c= d-roots_of_1
proof
let a be object;
assume a in s;
then ex y being Element of cMGFC st a = y & ord y = d;
hence thesis by A3;
end;
1 gcd i = 1 by WSIERP_1:8;
then ord x = d div 1 by Th31
.= d;
then x in s;
then reconsider s as non empty finite Subset of F_Complex by A4,XBOOLE_1:1;
take poly_with_roots((s,1)-bag);
thus thesis;
end;
uniqueness;
end;
theorem Th48:
cyclotomic_poly(1) = <%-1_F_Complex, 1_F_Complex %>
proof
set cMGFC = the carrier of MultGroup F_Complex;
consider s being non empty finite Subset of F_Complex such that
A1: s = { y where y is Element of cMGFC : ord y = 1 } and
A2: cyclotomic_poly(1) = poly_with_roots((s,1)-bag) by Def5;
A3: 1-roots_of_1 = {x where x is Element of cMGFC : ord x divides 1} by Th35;
now
let x be object;
hereby
assume x in s;
then ex x1 being Element of cMGFC st x = x1 & ord x1 = 1 by A1;
hence x in 1-roots_of_1 by A3;
end;
assume x in 1-roots_of_1;
then consider x1 being Element of cMGFC such that
A4: x = x1 and
A5: ord x1 divides 1 by A3;
ord x1 = 1 by A5,WSIERP_1:15;
hence x in s by A1,A4;
end;
then s = 1-roots_of_1 by TARSKI:2;
hence thesis by A2,Lm4,Th46;
end;
theorem Th49:
for n being non zero Element of NAT, f being FinSequence of (
the carrier of Polynom-Ring F_Complex) st len f = n & for i being non zero
Element of NAT st i in dom f holds (not i divides n implies f.i = <%1_F_Complex
%>) & (i divides n implies f.i = cyclotomic_poly(i)) holds unital_poly(
F_Complex,n) = Product(f)
proof
set cMGFC = the carrier of MultGroup F_Complex;
let n be non zero Element of NAT, f be FinSequence of (the carrier of
Polynom-Ring F_Complex) such that
A1: len f = n and
A2: for i being non zero Element of NAT st i in dom f holds (not i
divides n implies f.i = <%1_F_Complex%>) & (i divides n implies f.i =
cyclotomic_poly(i));
defpred P[Nat,set] means for fi being FinSequence of (the carrier of
Polynom-Ring F_Complex) st fi = f|Seg $1 holds $2 = Product(fi);
set nr1 = n-roots_of_1;
deffunc MG(Nat) = {y where y is Element of MultGroup F_Complex : y in nr1 &
ord y <= $1 };
A3: now
let i being Nat;
assume i in Seg len f;
reconsider fi = f|Seg i as FinSequence of (the carrier of Polynom-Ring
F_Complex) by FINSEQ_1:18;
set x = Product fi;
take x;
thus P[i,x];
end;
consider F being FinSequence of Polynom-Ring F_Complex such that
dom F = Seg len f and
A4: for i being Nat st i in Seg len f holds P[i,F.i] from FINSEQ_1:sch 5
(A3 );
defpred R[Nat] means ex t being finite Subset of F_Complex st t =
MG($1) & F.$1 = poly_with_roots((t,1)-bag);
A5: now
let i be Element of NAT;
MG(i) c= nr1
proof
let x be object;
assume x in MG(i);
then ex y being Element of cMGFC st x = y & y in nr1 & ord y <= i;
hence thesis;
end;
hence MG(i) is finite Subset of F_Complex by XBOOLE_1:1;
end;
then reconsider sB = MG(n) as finite Subset of F_Complex;
A6: nr1 = {x where x is Element of MultGroup F_Complex : ord x divides n} by
Th35;
A7: for i being Element of NAT st 1 <= i & i < len f holds R[i] implies R[i +1]
proof
let i be Element of NAT such that
A8: 1 <= i and
A9: i < len f and
A10: R[i];
reconsider fi = f|Seg i as FinSequence of (the carrier of Polynom-Ring
F_Complex) by FINSEQ_1:18;
i in Seg len f by A8,A9,FINSEQ_1:1;
then
A11: F.i = Product fi by A4;
reconsider fi1 = f|Seg (i+1) as FinSequence of (the carrier of
Polynom-Ring F_Complex) by FINSEQ_1:18;
A12: i+1 <= len f by A9,NAT_1:13;
then i+1 = min(i+1,len f) by XXREAL_0:def 9;
then
A13: len fi1 = i+1 by FINSEQ_2:21;
1 <= i+1 by A8,NAT_1:13;
then
A14: i+1 in Seg len f by A12,FINSEQ_1:1;
then
A15: i+1 in dom f by FINSEQ_1:def 3;
i+1 in NAT by ORDINAL1:def 12;
then reconsider sB = MG(i+1) as finite Subset of F_Complex by A5;
take sB;
thus sB = MG(i+1);
set B = (sB,1)-bag;
consider sb being finite Subset of F_Complex such that
A16: sb = MG(i) and
A17: F.i = poly_with_roots((sb,1)-bag) by A10;
A18: (f|Seg (i+1)).(i+1) = f.(i+1) by FINSEQ_1:4,FUNCT_1:49;
then reconsider
fi1d1 = fi1.(i+1) as Element of (the carrier of Polynom-Ring
F_Complex) by A15,FINSEQ_2:11;
set b = (sb, 1)-bag;
reconsider fi1d1p = fi1d1 as Polynomial of F_Complex by POLYNOM3:def 10;
fi = fi1 | Seg i by Lm2,NAT_1:12;
then fi1 = fi ^ <* fi1d1 *> by A13,FINSEQ_3:55;
then
A19: Product fi1 = Product fi * fi1d1 by GROUP_4:6
.= (poly_with_roots b) *' fi1d1p by A17,A11,POLYNOM3:def 10;
per cases;
suppose
A20: not (i+1) divides n;
set eb = EmptyBag the carrier of F_Complex;
now
let x be object;
hereby
assume x in sB;
then consider y being Element of MultGroup F_Complex such that
A21: x = y and
A22: y in nr1 and
A23: ord y <= i+1;
ord y divides n by A22,Th34;
then ord y < i+1 by A20,A23,XXREAL_0:1;
then ord y <= i by NAT_1:13;
hence x in sb by A16,A21,A22;
end;
assume x in sb;
then consider y being Element of cMGFC such that
A24: x = y & y in nr1 and
A25: ord y <= i by A16;
ord y <= i+1 by A25,NAT_1:12;
hence x in sB by A24;
end;
then
A26: sB = sb by TARSKI:2;
f.(i+1) = <%1_F_Complex%> by A2,A15,A20
.= poly_with_roots(eb) by UPROOTS:60;
hence
F.(i+1) = (poly_with_roots b)*' poly_with_roots(eb) by A4,A14,A18,A19
.= poly_with_roots (b+eb) by UPROOTS:64
.= poly_with_roots(B) by A26,PRE_POLY:53;
end;
suppose
A27: i+1 divides n;
consider scb being non empty finite Subset of F_Complex such that
A28: scb = {y where y is Element of cMGFC : ord y = i+1 } and
A29: cyclotomic_poly(i+1) = poly_with_roots((scb,1)-bag) by Def5;
now
let x be object;
hereby
assume x in sB;
then consider y being Element of cMGFC such that
A30: x = y and
A31: y in nr1 and
A32: ord y <= i+1;
ord y <= i or ord y = i+1 by A32,NAT_1:8;
then y in sb or y in scb by A16,A28,A31;
hence x in sb \/ scb by A30,XBOOLE_0:def 3;
end;
assume
A33: x in sb \/ scb;
per cases by A33,XBOOLE_0:def 3;
suppose
x in sb;
then consider y being Element of cMGFC such that
A34: x = y & y in nr1 and
A35: ord y <= i by A16;
ord y <= i+1 by A35,NAT_1:12;
hence x in sB by A34;
end;
suppose
x in scb;
then consider y being Element of cMGFC such that
A36: x = y and
A37: ord y = i+1 by A28;
y in nr1 by A6,A27,A37;
hence x in sB by A36,A37;
end;
end;
then
A38: sB = sb \/ scb by TARSKI:2;
set cb = (scb,1)-bag;
A39: sb misses scb
proof
assume sb /\ scb <> {};
then consider x being object such that
A40: x in sb /\ scb by XBOOLE_0:def 1;
x in scb by A40,XBOOLE_0:def 4;
then
A41: ex y2 being Element of cMGFC st x = y2 & ord y2 = i+1 by A28;
x in sb by A40,XBOOLE_0:def 4;
then ex y1 being Element of cMGFC st x = y1 & y1 in nr1 & ord y1 <= i
by A16;
hence contradiction by A41,NAT_1:13;
end;
f.(i+1) = poly_with_roots(cb) by A2,A15,A27,A29;
hence F.(i+1) = (poly_with_roots b)*' poly_with_roots(cb) by A4,A14,A18
,A19
.= poly_with_roots (b+cb) by UPROOTS:64
.= poly_with_roots(B) by A38,A39,UPROOTS:10;
end;
end;
A42: 0+1 <= n by NAT_1:13;
A43: R[1]
proof
reconsider t = MG(1) as finite Subset of F_Complex by A5;
take t;
thus t = MG(1);
reconsider f1 = f|Seg 1 as FinSequence of (the carrier of Polynom-Ring
F_Complex) by FINSEQ_1:18;
A44: 1 in dom f & 1 divides n by A1,A42,FINSEQ_3:25,NAT_D:6;
A45: 1 in Seg len f by A1,A42,FINSEQ_1:1;
then 1 in dom f by FINSEQ_1:def 3;
then reconsider
fd1 = f.1 as Element of (the carrier of Polynom-Ring F_Complex)
by FINSEQ_2:11;
f1 = <*f.1*> by A1,A42,Th1;
then F.1 = Product <*fd1*> by A4,A45
.= fd1 by FINSOP_1:11
.= cyclotomic_poly(1) by A2,A44;
then consider sB being non empty finite Subset of F_Complex such that
A46: sB = { y where y is Element of cMGFC : ord y = 1 } and
A47: F.1 = poly_with_roots((sB,1)-bag) by Def5;
now
let x be object;
hereby
assume x in MG(1);
then consider y being Element of cMGFC such that
A48: x = y and
A49: y in nr1 and
A50: ord y <= 1;
y is not being_of_order_0 by A49,Th30;
then ord y <> 0 by GROUP_1:def 11;
then 0+1 <= ord y by NAT_1:13;
then ord y = 1 by A50,XXREAL_0:1;
hence x in sB by A46,A48;
end;
assume x in sB;
then consider y being Element of cMGFC such that
A51: x = y and
A52: ord y = 1 by A46;
ord y divides n by A52,NAT_D:6;
then y in nr1 by A6;
hence x in MG(1) by A51,A52;
end;
hence thesis by A47,TARSKI:2;
end;
for i being Element of NAT st 1 <= i & i <= len f holds R[i] from
INT_1:sch 7 (A43,A7);
then
A53: ex t being finite Subset of F_Complex st t = MG(len f) & F.len f =
poly_with_roots((t,1)-bag) by A1,A42;
set b = (nr1, 1)-bag;
A54: f = f|Seg len f by FINSEQ_3:49;
now
let x be object;
hereby
assume
A55: x in nr1;
then consider y being Element of MultGroup F_Complex such that
A56: x = y and
A57: ord y divides n by A6;
ord y <= n by A57,NAT_D:7;
hence x in sB by A55,A56;
end;
assume x in sB;
then ex y being Element of MultGroup F_Complex st y = x & y in nr1 & ord
y <= n;
hence x in nr1;
end;
then
A58: nr1 = sB by TARSKI:2;
thus unital_poly(F_Complex,n) = poly_with_roots(b) by Th46
.= Product(f) by A1,A4,A58,A53,A54,FINSEQ_1:3;
end;
theorem Th50:
for n being non zero Element of NAT ex f being FinSequence of (
the carrier of Polynom-Ring F_Complex), 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 = n implies f.i = <%1_F_Complex%>) & (i divides n
& i <> n implies f.i = cyclotomic_poly(i))) & unital_poly(F_Complex,n) = (
cyclotomic_poly n)*'p
proof
set cPRFC = the carrier of Polynom-Ring F_Complex;
let n be non zero Element of NAT;
defpred P[set,set] means ex i being non zero Element of NAT st i = $1 & (
not i divides n implies $2 = <%1_F_Complex%>) & (i divides n implies $2 =
cyclotomic_poly(i));
consider m being Nat such that
A1: n = m+1 by NAT_1:6;
A2: for k being Nat st k in Seg n ex x being Element of cPRFC st
P[k,x]
proof
let k be Nat;
assume k in Seg n;
then reconsider i = k as non zero Element of NAT by FINSEQ_1:1;
per cases;
suppose
A3: not i divides n;
reconsider FC1 = <%1_F_Complex%> as Element of cPRFC by POLYNOM3:def 10;
take FC1;
take i;
thus i = k;
thus thesis by A3;
end;
suppose
A4: i divides n;
reconsider FC1 = cyclotomic_poly(i) as Element of cPRFC by
POLYNOM3:def 10;
take FC1;
take i;
thus i = k;
thus thesis by A4;
end;
end;
consider f being FinSequence of cPRFC such that
A5: dom f = Seg n and
A6: for k being Nat st k in Seg n holds P[k,f/.k] from
RECDEF_1:sch 17(A2);
reconsider fm = f|Seg m as FinSequence of cPRFC by FINSEQ_1:18;
A7: len f = n by A5,FINSEQ_1:def 3;
A8: now
let i be non zero Element of NAT;
assume
A9: i in dom f;
then
A10: i <= n by A5,FINSEQ_1:1;
(ex j being non zero Element of NAT st j = i &( not j divides n
implies f/.i = <%1_F_Complex%>)&( j divides n implies f/.i = cyclotomic_poly(j)
))& 1 <= i by A5,A6,A9,FINSEQ_1:1;
hence (not i divides n implies f.i = <%1_F_Complex%>) & (i divides n
implies f.i = cyclotomic_poly(i)) by A7,A10,FINSEQ_4:15;
end;
reconsider FC1 = <%1_F_Complex %> as Element of cPRFC by POLYNOM3:def 10;
<* FC1 *> is FinSequence of cPRFC;
then reconsider h = fm^<* <%1_F_Complex %> *> as FinSequence of cPRFC by
FINSEQ_1:75;
reconsider p = Product(h) as Polynomial of F_Complex by POLYNOM3:def 10;
take h, p;
thus p = Product(h);
A11: m <= n by A1,NAT_1:13;
then
A12: len fm = m by A7,FINSEQ_1:17;
reconsider cpn = cyclotomic_poly n as Element of cPRFC by POLYNOM3:def 10;
reconsider fn = f|Seg n as FinSequence of cPRFC by FINSEQ_1:18;
1 <= n by NAT_1:53;
then
A13: n in Seg n by FINSEQ_1:1;
then
A14: f.n = cyclotomic_poly n by A5,A8;
len <* <%1_F_Complex %> *> = 1 by FINSEQ_1:40;
hence dom h = Seg n by A1,A12,FINSEQ_1:def 7;
A15: dom fm = Seg m by A7,A11,FINSEQ_1:17;
thus for i being non zero Element of NAT st i in Seg n holds (not i divides
n or i = n implies h.i = <%1_F_Complex%>) & (i divides n & i <> n implies h.i =
cyclotomic_poly(i))
proof
let i be non zero Element of NAT;
assume
A16: i in Seg n;
per cases;
suppose
A17: i in Seg m;
then
A18: fm.i = f.i & i <= m by FINSEQ_1:1,FUNCT_1:49;
h.i = fm.i by A15,A17,FINSEQ_1:def 7;
hence thesis by A5,A1,A8,A16,A18,NAT_1:13;
end;
suppose
not i in Seg m;
then not (1 <= i & i <= m) by FINSEQ_1:1;
then
A19: n <= i by A1,A16,FINSEQ_1:1,NAT_1:13;
A20: i <= n by A16,FINSEQ_1:1;
1 in Seg 1 by FINSEQ_1:1;
then 1 in dom <* <%1_F_Complex %> *> by FINSEQ_1:38;
then h.n = <* <%1_F_Complex %> *>.1 by A1,A12,FINSEQ_1:def 7
.= <%1_F_Complex%>;
hence
not i divides n or i = n implies h.i = <%1_F_Complex%> by A19,A20,
XXREAL_0:1;
thus thesis by A19,A20,XXREAL_0:1;
end;
end;
reconsider p1 = <%1_F_Complex %> as Element of cPRFC by POLYNOM3:def 10;
reconsider Pfm = Product fm as Polynomial of F_Complex by POLYNOM3:def 10;
A21: Product(h) = Product(fm) * p1 by GROUP_4:6
.= Pfm *' <%1_F_Complex %> by POLYNOM3:def 10
.= Product(fm) by UPROOTS:32;
f = fn by A7,FINSEQ_2:20
.= fm^<*cyclotomic_poly n*> by A5,A1,A13,A14,FINSEQ_5:10;
then
A22: Product(f) = Product(fm) * cpn by GROUP_4:6;
unital_poly(F_Complex,n) = Product(f) by A7,A8,Th49;
hence thesis by A21,A22,POLYNOM3:def 10;
end;
theorem Th51:
for d being non zero Element of NAT, i being Element of NAT
holds ((cyclotomic_poly d).0 = 1 or (cyclotomic_poly d).0 = -1) & (
cyclotomic_poly d).i is integer
proof
deffunc cp(non zero Nat) = cyclotomic_poly($1);
set cPRFC = the carrier of Polynom-Ring F_Complex;
set cFC = the carrier of F_Complex;
defpred P[non zero Element of NAT] means (cp($1).0 = 1 or cp($1).0 = -1) &
for i being Element of NAT holds cp($1).i is integer;
A1: -1_F_Complex = -1 by COMPLFLD:8;
A2: now
let k be non zero Element of NAT such that
A3: for n being non zero Element of NAT st n < k holds P[n];
A4: 1 <= k by Lm1;
per cases by A4,XXREAL_0:1;
suppose
A5: k = 1;
now
let i be Element of NAT;
per cases by NAT_1:23;
suppose
i = 0;
hence cp(k).i is integer by A1,A5,Th48,POLYNOM5:38;
end;
suppose
i = 1;
hence cp(k).i is integer by A5,Th48,COMPLFLD:8,POLYNOM5:38;
end;
suppose
i >= 2;
hence cp(k).i is integer by A5,Th48,COMPLFLD:7,POLYNOM5:38;
end;
end;
hence P[k] by A1,A5,Th48,POLYNOM5:38;
end;
suppose
A6: k > 1;
consider f being FinSequence of cPRFC, 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 = cp(i)) and
A10: unital_poly(F_Complex,k) = (cyclotomic_poly k)*'p by Th50;
defpred G[Nat,object] means ex g being FinSequence of cPRFC, 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 H[Nat] means $1 in Seg len f implies ex x being object
st G[$1,x];
A11: k = len f by A8,FINSEQ_1:def 3;
A12: for l being Nat st H[l] holds H[l+1]
proof
let l be Nat;
assume
A13: H[l];
assume
A14: l+1 in Seg len f;
per cases;
suppose
A15: l = 0;
reconsider fl1 = f.(l+1) as Element of cPRFC by A8,A11,A14,
FINSEQ_2:11;
reconsider g = f | Seg (l+1) as FinSequence of cPRFC by FINSEQ_1:18;
reconsider p = Product(g) as Polynomial of F_Complex by
POLYNOM3:def 10;
<*>cPRFC = f |(Seg 0 qua set);
then g = (<*>cPRFC)^<*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;
take g;
take p;
thus g = f | Seg (l+1) & p = Product(g) & p = p;
1 divides k by NAT_D:6;
then
A17: f.1 = cp(1) by A6,A9,A11,A14,A15;
hence p.0 = 1 or p.0 = -1 by A1,A15,A16,Th48,POLYNOM5:38;
let j be Element of NAT;
thus p.j is integer
proof
per cases by NAT_1:23;
suppose
j = 0;
hence thesis by A1,A15,A16,A17,Th48,POLYNOM5:38;
end;
suppose
j = 1;
hence thesis by A15,A16,A17,Th48,COMPLFLD:8,POLYNOM5:38;
end;
suppose
j >= 2;
hence thesis by A15,A16,A17,Th48,COMPLFLD:7,POLYNOM5:38;
end;
end;
end;
suppose
A18: 0 < l;
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: G[l,x] by A13,A19,FINSEQ_1:1;
reconsider fl1 = f.(l+1) as Element of cPRFC by A8,A11,A14,
FINSEQ_2:11;
reconsider g1 = f | Seg (l+1) as FinSequence of cPRFC by FINSEQ_1:18;
reconsider p1 = Product(g1) as Polynomial of F_Complex by
POLYNOM3:def 10;
take p1;
take g1;
take p1;
thus g1 = f | Seg (l+1) & p1 = Product(g1) & p1 = p1;
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 cPRFC, 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 thesis
proof
per cases;
suppose
not (l+1) divides k or (l+1) = k;
then
A26: fl1p = <%1_F_Complex%> by A9,A11,A14;
consider r be FinSequence of F_Complex such that
A27: len r = 0+1 and
A28: p1.0 = Sum r and
A29: for m be 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
proof
per cases by A23;
suppose
p.0 = 1;
hence thesis by A31;
end;
suppose
p.0 = -1;
hence thesis by A31;
end;
end;
let j be Element of NAT;
consider r be FinSequence of F_Complex such that
len r = j+1 and
A32: p1.j = Sum r and
A33: for m be 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
let i be Element of NAT;
reconsider pi1 = p.(i-'1) as Integer by A24;
set j1i = j+1-'i;
now
A34: j1i = 0 or j1i >= 0+1 by NAT_1:13;
per cases by A34;
case
j1i = 0;
hence fl1p.j1i = 1 by A26,COMPLFLD:8,POLYNOM5:32;
end;
case
j1i >= 1;
hence fl1p.j1i = 0 by A26,COMPLFLD:7,POLYNOM5:32;
end;
end;
then reconsider fl1pj1i = fl1p.(j+1-'i) as Integer;
assume i in dom r;
then r.i = p.(i-'1) * fl1p.(j+1-'i) by A33
.= pi1 * fl1pj1i;
hence thesis;
end;
hence thesis by A32,Th4;
end;
suppose
A35: (l+1) divides k & (l+1) <> k;
consider r be FinSequence of F_Complex such that
A36: len r = 0+1 and
A37: p1.0 = Sum r and
A38: for m be 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 = cp(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
proof
per cases by A23;
suppose
p.0 = 1;
hence thesis by A3,A43,A41,A40;
end;
suppose
p.0 = -1;
hence thesis by A40,A44;
end;
end;
let j be Element of NAT;
consider r be FinSequence of F_Complex such that
len r = j+1 and
A45: p1.j = Sum r and
A46: for m be 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
let i be Element of NAT;
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;
then r.i = p.(i-'1) * fl1p.(j+1-'i) by A46
.= pi1 * fl1pj1i;
hence thesis;
end;
hence thesis by A45,Th4;
end;
end;
end;
end;
defpred C[Nat] means cp(k).$1 is integer;
A47: 0+1-'1 = 0 by NAT_D:34;
A48: H[0] by FINSEQ_1:1;
for l being Nat holds H[l] from NAT_1:sch 2(A48,A12 );
then
A49: for l being Nat st l in Seg len f ex x being object st G[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 G[i,F.i] from FINSEQ_1:
sch 1 (A49);
consider g being FinSequence of cPRFC, 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
let m be Nat;
reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
consider r be FinSequence of cFC such that
A56: len r = m+1 and
A57: unital_poly(F_Complex,k).m = Sum r and
A58: for l be Element of NAT st l in dom r holds r.l = p.(l-'1) *
(cp(k).(m1+1-'l)) by A10,POLYNOM3:def 9;
reconsider Src = Sum r as Element of COMPLEX by COMPLFLD:def 1;
now
per cases;
suppose
m1 = 0;
hence Src is integer by A1,A57,Th38;
end;
suppose
m1 = k;
hence Src is integer by A57,Th38,COMPLFLD:8;
end;
suppose
m1 <> 0 & m1 <> k;
hence Src is integer by A57,Th39,COMPLFLD:7;
end;
end;
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 s as Element of COMPLEX by COMPLFLD:def 1;
assume
A60: for n being Nat st n < m holds C[n];
now
let i be Element of NAT;
assume
A61: i in dom s;
per cases;
suppose
len r < 2;
then s = {} by FINSEQ_6:def 4;
hence s.i is integer;
end;
suppose
A62: 1+1 <= len r;
then
A63: len s +(1+1) = len r + 1 by FINSEQ_6:def 4;
per cases;
suppose
m = 0;
hence s.i is integer by A56,A62;
end;
suppose
A64: m > 0;
i <> 0 by A61,FINSEQ_3:25;
then reconsider cpkmi = cp(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 s by A61,FINSEQ_3:25;
then 1 <= i+1 & i+1 <= len s +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) * cp(k).(m+1-'(1+i)) by A58
.= p.(i+1-'1) * cp(k).(m+1-'1-'i) by NAT_2:30
.= p.i * cp(k).(m+1-'1-'i) by NAT_D:34
.= ppi *cpkmi by NAT_D:34;
i1 < len s by A66,A65,NAT_1:13;
then s.i = r.(1+1+i1) by A62,A65,FINSEQ_6:def 4
.= r.(1+i) by A65;
hence s.i is integer by A67;
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 cFC 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 s by A59,FVSUM_1:72;
then r1c = Sr -Ss;
then reconsider r1i = r1 as Integer;
A70: r1i = p.(1-'1) * cp(k).(m+1-'1) by A58,A69
.= p.0 * cp(k).m1 by A47,NAT_D:34;
per cases by A7,A11,A51,A52,FINSEQ_3:49;
suppose
p.0 = 1;
hence C[m] by A70;
end;
suppose
p.0 = -1;
then r1 = (-1_F_Complex) * cp(k).m1 by A70,COMPLFLD:8
.= -1_F_Complex * cp(k).m1
.= - cp(k).m1;
then 0.F_Complex = - cp(k).m1 + - r1 by RLVECT_1:def 10
.= -r1 - cp(k).m1;
then - r1 = cp(k).m by VECTSP_1:19;
then - r1i = cp(k).m;
hence C[m];
end;
end;
A71: for i being Nat holds C[i] from NAT_1:sch 4(A55);
consider r be FinSequence of cFC such that
A72: len r = 0+1 and
A73: unital_poly(F_Complex,k).0 = Sum r and
A74: for l be Element of NAT st l in dom r holds r.l = p.(l-'1) * (
cp(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 cFC by FINSEQ_2:11;
r = <*r1*> by A72,FINSEQ_1:40;
then
A76: Sum r = r.1 by RLVECT_1:44
.= p.0 * (cp(k).0) by A74,A47,A75;
cp(k).0 = 1 or cp(k).0 = -1
proof
per cases by A7,A11,A51,A52,FINSEQ_3:49;
suppose
p.0 = 1;
hence thesis by A1,A73,A76,Th38;
end;
suppose
p.0 = -1;
then -1_F_Complex = (-1_F_Complex) * cp(k).0 by A1,A73,A76,Th38
.= -1_F_Complex * cp(k).0
.= - cp(k).0;
hence thesis by COMPLFLD:8;
end;
end;
hence P[k] by A71;
end;
end;
for d being non zero Element of NAT holds P[d] from CompIndNE(A2);
hence thesis;
end;
theorem Th52: :: WEDDWITT
for d being non zero Element of NAT, z being Element of
F_Complex st z is Integer holds eval(cyclotomic_poly(d),z) is Integer
proof
let d be non zero Element of NAT,z be Element of F_Complex such that
A1: z is Integer;
set phi = cyclotomic_poly(d);
consider F being FinSequence of F_Complex such that
A2: eval(phi,z) = Sum F and
len F = len phi and
A3: for i being Element of NAT st i in dom F holds F.i = phi.(i-'1) * (
power F_Complex).(z,i-'1) by POLYNOM4:def 2;
for i being Element of NAT st i in dom F holds F.i is Integer
proof
let i be Element of NAT;
assume i in dom F;
then
A4: F.i = phi.(i-'1) * (power F_Complex).(z,i-'1) by A3;
reconsider i2 = (power F_Complex).(z,i-'1) as Integer by A1,Th13;
reconsider i1 = phi.(i-'1) as Integer by Th51;
F.i = i1*i2 by A4;
hence thesis;
end;
hence thesis by A2,Th14;
end;
theorem Th53:
for n, ni being non zero Element of NAT, f being FinSequence of
(the carrier of Polynom-Ring F_Complex), s being finite Subset of F_Complex st
s = {y where y is Element of MultGroup F_Complex : ord y divides n & not ord y
divides ni & ord y <> n} & dom f = Seg n & for i being non zero Element of NAT
st i in dom f 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)) holds Product(f) = poly_with_roots((s,1)-bag)
proof
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;
let f be FinSequence of cPRFC, s be finite Subset of F_Complex such that
A1: s = {y where y is Element of cMGFC: ord y divides n & not ord y
divides ni & ord y <> n} and
A2: dom f = Seg n and
A3: for i being non zero Element of NAT st i in dom f 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));
deffunc MG(Nat) = {y where y is Element of cMGFC : y in s & ord y <= $1 };
A4: now
let i be Element of NAT;
MG(i) c= s
proof
let x be object;
assume x in MG(i);
then ex y being Element of cMGFC st x = y & y in s & ord y <= i;
hence thesis;
end;
hence MG(i) is finite Subset of F_Complex by XBOOLE_1:1;
end;
then reconsider sB = MG(n) as finite Subset of F_Complex;
A5: len f = n by A2,FINSEQ_1:def 3;
defpred P[Nat,set] means for fi being FinSequence of cPRFC st fi = f|Seg $1
holds $2 = Product(fi);
A6: now
let i being Nat;
assume i in Seg len f;
reconsider fi = f|Seg i as FinSequence of cPRFC by FINSEQ_1:18;
set x = Product fi;
take x;
thus P[i,x];
end;
consider F being FinSequence of cPRFC such that
dom F = Seg len f and
A7: for i being Nat st i in Seg len f holds P[i,F.i] from FINSEQ_1:sch 5
( A6);
defpred R[Nat] means ex t being finite Subset of F_Complex st t =
MG($1) & F.$1 = poly_with_roots((t,1)-bag);
A8: for i being Element of NAT st 1 <= i & i < len f holds R[i] implies R[i +1]
proof
let i be Element of NAT such that
A9: 1 <= i and
A10: i < len f and
A11: R[i];
reconsider fi = f|Seg i as FinSequence of (the carrier of Polynom-Ring
F_Complex) by FINSEQ_1:18;
i in Seg len f by A9,A10,FINSEQ_1:1;
then
A12: F.i = Product fi by A7;
reconsider fi1 = f|Seg (i+1) as FinSequence of (the carrier of
Polynom-Ring F_Complex) by FINSEQ_1:18;
A13: i+1 <= len f by A10,NAT_1:13;
then i+1 = min(i+1,len f) by XXREAL_0:def 9;
then
A14: len fi1 = i+1 by FINSEQ_2:21;
i+1 in NAT by ORDINAL1:def 12;
then reconsider sB = MG(i+1) as finite Subset of F_Complex by A4;
take sB;
thus sB = MG(i+1);
set B = (sB, 1)-bag;
consider sb being finite Subset of F_Complex such that
A15: sb = MG(i) and
A16: F.i = poly_with_roots((sb,1)-bag) by A11;
1 <= i+1 by A9,NAT_1:13;
then
A17: i+1 in Seg len f by A13,FINSEQ_1:1;
then
A18: i+1 in dom f by FINSEQ_1:def 3;
A19: (f|Seg (i+1)).(i+1) = f.(i+1) by FINSEQ_1:4,FUNCT_1:49;
then reconsider
fi1d1 = fi1.(i+1) as Element of (the carrier of Polynom-Ring
F_Complex) by A18,FINSEQ_2:11;
reconsider fi1d1p = fi1d1 as Polynomial of F_Complex by POLYNOM3:def 10;
A20: F.(i+1) = Product fi1 by A7,A17;
set b = (sb, 1)-bag;
fi = fi1 | Seg i by Lm2,NAT_1:12;
then fi1 = fi ^ <* fi1d1 *> by A14,FINSEQ_3:55;
then Product fi1 = Product fi * fi1d1 by GROUP_4:6;
then
A21: Product fi1=(poly_with_roots b)*' fi1d1p by A12,A16,POLYNOM3:def 10;
per cases;
suppose
A22: not (i+1) divides n or (i+1) divides ni or i+1 = n;
A23: now
let x be object;
hereby
assume x in sB;
then consider y being Element of MultGroup F_Complex such that
A24: x = y and
A25: y in s and
A26: ord y <= i+1;
ex y1 being Element of cMGFC st y = y1 & ord y1 divides n & not
ord y1 divides ni & ord y1 <> n by A1,A25;
then ord y < i+1 by A22,A26,XXREAL_0:1;
then ord y <= i by NAT_1:13;
hence x in sb by A15,A24,A25;
end;
assume x in sb;
then consider y being Element of MultGroup F_Complex such that
A27: x = y & y in s and
A28: ord y <= i by A15;
ord y <= i+1 by A28,NAT_1:12;
hence x in sB by A27;
end;
f.(i+1) = <%1_F_Complex%> by A3,A18,A22;
then F.(i+1) = (poly_with_roots b) by A20,A19,A21,UPROOTS:32
.= poly_with_roots(B) by A23,TARSKI:2;
hence thesis;
end;
suppose
A29: (i+1) divides n & not (i+1) divides ni & (i+1) <> n;
consider scb being non empty finite Subset of F_Complex such that
A30: scb = { y where y is Element of cMGFC : ord y = i+1 } and
A31: cyclotomic_poly(i+1) = poly_with_roots((scb,1)-bag) by Def5;
now
let x be object;
hereby
assume x in sB;
then consider y being Element of cMGFC such that
A32: x = y and
A33: y in s and
A34: ord y <= i+1;
ord y <= i or ord y = i+1 by A34,NAT_1:8;
then y in sb or y in scb by A15,A30,A33;
hence x in sb \/ scb by A32,XBOOLE_0:def 3;
end;
assume
A35: x in sb \/ scb;
per cases by A35,XBOOLE_0:def 3;
suppose
x in sb;
then consider y being Element of cMGFC such that
A36: x = y & y in s and
A37: ord y <= i by A15;
ord y <= i+1 by A37,NAT_1:12;
hence x in sB by A36;
end;
suppose
x in scb;
then consider y being Element of cMGFC such that
A38: x = y and
A39: ord y = i+1 by A30;
y in s by A1,A29,A39;
hence x in sB by A38,A39;
end;
end;
then
A40: sB = sb \/ scb by TARSKI:2;
set cb = (scb,1)-bag;
A41: sb misses scb
proof
assume sb /\ scb <> {};
then consider x being object such that
A42: x in sb /\ scb by XBOOLE_0:def 1;
x in scb by A42,XBOOLE_0:def 4;
then
A43: ex y2 being Element of cMGFC st x = y2 & ord y2 = i+1 by A30;
x in sb by A42,XBOOLE_0:def 4;
then ex y1 being Element of cMGFC st x = y1 & y1 in s & ord y1 <= i by
A15;
hence contradiction by A43,NAT_1:13;
end;
f.(i+1) = poly_with_roots(cb) by A3,A18,A29,A31;
then F.(i+1) = (poly_with_roots b)*' poly_with_roots(cb) by A7,A17,A19
,A21
.= poly_with_roots (b+cb) by UPROOTS:64
.= poly_with_roots(B) by A40,A41,UPROOTS:10;
hence thesis;
end;
end;
now
let x be object;
hereby
assume
A44: x in s;
then consider y being Element of MultGroup F_Complex such that
A45: x = y and
A46: ord y divides n and
not ord y divides ni and
ord y <> n by A1;
ord y <= n by A46,NAT_D:7;
hence x in sB by A44,A45;
end;
assume x in sB;
then ex y being Element of MultGroup F_Complex st y = x & y in s & ord y
<= n;
hence x in s;
end;
then
A47: s = sB by TARSKI:2;
A48: 0+1 <= n by NAT_1:13;
A49: R[1]
proof
reconsider t = MG(1) as finite Subset of F_Complex by A4;
take t;
thus t = MG(1);
reconsider f1 = f|Seg 1 as FinSequence of cPRFC by FINSEQ_1:18;
A50: 1 in dom f by A5,A48,FINSEQ_3:25;
A51: 1 divides ni by NAT_D:6;
now
assume t is non empty;
then consider x being object such that
A52: x in t;
consider y being Element of cMGFC such that
x = y and
A53: y in s and
A54: ord y <= 1 by A52;
consider y1 being Element of cMGFC such that
A55: y = y1 and
A56: ord y1 divides n and
A57: not ord y1 divides ni and
ord y1 <> n by A1,A53;
now
assume ord y1 = 0;
then ex u being Nat st n = 0 * u by A56,NAT_D:def 3;
hence contradiction;
end;
then 0+1 <= ord y1 by NAT_1:13;
hence contradiction by A51,A54,A55,A57,XXREAL_0:1;
end;
then
A58: (t,1)-bag = EmptyBag the carrier of F_Complex by UPROOTS:9;
A59: 1 in Seg len f by A5,A48,FINSEQ_1:1;
then 1 in dom f by FINSEQ_1:def 3;
then reconsider fd1 = f.1 as Element of cPRFC by FINSEQ_2:11;
f1 = <*f.1*> by A5,A48,Th1;
then F.1 = Product <*fd1*> by A7,A59
.= fd1 by FINSOP_1:11
.= <%1_F_Complex%> by A3,A50,A51;
hence thesis by A58,UPROOTS:60;
end;
for i being Element of NAT st 1 <= i & i <= len f holds R[i] from
INT_1:sch 7 (A49,A8);
then f = f|Seg len f & ex S being finite Subset of F_Complex st S = MG(len
f) & F.len f = poly_with_roots((S,1)-bag) by A5,A48,FINSEQ_3:49;
hence thesis by A5,A7,A47,FINSEQ_1:3;
end;
theorem Th54:
for n, ni being non zero Element of NAT st ni < n & ni divides
n ex f being FinSequence of (the carrier of Polynom-Ring F_Complex), 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
proof
set cMGFC = the carrier of MultGroup F_Complex;
set cPRFC = the carrier of Polynom-Ring F_Complex;
let n, ni being non zero Element of NAT such that
A1: ni < n and
A2: ni divides n;
set rbp = {y where y is Element of cMGFC: ord y divides n & not ord y
divides ni & ord y <> n};
rbp c= n-roots_of_1
proof
let x be object;
assume x in rbp;
then ex y being Element of cMGFC st x = y & ord y divides n & not ord y
divides ni & ord y <> n;
hence thesis by Th34;
end;
then reconsider rbp as finite Subset of F_Complex by XBOOLE_1:1;
A3: n-roots_of_1 c= cMGFC by Th32;
set bp = (rbp,1)-bag;
defpred P[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
let i be Nat;
assume
A5: i in Seg n;
then
A6: i is non zero by FINSEQ_1:1;
per cases;
suppose
A7: not i divides n or i divides ni or i = n;
<%1_F_Complex%> is Element of cPRFC by POLYNOM3:def 10;
hence ex x being Element of cPRFC st P[i,x] by A6,A7;
end;
suppose
A8: i divides n & not i divides ni & i <> n;
reconsider i9 = i as non zero Element of NAT by A5,FINSEQ_1:1;
cyclotomic_poly(i9) is Element of cPRFC by POLYNOM3:def 10;
hence ex x being Element of cPRFC st P[i,x] by A8;
end;
end;
consider f being FinSequence of cPRFC such that
A9: dom f = Seg n and
A10: for i being Nat st i in Seg n holds P[i,f.i] from FINSEQ_1:sch 5(A4
);
A11: now
let i be non zero Element of NAT;
assume i in Seg n;
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)
);
end;
then Product(f) = poly_with_roots(bp) by A9,Th53;
then reconsider p = Product(f) as Polynomial of F_Complex;
take f;
take p;
thus p = Product(f);
thus dom f = Seg n by A9;
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;
set b = (n-roots_of_1, 1)-bag, 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 cMGFC: 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 <> {};
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 cMGFC 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 cMGFC st x = y & ord y divides ni by Th36;
hence contradiction by A1,A15,NAT_D:7;
end;
then
A16: bi + bn = (ni-roots_of_1 \/ rbn, 1)-bag by UPROOTS:10;
set rbibn = (ni-roots_of_1) \/ rbn;
reconsider rbibn as finite Subset of F_Complex;
A17: ni-roots_of_1 c= n-roots_of_1 by A2,Th28;
now
let x be object;
hereby
assume
A18: x in n-roots_of_1;
then reconsider y = x as Element of cMGFC by A3;
A19: ord y divides n by A18,Th34;
per cases;
suppose
ord y = n;
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;
end;
suppose
ord y <> n & not ord y divides ni;
then y in rbp by A19;
hence x in rbibn \/ rbp by XBOOLE_0:def 3;
end;
suppose
ord y <> n & ord y divides ni;
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;
end;
end;
assume x in rbibn \/ rbp;
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;
hence x in n-roots_of_1 by A17;
end;
suppose
x in rbn;
then ex y being Element of cMGFC st x = y & ord y = n by A12;
hence x in n-roots_of_1 by Th34;
end;
suppose
x in rbp;
then
ex y being Element of cMGFC st x = y & ord y divides n & ( not ord y
divides ni)& ord y <> n;
hence x in n-roots_of_1 by Th34;
end;
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(bi) by Th46;
rbibn misses rbp
proof
assume rbibn /\ rbp <> {};
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 cMGFC 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;
then ex y being Element of cMGFC st x = y & ord y divides ni by Th36;
hence contradiction by A24;
end;
suppose
x in rbn;
then ex y being Element of cMGFC st x = y & ord y = n by A12;
hence contradiction by A24;
end;
end;
then
A26: b = bibn+bp by A21,UPROOTS:10;
unital_poly(F_Complex,n) = poly_with_roots(b) by Th46
.= (poly_with_roots bibn) *' poly_with_roots(bp) by A26,UPROOTS:64
.= unital_poly(F_Complex,ni)*'(cyclotomic_poly n)*'poly_with_roots(bp)
by A13,A16,A22,UPROOTS:64;
hence thesis by A9,A11,Th53;
end;
theorem Th55:
for i being Integer, c being Element of F_Complex, f being
FinSequence of (the carrier of Polynom-Ring F_Complex), p being Polynomial of
F_Complex st p = Product(f) & c = i & for i being non zero Element of NAT st i
in dom f holds f.i = <%1_F_Complex%> or f.i = cyclotomic_poly(i) holds eval(p,c
) is integer
proof
A1: 1_.(F_Complex) = 1_F_Complex * 1_.(F_Complex) by POLYNOM5:27
.= <%1_F_Complex%> by POLYNOM5:29;
let i be Integer, c be Element of F_Complex, 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: c = i and
A4: for i being non zero Element of NAT st i in dom f holds f.i = <%
1_F_Complex%> or f.i = cyclotomic_poly(i);
A5: eval(1_.F_Complex,c) = 1 by COMPLFLD:8,POLYNOM4:18;
per cases;
suppose
len f = 0;
then f = <*>(the carrier of Polynom-Ring F_Complex);
then p = 1_Polynom-Ring F_Complex by A2,GROUP_4:8
.= 1.Polynom-Ring F_Complex;
hence thesis by A5,POLYNOM3:def 10;
end;
suppose
A6: 0 < len f;
defpred P[Nat,set] means for fi being FinSequence of (the carrier of
Polynom-Ring F_Complex) st fi = f|Seg $1 holds $2 = Product(fi);
A7: f = f|Seg len f by FINSEQ_3:49;
A8: now
let i be Nat;
assume i in Seg len f;
reconsider fi = f|Seg i as FinSequence of (the carrier of Polynom-Ring
F_Complex) by FINSEQ_1:18;
set x = Product fi;
take x;
thus P[i,x];
end;
consider F being FinSequence of (the carrier of Polynom-Ring F_Complex)
such that
dom F = Seg len f and
A9: for i being Nat st i in Seg len f holds P[i,F.i] from FINSEQ_1:
sch 5( A8);
defpred R[Nat] means ex r being Polynomial of F_Complex st r =
F.$1 & eval(r,c) is integer;
A10: now
let i be Element of NAT such that
A11: 1 <= i and
A12: i < len f;
A13: i in Seg len f by A11,A12,FINSEQ_1:1;
reconsider fi1 = f|Seg (i+1) as FinSequence of (the carrier of
Polynom-Ring F_Complex) by FINSEQ_1:18;
A14: i+1 <= len f by A12,NAT_1:13;
then i+1 = min(i+1,len f) by XXREAL_0:def 9;
then
A15: len fi1 = i+1 by FINSEQ_2:21;
1 <= i+1 by A11,NAT_1:13;
then
A16: i+1 in Seg len f by A14,FINSEQ_1:1;
then
A17: i+1 in dom f by FINSEQ_1:def 3;
reconsider fi = f|Seg i as FinSequence of (the carrier of Polynom-Ring
F_Complex) by FINSEQ_1:18;
assume
A18: R[i];
A19: (f|Seg (i+1)).(i+1) = f.(i+1) by FINSEQ_1:4,FUNCT_1:49;
then reconsider
fi1d1 = fi1.(i+1) as Element of (the carrier of Polynom-Ring
F_Complex) by A17,FINSEQ_2:11;
reconsider pfi1 = Product fi1, pfi = Product fi as Polynomial of
F_Complex by POLYNOM3:def 10;
reconsider fi1d1p = fi1d1 as Polynomial of F_Complex by POLYNOM3:def 10;
fi = fi1 | Seg i by Lm2,NAT_1:12;
then fi1 = fi ^ <* fi1d1 *> by A15,FINSEQ_3:55;
then
A20: Product fi1 = Product fi * fi1d1 by GROUP_4:6;
thus R[i+1]
proof
reconsider epfi = eval(pfi,c), efi1d1p = eval(fi1d1p,c) as Element of
COMPLEX by COMPLFLD:def 1;
now
reconsider i1 = i+1 as non zero Element of NAT by ORDINAL1:def 12;
per cases by A4,A17;
suppose
f.i1 = <%1_F_Complex%>;
hence eval(fi1d1p,c) is integer by A5,A1,FINSEQ_1:4,FUNCT_1:49;
end;
suppose
f.i1 = cyclotomic_poly(i1);
hence eval(fi1d1p,c) is integer by A3,A19,Th52;
end;
end;
then reconsider iefi1d1p = efi1d1p as Integer;
reconsider iepfi = epfi as Integer by A9,A18,A13;
take pfi1;
thus pfi1 = F.(i+1) by A9,A16;
pfi1 = pfi *' fi1d1p by A20,POLYNOM3:def 10;
then eval(pfi1, c) = eval(pfi,c) * eval(fi1d1p,c) by POLYNOM4:24
.= iepfi * iefi1d1p;
hence thesis;
end;
end;
A21: 0+1 <= len f by A6,NAT_1:13;
then
A22: 1 in Seg len f by FINSEQ_1:1;
A23: R[1]
proof
reconsider f1 = f | Seg 1 as FinSequence of (the carrier of Polynom-Ring
F_Complex) by FINSEQ_1:18;
A24: 1 in dom f by A22,FINSEQ_1:def 3;
then reconsider fd1 = f.1 as Element of (the carrier of Polynom-Ring
F_Complex) by FINSEQ_2:11;
reconsider fd1 as Polynomial of F_Complex by POLYNOM3:def 10;
take fd1;
f1 = <*f.1*> by A21,Th1;
hence fd1 = Product f1 by FINSOP_1:11
.= F.1 by A9,A22;
per cases by A4,A24;
suppose
f.1 = <%1_F_Complex%>;
hence thesis by A1,COMPLFLD:8,POLYNOM4:18;
end;
suppose
f.1 = cyclotomic_poly(1);
hence thesis by A3,Th52;
end;
end;
for i being Element of NAT st 1 <= i & i <= len f holds R[i] from
INT_1:sch 7 (A23,A10);
then ex r being Polynomial of F_Complex st r = F.len f & eval (r,c) is
integer by A21;
hence thesis by A2,A6,A9,A7,FINSEQ_1:3;
end;
end;
theorem Th56:
for n being non zero Element of NAT, j, k, q being Integer, qc
being Element of F_Complex st qc = q & j = eval(cyclotomic_poly(n),qc) & k =
eval(unital_poly(F_Complex, n),qc) holds j divides k
proof
let n be non zero Element of NAT, j,k,q being Integer, qc being Element of
F_Complex such that
A1: qc = q and
A2: j = eval(cyclotomic_poly(n),qc) and
A3: k = eval(unital_poly(F_Complex, n),qc);
set jfc = eval(cyclotomic_poly(n),qc);
per cases by NAT_1:53;
suppose
n = 1;
hence thesis by A2,A3,Th48;
end;
suppose
A4: n > 1;
set eup1fc = eval(unital_poly(F_Complex,1),qc);
reconsider eup1 = eup1fc as Integer by A1,Th47;
consider f being FinSequence of (the carrier of Polynom-Ring F_Complex), p
being Polynomial of F_Complex such that
A5: p = Product(f) and
A6: 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 1 or i = n implies f.i = <%1_F_Complex%>)
& (i divides n & not i divides 1 & i <> n implies f.i = cyclotomic_poly(i))
and
A7: unital_poly(F_Complex,n) = unital_poly(F_Complex,1)*'(
cyclotomic_poly n)*'p by A4,Th54,NAT_D:6;
set epfc = eval(p,qc);
now
let i be non zero Element of NAT;
assume
A8: i in dom f;
per cases;
suppose
not i divides n or i divides 1 or i = n;
hence f.i = <%1_F_Complex%> or f.i = cyclotomic_poly(i) by A6,A8;
end;
suppose
i divides n & not i divides 1 & i <> n;
hence f.i = <%1_F_Complex%> or f.i = cyclotomic_poly(i) by A6,A8;
end;
end;
then reconsider ep = epfc as Integer by A1,A5,Th55;
k = eval((unital_poly(F_Complex,1)*'cyclotomic_poly(n)),qc) * epfc by A3,A7
,POLYNOM4:24;
then k = eup1fc * jfc * epfc by POLYNOM4:24;
then k = eup1 * ep * j by A2;
hence thesis by INT_1:def 3;
end;
end;
theorem Th57:
for n,ni being non zero Element of NAT, q being Integer st ni <
n & ni divides n for qc being Element of F_Complex st qc = q 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)
proof
let n,ni be non zero Element of NAT, q being Integer such that
A1: ni < n & ni divides n;
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) = ttt *' p by A1,Th54;
A5: now
let i being non zero Element of NAT such that
A6: i in dom f;
per cases;
suppose
not i divides n or i divides ni or i = n;
hence f.i = <%1_F_Complex%> or f.i = cyclotomic_poly(i) by A3,A6;
end;
suppose
i divides n & not i divides ni & i <> n;
hence f.i = <%1_F_Complex%> or f.i = cyclotomic_poly(i) by A3,A6;
end;
end;
let qc be Element of F_Complex;
assume qc = q;
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 such that
A8: j = eval(cyclotomic_poly(n),qc) & k = eval(unital_poly(F_Complex,n),
qc) & l = eval(unital_poly(F_Complex,ni),qc);
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(ttt,qc) * eval(p,qc) by A4,
POLYNOM4:24;
then
A9: k = lcf*jcf*mcf by A8,A7,POLYNOM4:24
.= l*j*m;
now
per cases;
suppose
A10: l <> 0;
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;
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 thesis by INT_1:def 3;
end;
suppose
l = 0;
then k div l = 0;
hence thesis by INT_2:12;
end;
end;
hence thesis;
end;
theorem
for n,q being non zero Element of NAT, qc being Element of F_Complex
st qc = q for j being Integer st j = eval(cyclotomic_poly(n),qc) holds j
divides (q |^ n - 1)
proof
let n,q be non zero Element of NAT;
let qc be Element of F_Complex such that
A1: qc = q;
A2: ex y1 being Element of F_Complex st y1 = q & eval( unital_poly(F_Complex,
n),y1) = (q |^ n) - 1 by Th44;
let j be Integer;
assume j = eval(cyclotomic_poly(n),qc);
hence thesis by A1,A2,Th56;
end;
theorem
for n,ni,q being non zero Element of NAT st ni < n & ni divides n for
qc being Element of F_Complex st qc = q for j being Integer st j = eval(
cyclotomic_poly(n),qc) holds j divides ((q |^ n - 1) div (q |^ ni - 1))
proof
let n,ni,q be non zero Element of NAT such that
A1: ni < n & ni divides n;
let qc be Element of F_Complex such that
A2: qc = q;
A3: (ex y1 being Element of F_Complex st y1 = q & eval( unital_poly(
F_Complex,n) ,y1) = (q |^ n) - 1 )& ex y2 being Element of F_Complex st y2=q &
eval( unital_poly(F_Complex,ni),y2) = (q |^ ni) - 1 by Th44;
let j be Integer;
assume j = eval(cyclotomic_poly(n),qc);
hence thesis by A1,A2,A3,Th57;
end;
theorem
for n being non zero Element of NAT st 1 < n for q being Element of
NAT st 1 < q for qc being Element of F_Complex st qc = q for i being Integer st
i = eval(cyclotomic_poly(n),qc) holds |.i.| > q - 1
proof
set MGFC = MultGroup F_Complex;
set cMGFC = the carrier of MultGroup F_Complex;
let n be non zero Element of NAT such that
A1: 1 < n;
consider S being non empty finite Subset of F_Complex such that
A2: S = {y where y is Element of cMGFC : ord y = n} and
A3: cyclotomic_poly(n) = poly_with_roots((S,1)-bag) by Def5;
rng canFS(S) = S by FUNCT_2:def 3;
then reconsider fs = canFS(S) as FinSequence of F_Complex by FINSEQ_1:def 4;
let q be Element of NAT such that
A4: 1 < q;
let qc be Element of F_Complex such that
A5: qc = q;
deffunc F(set) = |.qc - fs/.$1.|;
consider p1 being FinSequence such that
A6: len p1 = len fs & for i being Nat st i in dom p1 holds p1.i = F(i)
from FINSEQ_1:sch 2;
A7: for i being Element of NAT, c being Element of F_Complex st i in dom p1
& c = (canFS(S)).i holds p1.i = |.qc - c.|
proof
let i be Element of NAT, c being Element of F_Complex such that
A8: i in dom p1 and
A9: c = (canFS(S)).i;
i in dom fs by A6,A8,FINSEQ_3:29;
then fs/.i = (canFS(S)).i by PARTFUN1:def 6;
hence thesis by A6,A8,A9;
end;
for x being object st x in rng p1 holds x in REAL
proof
let x be object;
assume x in rng p1;
then consider i being Nat such that
A10: i in dom p1 and
A11: p1.i = x by FINSEQ_2:10;
i in dom fs by A6,A10,FINSEQ_3:29;
then fs/.i = (canFS(S)).i by PARTFUN1:def 6;
then x = F(i) by A7,A10,A11;
hence thesis by XREAL_0:def 1;
end;
then rng p1 c= REAL;
then reconsider ps=p1 as non empty FinSequence of REAL by A6,FINSEQ_1:def 4;
len fs = card S by FINSEQ_1:93;
then
A12: |.eval(cyclotomic_poly(n),qc).| = Product(ps) by A3,A6,A7,Th3;
A13: rng fs = S by FUNCT_2:def 3;
A14: for i being Element of NAT st i in dom ps holds ps.i > q - 1
proof
let i be Element of NAT such that
A15: i in dom ps;
i in dom fs by A6,A15,FINSEQ_3:29;
then fs/.i = (canFS(S)).i by PARTFUN1:def 6;
then
A16: ps.i = |.[**q,0**] - fs/.i.| by A5,A7,A15;
A17: i in dom fs by A6,A15,FINSEQ_3:29;
then fs.i in rng fs by FUNCT_1:3;
then fs/.i in rng fs by A17,PARTFUN1:def 6;
then
A18: ex y being Element of MGFC st fs/.i = y & ord y = n by A2,A13;
A19: now
assume
A20: fs/.i = [**1,0**];
1_MultGroup F_Complex = [**1, 0**] by Th17,COMPLFLD:8;
hence contradiction by A1,A18,A20,GROUP_1:42;
end;
fs/.i in n-roots_of_1 by A18,Th34;
then |.fs/.i.| = 1 by Th23;
hence thesis by A4,A16,A19,Th6;
end;
reconsider qi=q as Integer;
1+1 <= qi by A4,INT_1:7;
then
A21: 1+1+-1 <= qi +-1 by XREAL_1:7;
let i be Integer;
reconsider x = q-1 as Real;
assume i = eval(cyclotomic_poly(n),qc);
then |.i.| > x by A21,A12,A14,Th7;
hence |.i.| > q - 1;
end;