:: Primitive Roots of Unity and Cyclotomic Polynomials
::  by Broderick Arneson and Piotr Rudnicki
::
:: Received December 30, 2003
:: Copyright (c) 2003-2012 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, XREAL_0, ORDINAL1, 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, NUMBERS, XREAL_0,
      ZFMISC_1, XXREAL_0, COMPLEX1, REAL_1, SQUARE_1, INT_1, INT_2, ORDINAL1,
      NAT_D, PREPOWER, POWER, BINOP_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
      FINSEQ_1, RAT_1, DOMAIN_1, FINSET_1, BINOP_2, STRUCT_0, ALGSTR_0,
      VECTSP_2, VECTSP_1, GROUP_4, RVSUM_1, 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;
 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_2,
      HAHNBAN1, GRAPH_2, POLYNOM4, POLYNOM5, UPROOTS, SEQ_1, RECDEF_1, BINOP_2,
      RELSET_1, PBOOLE, FUNCT_7, NEWTON, FVSUM_1;
 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, UPROOTS, RELSET_1,
      PRE_POLY, XBOOLE_0, ZFMISC_1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
 definitions TARSKI, GROUP_1, XBOOLE_0, BINOP_1, REALSET1, SQUARE_1, HAHNBAN1,
      POLYNOM3, FINSEQ_2, COMPLEX1, GROUP_4, ALGSTR_0, STRUCT_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;
 schemes NAT_1, FUNCT_2, FINSEQ_1, INT_1, RECDEF_1;

begin :: Preliminaries

Lm1: for k being Element of NAT holds k is non empty iff 1 <= k
proof
  let k be Element of NAT;
  hereby
    assume k is non empty;
    then 0+1 <= k by NAT_1:13;
    hence 1 <= k;
  end;
  assume 1 <= k;
  hence thesis;
end;

scheme
  CompIndNE { P[non empty Nat] } : for k being non empty Element of NAT holds
  P[k]
provided
A1: for k being non empty Element of NAT st for n being non empty
Element of NAT st n < k holds P[n] holds P[k]
proof
  let k be non empty Element of NAT;
  defpred R[Nat] means ex m being non empty 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 empty Element of NAT by A3,ORDINAL1:def 12;
    now
      let n be non empty 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 empty 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
proof
  let f be FinSequence, n, i be Element of NAT;
  assume i <= n;
  then Seg i c= Seg n by FINSEQ_1:5;
  hence thesis by RELAT_1:74;
end;

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[Element of 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 cFC = the carrier of F_Complex;
  set FC = F_Complex;
A1: for i being Element of NAT st P[i] holds P[i+1]
  proof
    let i being Element of 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 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 Element of NAT holds P[i] from NAT_1:sch 1(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 UPROOTS:3;
  then
A3: dom canFS(s) = Seg card s by FINSEQ_1:def 3;
A4: for k being Element of NAT st k in Seg card s ex y being Element of FC
  st P[k,y]
  proof
    let k be Element of 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 Element of 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[Element of 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 Element of NAT st P[n] holds P[n+1]
  proof
    let n be Element of 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 Element of NAT holds P[n] from NAT_1:sch 1(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 by POLYNOM5:6
    .= (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 set 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 Real by ZFMISC_1:31;
  defpred P[Element of 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 Element of NAT st P[k] holds P[k+1]
  proof
    let k be Element of 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 set 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 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 Element of NAT holds P[k] from NAT_1:sch 1(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,POWER:26;
  hence thesis;
end;

theorem Th9:
  for n, i being Element of 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 Element of 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 Element of 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 Element of 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 Element of 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
  Element of NAT;
  defpred P[Element of NAT] means (power L).(x,n*$1) = (power L).((power L).(x
  ,n),$1);
  set pL = power L;
A1: for m being Element of NAT st P[m] holds P[m+1]
  proof
    let m be Element of NAT such that
A2: P[m];
    thus pL.(x,n*(m+1)) = pL.(x,n*m+n*1) .= pL.(x,n*m)*pL.(x,n) by POLYNOM2:1
      .= pL.(pL.(x,n),m+1) by A2,GROUP_1:def 7;
  end;
  pL.(x,n*(0 qua Nat)) = 1_L by GROUP_1:def 7
    .= pL.(pL.(x,n),0) by GROUP_1:def 7;
  then
A3: P[0];
  thus for m being Element of NAT holds P[m] from NAT_1:sch 1(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[Element of NAT] means (power F_Complex).(x,$1) is Integer;
A2: now
    reconsider i1=x as Integer by A1;
    let k be Element of NAT;
    assume P[k];
    then reconsider i2=(power F_Complex).(x,k) as Integer;
    (power F_Complex).(x,k)*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 Element of NAT holds P[k] from NAT_1:sch 1(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[Element of 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 Element of NAT st P[k] holds P[k+1]
  proof
    let k be Element of 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 set 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 Element of NAT holds P[k] from NAT_1:sch 1(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 set;
      assume x in [:ccs,ccs:];
      then ex a,b being set 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 set;
      assume y in rng mcs;
      then consider x being set 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 set 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 by VECTSP_1:def 4;
      thus e * h = (1_R)*h9 by A9
        .= h by VECTSP_1:def 8;
      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 by VECTSP_1:def 4;
    hence h * uR = h by Th16;
    1_R * g = g by VECTSP_1:def 8;
    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 set;
  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 empty 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 set st x in H holds x in the carrier of F_Complex
    proof
      let x be set;
      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 empty 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 empty 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 empty Element of NAT holds 1_F_Complex in n -roots_of_1
proof
  let n be non empty 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 empty Element of NAT, x being Element of
  F_Complex st x in n-roots_of_1 holds |.x.| = 1
proof
  let n be non empty 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 F_Complex).(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 empty 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 empty 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 F_Complex).(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 number 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)**];
    0+1<=n by NAT_1:13;
    then n-root 1 = 1 by POWER:6;
    then 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 empty 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 empty 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 empty 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 empty 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 set;
    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:1;
end;

theorem Th27:
  for n being non empty Element of NAT holds card (n-roots_of_1) = n
proof
  let n be non empty 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[set, set] 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 set st x in Seg n ex y being set st y in Y & P[x,y]
  proof
    let x be set 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 set st x in Seg n holds P[x,F.x] from FUNCT_2:sch 1(A2);
  for c being set st c in X ex x being set st x in Seg n & c = F.x
  proof
    let c be set;
    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 set st x1 in dom F & x2 in dom F & F.x1=F.x2 holds x1= x2
  proof
    let x1,x2 be set 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 empty 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 empty Element of NAT st ni divides n holds
  ni-roots_of_1 c= n-roots_of_1
proof
  let n,ni be non empty 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 set st x in ni-roots_of_1 holds x in n-roots_of_1
  proof
    let x be set 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 by TARSKI:def 3;
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 Element of 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[Element of NAT] means (power (MultGroup R)).(x,$1) = (power R).(y,
  $1);
A2: for k be Element of NAT st P[k] holds P[k+1]
  proof
    let k be Element of NAT such that
A3: P[k];
    thus (power (MultGroup R)).(x,k+1) = (power (MultGroup R)).(x,k) * x by
GROUP_1:def 7
      .= (power R).(y,k) * 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 Element of NAT holds P[k] from NAT_1:sch 1(A4,A2);
end;

theorem Th30:
  for n being non empty 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 empty 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 by GROUP_1:def 10;
end;

theorem Th31:
  for n being non empty 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 empty 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;
A8: vn is not empty by A2;
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_relative_prime 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 A13,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 A8,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 empty Element of NAT holds n-roots_of_1 c= the
  carrier of MultGroup F_Complex
proof
  let n be non empty Element of NAT;
  set cMGFC = the carrier of MultGroup F_Complex;
  set FC = F_Complex;
  let a be set;
  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 empty Element of NAT holds ex x being Element of
  MultGroup F_Complex st ord x = n
proof
  let n be non empty 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 by NAT_2:4;
end;

theorem Th34:
  for n being non empty 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 empty 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 empty 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 empty 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 set;
    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:1;
end;

theorem Th36:
  for n being non empty 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 empty 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 empty 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 set st x in X holds mru.x in n-roots_of_1
    proof
      let x be set such that
A5:   x in X;
      consider a,b being set 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 empty 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 empty 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 empty 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 %> by
POLYNOM5:def 4;

theorem Th38:
  for L being left_unital non empty doubleLoopStr for n being
non empty 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 empty 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 empty 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 empty 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 empty 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 empty 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;
  for i being Nat st i >= n+1 holds unital_poly(L,n).i=0.L
  proof
    let i be Nat such that
A3: i >= n+1;
    now
A4:   n + 0 < n + 1 by XREAL_1:8;
      assume i = n;
      hence contradiction by A3,A4;
    end;
    hence thesis by A3,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;
end;

registration
  let L be non degenerated well-unital non empty doubleLoopStr, n be non
  empty 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 empty 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 empty 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 by COMPLFLD:8;
    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) by VECTSP_1:def 8;
            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:2,7,FVSUM_1:76;
  hence thesis by A2,COMPLFLD:8;
end;

theorem Th42:
  for n being non empty Element of NAT holds Roots unital_poly(
  F_Complex, n) = n-roots_of_1
proof
  let n be non empty Element of NAT;
  now
    set p = unital_poly(F_Complex,n);
    let x be set;
    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 9;
      then 0.F_Complex = eval(p,x9) by POLYNOM5:def 6
        .= (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 6;
    hence x in Roots unital_poly(F_Complex,n) by POLYNOM5:def 9;
  end;
  hence thesis by TARSKI:1;
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[Element of NAT] means (power F_Complex).(z,$1) = x |^ $1;
A7: for n being Element of NAT st P[n] holds P[n+1]
    proof
      let n be Element of NAT such that
A8:   P[n];
      (power F_Complex).(z,n+1) = (power F_Complex).(z,n)*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 Element of NAT holds P[n] from NAT_1:sch 1(A9,A7);
    then (power F_Complex).(z,n) = x |^ n;
    hence thesis;
  end;
end;

theorem Th44:
  for n being non empty 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 empty 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 empty Element of NAT holds BRoots unital_poly(
  F_Complex, n) = (n-roots_of_1, 1)-bag
proof
  let n being non empty 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 empty Element of NAT holds unital_poly(F_Complex
  , n) = poly_with_roots((n-roots_of_1, 1)-bag)
proof
  let n be non empty 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 empty 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 empty Element of NAT;
  let i be Element of F_Complex such that
A1: i is Integer;
  reconsider j = i as Integer by A1;
  i is Real by A1,XREAL_0:def 1;
  then
  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 empty 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 empty 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 set;
      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 by NAT_2:4;
    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 set;
    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:1;
  hence thesis by A2,Lm4,Th46;
end;

theorem Th49:
  for n being non empty Element of NAT, f being FinSequence of (
  the carrier of Polynom-Ring F_Complex) st len f = n & for i being non empty
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 empty 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 empty 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[Element of 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 set;
      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;
    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 set;
        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:1;
      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 set;
        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:1;
      set cb = (scb,1)-bag;
A39:  sb misses scb
      proof
        assume sb /\ scb <> {};
        then consider x being set 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 set;
      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:1;
  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 set;
    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:1;
  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 empty 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 empty 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 empty Element of NAT;
  defpred P[set,set] means ex i being non empty 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 Element of NAT st k in Seg n ex x being Element of cPRFC st
  P[k,x]
  proof
    let k be Element of NAT;
    assume k in Seg n;
    then reconsider i = k as non empty 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 Element of 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 empty Element of NAT;
    assume
A9: i in dom f;
    then
A10: i <= n by A5,FINSEQ_1:1;
    (ex j being non empty 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 empty 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 empty 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%> by FINSEQ_1:40;
      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 empty 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 empty Element of NAT) = cyclotomic_poly($1);
  set cPRFC = the carrier of Polynom-Ring F_Complex;
  set cFC = the carrier of F_Complex;
  defpred P[non empty 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:2,8;
A2: now
    let k be non empty Element of NAT such that
A3: for n being non empty 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 empty 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,set] 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[Element of NAT] means $1 in Seg len f implies ex x being set
      st G[$1,x];
A11:  k = len f by A8,FINSEQ_1:def 3;
A12:  for l being Element of NAT st H[l] holds H[l+1]
      proof
        let l be Element of 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,COMPLFLD:8;
                end;
                suppose
                  p.0 = -1;
                  hence thesis by A31,COMPLFLD:8;
                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:          fl1p = cp(l+1) by A9,A11,A14,A35;
              then reconsider fl1p0 = fl1p.0 as Integer by A3,A41;
A43:          fl1p0 = 1 or fl1p0 = m1 by A3,A42,A41;
              thus p1.0 = 1 or p1.0 = -1
              proof
                per cases by A23;
                suppose
                  p.0 = 1;
                  hence thesis by A3,A42,A41,A40;
                end;
                suppose
                  p.0 = -1;
                  hence thesis by A40,A43;
                end;
              end;
              let j be Element of NAT;
              consider r be FinSequence of F_Complex such that
              len r = j+1 and
A44:          p1.j = Sum r and
A45:          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 fl1pj1i = fl1p.(j+1-'i) as Integer by A3,A42,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 A45
                  .= pi1 * fl1pj1i;
                hence thesis;
              end;
              hence thesis by A44,Th4;
            end;
          end;
        end;
      end;
      defpred C[Nat] means cp(k).$1 is integer;
A46:  0+1-'1 = 0 by NAT_D:34;
A47:  H[0] by FINSEQ_1:1;
      for l being Element of NAT holds H[l] from NAT_1:sch 1(A47,A12 );
      then
A48:  for l being Nat st l in Seg len f ex x being set st G[l,x];
      consider F being FinSequence such that
      dom F = Seg len f and
A49:  for i being Nat st i in Seg len f holds G[i,F.i] from FINSEQ_1:
      sch 1 (A48);
      consider g being FinSequence of cPRFC, p1 being Polynomial of F_Complex
      such that
A50:  g = f | Seg k & p1 = Product(g) and
      F.k = p1 and
A51:  p1.0 = 1 or p1.0 = -1 and
A52:  for j being Element of NAT holds p1.j is integer by A11,A49,FINSEQ_1:3;
A53:  p = p1 by A7,A11,A50,FINSEQ_3:49;
A54:  now
        let m be Nat;
        reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
        consider r be FinSequence of cFC such that
A55:    len r = m+1 and
A56:    unital_poly(F_Complex,k).m = Sum r and
A57:    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,A56,Th38;
          end;
          suppose
            m1 = k;
            hence Src is integer by A56,Th38,COMPLFLD:8;
          end;
          suppose
            m1 <> 0 & m1 <> k;
            hence Src is integer by A56,Th39,COMPLFLD:7;
          end;
        end;
        then reconsider Sr = Src as Integer;
A58:    (1,1)-cut r ^ (1+1,len r)-cut r = r by A55,GRAPH_2:9,NAT_1:11;
        set s = (1+1,len r)-cut r;
        reconsider Ssc = Sum s as Element of COMPLEX by COMPLFLD:def 1;
        assume
A59:    for n being Nat st n < m holds C[n];
        now
          let i be Element of NAT;
          assume
A60:      i in dom s;
          per cases;
          suppose
            len r < 2;
            then s = {} by GRAPH_2:def 1;
            hence s.i is integer;
          end;
          suppose
A61:        1+1 <= len r;
            then
A62:        len s +(1+1) = len r + 1 by GRAPH_2:def 1;
            per cases;
            suppose
              m = 0;
              hence s.i is integer by A55,A61;
            end;
            suppose
A63:          m > 0;
              i <> 0 by A60,FINSEQ_3:25;
              then reconsider cpkmi = cp(k).(m-'i) as Integer by A59,A63,
NAT_2:9;
              reconsider ppi = p.i as Integer by A52,A53;
              i <> 0 by A60,FINSEQ_3:25;
              then consider i1 being Nat such that
A64:          i = i1+1 by NAT_1:6;
A65:          i <= len s by A60,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 A62,FINSEQ_3:25;
              then
A66:          r.(1+i) = p.(1+i-'1) * cp(k).(m+1-'(1+i)) by A57
                .= 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 A65,A64,NAT_1:13;
              then s.i = r.(1+1+i1) by A61,A64,GRAPH_2:def 1
                .= r.(1+i) by A64;
              hence s.i is integer by A66;
            end;
          end;
        end;
        then reconsider Ss = Ssc as Integer by Th4;
A67:    1 <= len r by A55,NAT_1:11;
        then
A68:    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 A67,GRAPH_2:6;
        then Sum r = r1 + Sum s by A58,FVSUM_1:72;
        then r1c = Sr -Ss;
        then reconsider r1i = r1 as Integer;
A69:    r1i = p.(1-'1) * cp(k).(m+1-'1) by A57,A68
          .= p.0 * cp(k).m1 by A46,NAT_D:34;
        per cases by A7,A11,A50,A51,FINSEQ_3:49;
        suppose
          p.0 = 1;
          hence C[m] by A69;
        end;
        suppose
          p.0 = -1;
          then r1 = (-1_F_Complex) * cp(k).m1 by A69,COMPLFLD:2,8
            .= -1_F_Complex * cp(k).m1 by VECTSP_1:9
            .= - cp(k).m1 by VECTSP_1:def 8;
          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 by COMPLFLD:2;
          hence C[m];
        end;
      end;
A70:  for i being Nat holds C[i] from NAT_1:sch 4(A54);
      consider r be FinSequence of cFC such that
A71:  len r = 0+1 and
A72:  unital_poly(F_Complex,k).0 = Sum r and
A73:  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;
A74:  1 in dom r by A71,FINSEQ_3:25;
      then reconsider r1 = r.1 as Element of cFC by FINSEQ_2:11;
      r = <*r1*> by A71,FINSEQ_1:40;
      then
A75:  Sum r = r.1 by RLVECT_1:44
        .= p.0 * (cp(k).0) by A73,A46,A74;
      cp(k).0 = 1 or cp(k).0 = -1
      proof
        per cases by A7,A11,A50,A51,FINSEQ_3:49;
        suppose
          p.0 = 1;
          hence thesis by A1,A72,A75,Th38;
        end;
        suppose
          p.0 = -1;
          then -1_F_Complex = (-1_F_Complex) * cp(k).0 by A1,A72,A75,Th38
            .= -1_F_Complex * cp(k).0 by VECTSP_1:9
            .= - cp(k).0 by VECTSP_1:def 8;
          hence thesis by COMPLFLD:8,RLVECT_1:18;
        end;
      end;
      hence P[k] by A70;
    end;
  end;
  for d being non empty Element of NAT holds P[d] from CompIndNE(A2);
  hence thesis;
end;

theorem Th52: :: WEDDWITT
  for d being non empty 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 empty 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 empty 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 empty 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 empty 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 empty 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 set;
      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[Element of 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;
    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 set;
        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:1;
      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 set;
        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:1;
      set cb = (scb,1)-bag;
A41:  sb misses scb
      proof
        assume sb /\ scb <> {};
        then consider x being set 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 set;
    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:1;
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 set such that
A52:  x in t by XBOOLE_0:def 1;
      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 empty 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
empty 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 empty 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 set;
    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 empty 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 empty 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 empty 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 empty Element of NAT;
    assume i in Seg n;
    then ex d being non empty 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 empty 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 set 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 set;
    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:1;
  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 set 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 empty 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 empty 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[Element of 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 empty Element of NAT;
          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 empty 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 empty 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,POLYNOM5:def 4;
  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 empty 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 empty 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 empty 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 empty 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 empty 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 empty 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 by INT_1:25;
      then k div l = (j*m)*l/l by A9,INT_1:def 9;
      then k div l = j*m by A10,XCMPLX_1:89;
      hence thesis by INT_1:def 3;
    end;
    suppose
      l = 0;
      then k div l = 0 by INT_1:48;
      hence thesis by INT_2:12;
    end;
  end;
  hence thesis;
end;

theorem
  for n,q being non empty 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 empty 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 empty 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 empty 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 empty 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 abs(i) > q - 1
proof
  set MGFC = MultGroup F_Complex;
  set cMGFC = the carrier of MultGroup F_Complex;
  let n be non empty 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 set st x in rng p1 holds x in REAL
  proof
    let x be set;
    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 = |.qc - fs/.i.| by A7,A10,A11;
    hence thesis;
  end;
  then rng p1 c= REAL by TARSKI:def 3;
  then reconsider ps=p1 as non empty FinSequence of REAL by A6,FINSEQ_1:def 4;
  len fs = card S by UPROOTS:3;
  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 by XREAL_0:def 1;
  assume i = eval(cyclotomic_poly(n),qc);
  then abs(i) > x by A21,A12,A14,Th7;
  hence abs(i) > q - 1;
end;