uniroots.miz

begin



 Lm1: for k be Element of NAT holds k is non zero iff 1 <= k

 proof

 let k be Element of NAT ;

 hereby

 assume k is non zero;

 then ( 0 + 1) <= k by NAT_1: 13;

 hence 1 <= k;

 end;

 assume 1 <= k;

 hence thesis;

 end;

 scheme :: UNIROOTS:sch1

 CompIndNE { P[ non zero Nat] } :

for k be non zero Element of NAT holds P[k]

 provided

 A1: for k be non zero Element of NAT st for n be non zero Element of NAT st n < k holds P[n] holds P[k];

 let k be non zero Element of NAT ;

 defpred R[ Nat] means ex m be non zero Element of NAT st m = $1 & P[m];

 A2:

 now

 let k be Nat such that

 A3: k >= 1 and

 A4: for n be Nat st n >= 1 & n < k holds R[n];

 reconsider m = k as non zero Element of NAT by A3, ORDINAL1:def 12;

 now

 let n be non zero Element of NAT such that

 A5: n < m;

 n >= 1 by Lm1;

 then R[n] by A4, A5;

 hence P[n];

 end;

 then P[m] by A1;

 hence R[k];

 end;



 A6: for k be Nat st k >= 1 holds R[k] from NAT_1:sch 9( A2);

 k >= 1 by Lm1;

 then ex m be non zero Element of NAT st m = k & P[m] by A6;

 hence thesis;

 end;

 theorem :: UNIROOTS:1



 Th1: for f be 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 be FinSequence, n,i be Element of NAT st i <= n holds ((f | ( Seg n)) | ( Seg i)) = (f | ( Seg i)) by FINSEQ_1: 5, RELAT_1: 74;

 theorem :: UNIROOTS:2



 Th2: for f be FinSequence of F_Complex , g be FinSequence of REAL st ( len f) = ( len g) & for i be Element of NAT st i in ( dom f) holds |.(f /. i).| = (g . i) holds |.( Product f).| = ( Product g)

 proof

 defpred P[ Nat] means for f be FinSequence of F_Complex , g be FinSequence of REAL st ( len f) = ( len g) & (for i be Element of NAT st i in ( dom f) holds |.(f /. i).| = (g . i)) & $1 = ( len f) holds |.( Product f).| = ( Product g);

 set FC = F_Complex ;

 set cFC = the carrier of FC;



 A1: for i be Nat st P[i] holds P[(i + 1)]

 proof

 let i be 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 be Element of NAT st i in ( dom f) holds |.(f /. i).| = (g . i) and

 A5: (i + 1) = ( len f);

 consider g1 be FinSequence of REAL , r be Element of REAL such that

 A6: g = (g1 ^ <*r*>) by A3, A5, FINSEQ_2: 19;



 A7: ( len g) = (( len g1) + ( len <*r*>)) by A6, FINSEQ_1: 22

 .= (( len g1) + 1) by FINSEQ_1: 39;

 then

 A8: (g . ( len f)) = r by A3, A6, FINSEQ_1: 42;

 consider f1 be FinSequence of FC, c be 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 be 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 be Nat holds P[i] from NAT_1:sch 2( A18, A1);

 let f be FinSequence of F_Complex , g be FinSequence of REAL ;

 assume ( len f) = ( len g) & for i be Element of NAT st i in ( dom f) holds |.(f /. i).| = (g . i);

 hence thesis by A23;

 end;

 theorem :: UNIROOTS:3



 Th3: for s be non empty finite Subset of F_Complex , x be Element of F_Complex , r be FinSequence of REAL st ( len r) = ( card s) & for i be Element of NAT , c be 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 be Element of FC, r be FinSequence of REAL such that

 A1: ( len r) = ( card s) and

 A2: for i be Element of NAT , c be Element of FC st i in ( dom r) & c = (( canFS s) . i) holds (r . i) = |.(x - c).|;

 defpred P[ set, set] means ex c be Element of FC st c = (( canFS s) . $1) & $2 = ( eval ( <%( - c), ( 1_ F_Complex )%>,x));

 ( len ( canFS s)) = ( card s) by FINSEQ_1: 93;

 then

 A3: ( dom ( canFS s)) = ( Seg ( card s)) by FINSEQ_1:def 3;



 A4: for k be Nat st k in ( Seg ( card s)) holds ex y be Element of FC st P[k, y]

 proof

 let k be Nat such that

 A5: k in ( Seg ( card s));

 set c = (( canFS s) . k);

 c in s by A3, A5, FINSEQ_2: 11;

 then

 reconsider c as Element of FC;

 reconsider fi = ( eval ( <%( - c), ( 1_ F_Complex )%>,x)) as Element of FC;

 take fi, c;

 thus thesis;

 end;

 consider f be FinSequence of FC such that

 A6: ( dom f) = ( Seg ( card s)) and

 A7: for k be Nat st k in ( Seg ( card s)) holds P[k, (f /. k)] from RECDEF_1:sch 17( A4);

 A8:

 now

 let i be Element of NAT , c be Element of FC such that

 A9: i in ( dom f) and

 A10: c = (( canFS s) . i);

 ex c1 be 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 be 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 :: UNIROOTS:4



 Th4: for f be FinSequence of F_Complex st for i be 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 be Element of NAT st i in ( dom f) holds (f . i) is integer;

 defpred P[ Nat] means for f be FinSequence of FC st ( len f) = $1 & for i be Element of NAT st i in ( dom f) holds (f . i) is integer holds ( Sum f) is integer;



 A2: for n be Nat st P[n] holds P[(n + 1)]

 proof

 let n be Nat such that

 A3: P[n];

 let f be FinSequence of FC;

 assume that

 A4: ( len f) = (n + 1) and

 A5: for i be Element of NAT st i in ( dom f) holds (f . i) is integer;

 consider g be FinSequence of FC, c be 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 be Nat holds P[n] from NAT_1:sch 2( A12, A2);

 hence thesis by A1, A11;

 end;

 theorem :: UNIROOTS:5

 for x,y be Element of F_Complex , r1,r2 be Real st r1 = x & r2 = y holds (r1 * r2) = (x * y) & (r1 + r2) = (x + y);

 theorem :: UNIROOTS:6



 Th6: for q be Real st q > 0 holds for r be 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 :: UNIROOTS:7



 Th7: for ps be non empty FinSequence of REAL , x be Real st x >= 1 & for i be 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 be Element of NAT st j in ( dom ps) holds (ps . j) > x;

 consider ps1 be FinSequence, y be object such that

 A3: ps = (ps1 ^ <*y*>) by FINSEQ_1: 46;

 <*y*> is FinSequence of REAL by A3, FINSEQ_1: 36;

 then ( rng <*y*>) c= REAL by FINSEQ_1:def 4;

 then {y} c= REAL by FINSEQ_1: 38;

 then

 reconsider y2 = y as Element of REAL by ZFMISC_1: 31;

 defpred P[ Nat] means for f be FinSequence of REAL st ( len f) = $1 & for j be Element of NAT st j in ( dom f) holds (f . j) > x holds (( Product f) * y2) > x;



 A4: for k be Nat st P[k] holds P[(k + 1)]

 proof

 let k be Nat such that

 A5: P[k];

 let f be FinSequence of REAL such that

 A6: ( len f) = (k + 1) and

 A7: for j be Element of NAT st j in ( dom f) holds (f . j) > x;

 f <> {} by A6;

 then

 consider v be FinSequence, w be object such that

 A8: f = (v ^ <*w*>) by FINSEQ_1: 46;

 reconsider f1 = v, f2 = <*w*> as FinSequence of REAL by A8, FINSEQ_1: 36;

 ( rng f2) c= REAL ;

 then {w} c= REAL by FINSEQ_1: 38;

 then

 reconsider m = w as Element of REAL by ZFMISC_1: 31;

 (k + 1) = (( len f1) + ( len f2)) by A6, A8, FINSEQ_1: 22;

 then

 A9: (k + 1) = (( len f1) + 1) by FINSEQ_1: 39;

 then

 A10: (f . ( len f)) = m by A6, A8, FINSEQ_1: 42;

 ( len f) in ( Seg ( len f)) by A6, FINSEQ_1: 3;

 then

 A11: ( len f) in ( dom f) by FINSEQ_1:def 3;

 then m > 1 by A1, A7, A10, XXREAL_0: 2;

 then

 A12: (x * m) > x by A1, XREAL_1: 155;



 A13: for j be 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 be 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 be 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 be Nat holds P[k] from NAT_1:sch 2( A23, A4);

 then (( Product q) * y2) > x by A18, A21;

 hence thesis by A3, RVSUM_1: 96;

 end;

 theorem :: UNIROOTS:8



 Th8: for n be Element of NAT holds ( 1_ F_Complex ) = (( power F_Complex ) . (( 1_ F_Complex ),n))

 proof

 let n be Element of NAT ;

 ( 1_ F_Complex ) = [**1, 0 **] by COMPLFLD: 8;



 then (( power F_Complex ) . (( 1_ F_Complex ),n)) = [**(1 to_power n), 0 **] by HAHNBAN1: 29

 .= ( 1_ F_Complex ) by COMPLFLD: 8;

 hence thesis;

 end;

 theorem :: UNIROOTS:9



 Th9: for n,i be Nat holds ( cos (((2 * PI ) * i) / n)) = ( cos (((2 * PI ) * (i mod n)) / n)) & ( sin (((2 * PI ) * i) / n)) = ( sin (((2 * PI ) * (i mod n)) / n))

 proof

 let n,i be Nat;

 set j = (i div n);

 per cases ;

 suppose

 A1: n <> 0 ;

 then i = ((n * j) + (i mod n)) by NAT_D: 2;



 then

 A2: (((2 * PI ) * i) / n) = ((((2 * PI ) * (n * j)) + ((2 * PI ) * (i mod n))) / n)

 .= ((((2 * PI ) * (n * j)) / (n * 1)) + (((2 * PI ) * (i mod n)) / n)) by XCMPLX_1: 62

 .= (((((2 * PI ) / n) * (n * j)) / 1) + (((2 * PI ) * (i mod n)) / n)) by XCMPLX_1: 83

 .= ((((2 * PI ) * (1 / n)) * (n * j)) + (((2 * PI ) * (i mod n)) / n)) by XCMPLX_1: 99

 .= (((2 * PI ) * ((1 / n) * (j * n))) + (((2 * PI ) * (i mod n)) / n))

 .= (((2 * PI ) * (j * 1)) + (((2 * PI ) * (i mod n)) / n)) by A1, XCMPLX_1: 90

 .= (((2 * PI ) * j) + (((2 * PI ) * (i mod n)) / n));



 then

 A3: ( sin (((2 * PI ) * i) / n)) = ((( sin (((2 * PI ) * j) + 0 )) * ( cos (((2 * PI ) * (i mod n)) / n))) + (( cos (((2 * PI ) * j) + 0 )) * ( sin (((2 * PI ) * (i mod n)) / n)))) by SIN_COS: 75

 .= ((( sin . (((2 * PI ) * j) + 0 )) * ( cos (((2 * PI ) * (i mod n)) / n))) + (( cos (((2 * PI ) * j) + 0 )) * ( sin (((2 * PI ) * (i mod n)) / n)))) by SIN_COS:def 17

 .= ((( sin . (((2 * PI ) * j) + 0 )) * ( cos (((2 * PI ) * (i mod n)) / n))) + (( cos . (((2 * PI ) * j) + 0 )) * ( sin (((2 * PI ) * (i mod n)) / n)))) by SIN_COS:def 19

 .= ((( sin . 0 ) * ( cos (((2 * PI ) * (i mod n)) / n))) + (( cos . (((2 * PI ) * j) + 0 )) * ( sin (((2 * PI ) * (i mod n)) / n)))) by SIN_COS2: 10

 .= ((( sin . 0 ) * ( cos (((2 * PI ) * (i mod n)) / n))) + (( cos . 0 ) * ( sin (((2 * PI ) * (i mod n)) / n)))) by SIN_COS2: 11

 .= ( sin (((2 * PI ) * (i mod n)) / n)) by SIN_COS: 30;

 ( cos (((2 * PI ) * i) / n)) = ((( cos (((2 * PI ) * j) + 0 )) * ( cos (((2 * PI ) * (i mod n)) / n))) - (( sin (((2 * PI ) * j) + 0 )) * ( sin (((2 * PI ) * (i mod n)) / n)))) by A2, SIN_COS: 75

 .= ((( cos . (((2 * PI ) * j) + 0 )) * ( cos (((2 * PI ) * (i mod n)) / n))) - (( sin (((2 * PI ) * j) + 0 )) * ( sin (((2 * PI ) * (i mod n)) / n)))) by SIN_COS:def 19

 .= ((( cos . (((2 * PI ) * j) + 0 )) * ( cos (((2 * PI ) * (i mod n)) / n))) - (( sin . (((2 * PI ) * j) + 0 )) * ( sin (((2 * PI ) * (i mod n)) / n)))) by SIN_COS:def 17

 .= ((( cos . 0 ) * ( cos (((2 * PI ) * (i mod n)) / n))) - (( sin . (((2 * PI ) * j) + 0 )) * ( sin (((2 * PI ) * (i mod n)) / n)))) by SIN_COS2: 11

 .= ((( cos . 0 ) * ( cos (((2 * PI ) * (i mod n)) / n))) - (( sin . 0 ) * ( sin (((2 * PI ) * (i mod n)) / n)))) by SIN_COS2: 10

 .= ( cos (((2 * PI ) * (i mod n)) / n)) by SIN_COS: 30;

 hence thesis by A3;

 end;

 suppose

 A4: n = 0 ;

 then (((2 * PI ) * i) / n) = 0 by XCMPLX_1: 49;

 hence thesis by A4, XCMPLX_1: 49;

 end;

 end;

 theorem :: UNIROOTS:10



 Th10: for n,i be Nat holds [**( cos (((2 * PI ) * i) / n)), ( sin (((2 * PI ) * i) / n))**] = [**( cos (((2 * PI ) * (i mod n)) / n)), ( sin (((2 * PI ) * (i mod n)) / n))**]

 proof

 let n,i be Nat;

 [**( cos (((2 * PI ) * i) / n)), ( sin (((2 * PI ) * i) / n))**] = [**( cos (((2 * PI ) * (i mod n)) / n)), ( sin (((2 * PI ) * i) / n))**] by Th9

 .= [**( cos (((2 * PI ) * (i mod n)) / n)), ( sin (((2 * PI ) * (i mod n)) / n))**] by Th9;

 hence thesis;

 end;

 theorem :: UNIROOTS:11



 Th11: for n,i,j be 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 :: UNIROOTS:12



 Th12: for L be unital associative non empty multMagma, x be Element of L, n,m be Nat holds (( power L) . (x,(n * m))) = (( power L) . ((( power L) . (x,n)),m))

 proof

 let L be unital associative non empty multMagma, x be Element of L, n be Nat;

 defpred P[ Nat] means (( power L) . (x,(n * $1))) = (( power L) . ((( power L) . (x,n)),$1));

 set pL = ( power L);

 reconsider nn = n as Element of NAT by ORDINAL1:def 12;



 A1: for m be Nat st P[m] holds P[(m + 1)]

 proof

 let m be Nat such that

 A2: P[m];

 reconsider nm = (n * m), mm = m as Element of NAT by ORDINAL1:def 12;

 (pL . (x,(n * (m + 1)))) = (pL . (x,((n * m) + (n * 1))))

 .= ((pL . (x,nm)) * (pL . (x,nn))) by POLYNOM2: 1

 .= (pL . ((pL . (x,nn)),(mm + 1))) by A2, GROUP_1:def 7;

 hence thesis;

 end;

 (pL . (x,(n * 0 qua Nat))) = ( 1_ L) by GROUP_1:def 7

 .= (pL . ((pL . (x,nn)), 0 )) by GROUP_1:def 7;

 then

 A3: P[ 0 ];

 thus for m be Nat holds P[m] from NAT_1:sch 2( A3, A1);

 end;

 theorem :: UNIROOTS:13



 Th13: for n be Element of NAT , x be Element of F_Complex st x is Integer holds (( power F_Complex ) . (x,n)) is Integer

 proof

 let n be Element of NAT , x be Element of F_Complex such that

 A1: x is Integer;

 defpred P[ Nat] means (( power F_Complex ) . (x,$1)) is Integer;

 A2:

 now

 reconsider i1 = x as Integer by A1;

 let k be Nat;

 reconsider kk = k as Element of NAT by ORDINAL1:def 12;

 assume P[k];

 then

 reconsider i2 = (( power F_Complex ) . (x,k)) as Integer;

 ((( power F_Complex ) . (x,kk)) * x) = (i1 * i2);

 hence P[(k + 1)] by GROUP_1:def 7;

 end;



 A3: P[ 0 ] by COMPLFLD: 8, GROUP_1:def 7;

 for k be Nat holds P[k] from NAT_1:sch 2( A3, A2);

 hence thesis;

 end;

 theorem :: UNIROOTS:14



 Th14: for F be FinSequence of F_Complex st for i be Element of NAT st i in ( dom F) holds (F . i) is Integer holds ( Sum F) is Integer

 proof

 defpred P[ Nat] means for F be FinSequence of F_Complex st ( len F) = $1 & for i be 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 be Element of NAT st i in ( dom G) holds (G . i) is Integer;



 A2: for k be Nat st P[k] holds P[(k + 1)]

 proof

 let k be Nat such that

 A3: P[k];

 let F be FinSequence of F_Complex such that

 A4: ( len F) = (k + 1) and

 A5: for i be Element of NAT st i in ( dom F) holds (F . i) is Integer;

 F <> {} by A4;

 then

 consider G be FinSequence, x be object such that

 A6: F = (G ^ <*x*>) by FINSEQ_1: 46;

 ( len F) in ( Seg ( len F)) by A4, FINSEQ_1: 3;

 then

 A7: ( len F) in ( dom F) by FINSEQ_1:def 3;

 reconsider f2 = <*x*> as FinSequence of F_Complex by A6, FINSEQ_1: 36;

 reconsider f1 = G as FinSequence of F_Complex by A6, FINSEQ_1: 36;

 ( rng f2) c= the carrier of F_Complex by FINSEQ_1:def 4;

 then {x} c= the carrier of F_Complex by FINSEQ_1: 38;

 then

 reconsider m = x as Element of F_Complex by ZFMISC_1: 31;

 (k + 1) = (( len f1) + ( len f2)) by A4, A6, FINSEQ_1: 22;

 then

 A8: (k + 1) = (( len f1) + 1) by FINSEQ_1: 39;

 then (F . ( len F)) = m by A4, A6, FINSEQ_1: 42;

 then

 reconsider i2 = m as Integer by A5, A7;

 for j be 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 be 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 be Nat holds P[k] from NAT_1:sch 2( A11, A2);

 ( len G) = ( len G);

 hence thesis by A1, A13;

 end;



 Lm3: Z_3 is finite by MOD_2:def 20;

 registration

 cluster finite for Field;

 existence by Lm3, MOD_2: 27;

 cluster finite for Skew-Field;

 existence by Lm3, MOD_2: 27;

 end

 begin

 definition

 let R be Skew-Field;

 :: UNIROOTS:def1

 func MultGroup R -> strict Group means

 : Def1: the carrier of it = ( NonZero R) & the multF of it = (the multF of R || the carrier of it );

 existence

 proof

 set ccs = ( NonZero R);

 set cR = the carrier of R;

 reconsider ccs as non empty set;

 set mcs = (the multF of R || ccs);

 [:ccs, ccs:] c= [:cR, cR:]

 proof

 let x be object;

 assume x in [:ccs, ccs:];

 then ex a,b be object st a in ccs & b in ccs & x = [a, b] by ZFMISC_1:def 2;

 hence thesis by ZFMISC_1:def 2;

 end;

 then

 reconsider mcs as Function of [:ccs, ccs:], cR by FUNCT_2: 32;

 ( rng mcs) c= ccs

 proof

 let y be object;

 assume y in ( rng mcs);

 then

 consider x be object such that

 A1: x in ( dom mcs) and

 A2: y = (mcs . x) by FUNCT_1:def 3;



 A3: ( dom mcs) = [:ccs, ccs:] by FUNCT_2:def 1;

 then

 consider a,b be object such that

 A4: a in ccs and

 A5: b in ccs and

 A6: x = [a, b] by A1, ZFMISC_1:def 2;

 reconsider a, b as Element of cR by A4, A5;

 not b in {( 0. R)} by A5, XBOOLE_0:def 5;

 then

 A7: b <> ( 0. R) by TARSKI:def 1;

 not a in {( 0. R)} by A4, XBOOLE_0:def 5;

 then a <> ( 0. R) by TARSKI:def 1;

 then (a * b) <> ( 0. R) by A7, VECTSP_2: 12;

 then

 A8: not (a * b) in {( 0. R)} by TARSKI:def 1;

 (mcs . x) = (a * b) by A1, A3, A6, FUNCT_1: 49;

 hence thesis by A2, A8, XBOOLE_0:def 5;

 end;

 then

 reconsider mcs as BinOp of ccs by FUNCT_2: 6;

 reconsider cs = multMagma (# ccs, mcs #) as non empty multMagma;

 set ccs1 = the carrier of cs;

 A9:

 now

 let a,b be Element of cR, c,d be Element of ccs1 such that

 A10: a = c & b = d;

 [c, d] in [:ccs, ccs:] by ZFMISC_1:def 2;

 hence (a * b) = (c * d) by A10, FUNCT_1: 49;

 end;



 A11: not ( 1_ R) in {( 0. R)} by TARSKI:def 1;



 A12: cs is Group-like

 proof

 reconsider e = ( 1_ R) as Element of ccs1 by A11, XBOOLE_0:def 5;

 take e;

 let h be Element of ccs1;

 h in ccs;

 then

 reconsider h9 = h as Scalar of R;



 thus (h * e) = (h9 * ( 1_ R)) by A9

 .= h;



 thus (e * h) = (( 1_ R) * h9) by A9

 .= h;

 not h in {( 0. R)} by XBOOLE_0:def 5;

 then

 A13: h <> ( 0. R) by TARSKI:def 1;

 then (h9 " ) <> ( 0. R) by VECTSP_2: 13;

 then not (h9 " ) in {( 0. R)} by TARSKI:def 1;

 then

 reconsider g = (h9 " ) as Element of ccs1 by XBOOLE_0:def 5;

 take g;



 thus (h * g) = (h9 * (h9 " )) by A9

 .= e by A13, VECTSP_2: 9;



 thus (g * h) = ((h9 " ) * h9) by A9

 .= e by A13, VECTSP_2: 9;

 end;

 cs is associative

 proof

 let x,y,z be Element of ccs1;



 A14: z in ccs1;

 x in ccs1 & y in ccs1;

 then

 reconsider x9 = x, y9 = y, z9 = z as Element of cR by A14;



 A15: (y9 * z9) = (y * z) by A9;

 (x9 * y9) = (x * y) by A9;



 hence ((x * y) * z) = ((x9 * y9) * z9) by A9

 .= (x9 * (y9 * z9)) by GROUP_1:def 3

 .= (x * (y * z)) by A9, A15;

 end;

 hence thesis by A12;

 end;

 uniqueness ;

 end

 theorem :: UNIROOTS:15

 for R be Skew-Field holds the carrier of R = (the carrier of ( MultGroup R) \/ {( 0. R)})

 proof

 let R be Skew-Field;

 ( NonZero R) = the carrier of ( MultGroup R) by Def1;

 hence thesis by XBOOLE_1: 45;

 end;

 theorem :: UNIROOTS:16



 Th16: for R be Skew-Field, a,b be Element of R, c,d be 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 :: UNIROOTS:17



 Th17: for R be Skew-Field holds ( 1_ R) = ( 1_ ( MultGroup R))

 proof

 let R be Skew-Field;



 A1: the carrier of ( MultGroup R) = ( NonZero R) by Def1;

 not ( 1_ R) in {( 0. R)} by TARSKI:def 1;

 then

 reconsider uR = ( 1_ R) as Element of ( MultGroup R) by A1, XBOOLE_0:def 5;

 now

 let h be Element of ( MultGroup R);

 reconsider g = h as Element of R by A1, XBOOLE_0:def 5;

 (g * ( 1_ R)) = g;

 hence (h * uR) = h by Th16;

 (( 1_ R) * g) = g;

 hence (uR * h) = h by Th16;

 end;

 hence thesis by GROUP_1:def 4;

 end;

 registration

 let R be finite Skew-Field;

 cluster ( MultGroup R) -> finite;

 correctness

 proof

 the carrier of ( MultGroup R) = ( NonZero R) by Def1;

 hence thesis;

 end;

 end

 theorem :: UNIROOTS:18

 for R be 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 :: UNIROOTS:19



 Th19: for R be Skew-Field, s be 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 :: UNIROOTS:20

 for R be Skew-Field holds the carrier of ( MultGroup R) c= the carrier of R

 proof

 let R be Skew-Field, s be object;

 assume s in the carrier of ( MultGroup R);

 then s in ( NonZero R) by Def1;

 hence thesis;

 end;

 begin

 definition

 let n be non zero Element of NAT ;

 :: UNIROOTS:def2

 func n -roots_of_1 -> Subset of F_Complex equals { x where x be Element of F_Complex : x is CRoot of n, ( 1_ F_Complex ) };

 coherence

 proof

 set H = { x where x be Element of F_Complex : x is CRoot of n, ( 1_ F_Complex ) };

 for x be object st x in H holds x in the carrier of F_Complex

 proof

 let x be object;

 assume x in H;

 then ex y be 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 :: UNIROOTS:21



 Th21: for n be non zero Element of NAT , x be Element of F_Complex holds x in (n -roots_of_1 ) iff x is CRoot of n, ( 1_ F_Complex )

 proof

 let n be non zero Element of NAT , x be Element of F_Complex ;

 hereby

 assume x in (n -roots_of_1 );

 then ex y be 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 :: UNIROOTS:22



 Th22: for n be non zero Element of NAT holds ( 1_ F_Complex ) in (n -roots_of_1 )

 proof

 let n be non zero Element of NAT ;

 ( 1_ F_Complex ) = (( power F_Complex ) . (( 1_ F_Complex ),n)) by Th8;

 then ( 1_ F_Complex ) is CRoot of n, ( 1_ F_Complex ) by COMPLFLD:def 2;

 hence thesis;

 end;

 theorem :: UNIROOTS:23



 Th23: for n be non zero Element of NAT , x be Element of F_Complex st x in (n -roots_of_1 ) holds |.x.| = 1

 proof

 let n be non zero Element of NAT , x be Element of F_Complex such that

 A1: x in (n -roots_of_1 );

 A2:

 now

 assume x = ( 0. F_Complex );

 then (( power F_Complex ) . (x,n)) <> ( 1_ F_Complex ) by VECTSP_1: 36;

 then not x is CRoot of n, ( 1_ F_Complex ) by COMPLFLD:def 2;

 hence contradiction by A1, Th21;

 end;

 then

 A3: |.x.| > 0 by COMPLFLD: 59;

 x is CRoot of n, ( 1_ F_Complex ) by A1, Th21;

 then ( power (x,n)) = ( 1_ F_Complex ) by COMPLFLD:def 2;

 then

 A4: 1 = ( |.x.| to_power n) by A2, COMPLFLD: 60, POLYNOM5: 7;

 assume

 A5: |.x.| <> 1;

 per cases by A5, XXREAL_0: 1;

 suppose

 A6: |.x.| < 1;

 reconsider n9 = n as Rational;

 ( |.x.| #Q n9) < 1 by A3, A6, PREPOWER: 65;

 hence contradiction by A4, A3, PREPOWER: 49;

 end;

 suppose |.x.| > 1;

 hence contradiction by A4, POWER: 35;

 end;

 end;

 theorem :: UNIROOTS:24



 Th24: for n be non zero Element of NAT holds for x be Element of F_Complex holds x in (n -roots_of_1 ) iff ex k be Element of NAT st x = [**( cos (((2 * PI ) * k) / n)), ( sin (((2 * PI ) * k) / n))**]

 proof

 let n be non zero Element of NAT , x be Element of F_Complex ;

 hereby

 assume

 A1: x in (n -roots_of_1 );

 A2:

 now

 assume x = ( 0. F_Complex );

 then (( power F_Complex ) . (x,n)) <> ( 1_ F_Complex ) by VECTSP_1: 36;

 then not x is CRoot of n, ( 1_ F_Complex ) by COMPLFLD:def 2;

 hence contradiction by A1, Th21;

 end;

 then 0 <= ( Arg x) & ( Arg x) < (2 * PI ) by COMPLFLD: 7, COMPTRIG:def 1;

 then

 A3: ( 0 + ( - 1)) <= (((n * ( Arg x)) / (2 * PI )) + ( - 1)) by XREAL_1: 7;

 x is CRoot of n, ( 1_ F_Complex ) by A1, Th21;

 then ( power (x,n)) = ( 1_ F_Complex ) by COMPLFLD:def 2;

 then

 A4: 1 = ( |.x.| to_power n) by A2, COMPLFLD: 60, POLYNOM5: 7;

 A5:

 now



 A6: |.x.| > 0 by A2, COMPLFLD: 59;

 assume

 A7: |.x.| <> 1;

 per cases by A7, XXREAL_0: 1;

 suppose

 A8: |.x.| < 1;

 reconsider n9 = n as Rational;

 ( |.x.| #Q n9) < 1 by A6, A8, PREPOWER: 65;

 hence contradiction by A4, A6, PREPOWER: 49;

 end;

 suppose |.x.| > 1;

 hence contradiction by A4, POWER: 35;

 end;

 end;

 set m2 = [\((n * ( Arg x)) / (2 * PI ))/];

 reconsider z = x as Element of COMPLEX by XCMPLX_0:def 2;

 consider r be Real such that

 A9: r = (((2 * PI ) * ( - [\((n * ( Arg x)) / (2 * PI ))/])) + (n * ( Arg x))) and

 A10: 0 <= r & r < (2 * PI ) by COMPLEX2: 1, COMPTRIG: 5;

 (((n * ( Arg x)) / (2 * PI )) - 1) < m2 by INT_1:def 6;

 then not m2 <= ( - 1) by A3, XXREAL_0: 2;

 then (( - 1) + 1) <= m2 by INT_1: 7;

 then

 reconsider m = [\((n * ( Arg x)) / (2 * PI ))/] as Element of NAT by INT_1: 3;



 A11: ( cos (n * ( Arg x))) = ( cos . (((2 * PI ) * m) + r)) by A9, SIN_COS:def 19

 .= ( cos . r) by SIN_COS2: 11

 .= ( cos r) by SIN_COS:def 19;



 A12: ( sin (n * ( Arg x))) = ( sin . (((2 * PI ) * m) + r)) by A9, SIN_COS:def 17

 .= ( sin . r) by SIN_COS2: 10

 .= ( sin r) by SIN_COS:def 17;

 x is CRoot of n, ( 1_ F_Complex ) by A1, Th21;

 then (( power F_Complex ) . (x,n)) = [**1, 0 **] by COMPLFLD: 8, COMPLFLD:def 2;

 then

 A13: (z |^ n) = ((( |.z.| |^ n) * ( cos (n * ( Arg z)))) + ((( |.z.| |^ n) * ( sin (n * ( Arg z)))) * )) & (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 be 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 be 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))) * )) by A15, COMPLFLD: 8, COMPLFLD: 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 :: UNIROOTS:25



 Th25: for n be non zero Element of NAT holds for x,y be Element of COMPLEX st x in (n -roots_of_1 ) & y in (n -roots_of_1 ) holds (x * y) in (n -roots_of_1 )

 proof

 let n be non zero Element of NAT ;

 let x,y be Element of COMPLEX such that

 A1: x in (n -roots_of_1 ) and

 A2: y in (n -roots_of_1 );

 reconsider a = x as Element of F_Complex by COMPLFLD:def 1;

 consider i be 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 be 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 :: UNIROOTS:26



 Th26: for n be non zero Element of NAT holds (n -roots_of_1 ) = { [**( cos (((2 * PI ) * k) / n)), ( sin (((2 * PI ) * k) / n))**] where k be Element of NAT : k < n }

 proof

 let n be non zero Element of NAT ;

 set X = { [**( cos (((2 * PI ) * k) / n)), ( sin (((2 * PI ) * k) / n))**] where k be Element of NAT : k < n };

 now

 let x be object;

 hereby

 assume

 A1: x in (n -roots_of_1 );

 then

 reconsider a = x as Element of F_Complex ;

 consider k be 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 be Element of NAT st x = [**( cos (((2 * PI ) * k) / n)), ( sin (((2 * PI ) * k) / n))**] & k < n;

 hence x in (n -roots_of_1 ) by Th24;

 end;

 hence thesis by TARSKI: 2;

 end;

 theorem :: UNIROOTS:27



 Th27: for n be non zero Element of NAT holds ( card (n -roots_of_1 )) = n

 proof

 let n be non zero Element of NAT ;

 set X = { [**( cos (((2 * PI ) * k) / n)), ( sin (((2 * PI ) * k) / n))**] where k be Element of NAT : k < n };

 defpred P[ object, object] means ex j be 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 be object st x in ( Seg n) holds ex y be object st y in Y & P[x, y]

 proof

 let x be object such that

 A3: x in ( Seg n);

 reconsider a = x as Element of NAT by A3;

 a <= n by A3, FINSEQ_1: 1;

 then a < (n + 1) by NAT_1: 13;

 then

 A4: (a - 1) < ((n + 1) - 1) by XREAL_1: 14;

 consider b be 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 be Function of ( Seg n), Y such that

 A6: for x be object st x in ( Seg n) holds P[x, (F . x)] from FUNCT_2:sch 1( A2);

 for c be object st c in X holds ex x be object st x in ( Seg n) & c = (F . x)

 proof

 let c be object;

 assume c in X;

 then

 consider k be 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 be 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 be object st x1 in ( dom F) & x2 in ( dom F) & (F . x1) = (F . x2) holds x1 = x2

 proof

 let x1,x2 be object such that

 A13: x1 in ( dom F) and

 A14: x2 in ( dom F) and

 A15: (F . x1) = (F . x2);



 A16: x1 in ( Seg n) by A13, FUNCT_2:def 1;

 then

 consider j be 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 be 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, XCMPLX_1: 87;

 then j = ((k -' 1) + 1) by A19, XREAL_1: 235;

 hence thesis by A17, A22, A24, XREAL_1: 235;

 end;

 then F is one-to-one by FUNCT_1:def 4;

 then (( Seg n),(F .: ( Seg n))) are_equipotent by A12, CARD_1: 33;

 then (( Seg n),( rng F)) are_equipotent by A12, RELAT_1: 113;

 then ( card ( Seg n)) = ( card X) by A11, CARD_1: 5;

 hence thesis by A1, FINSEQ_1: 57;

 end;

 registration

 let n be non zero Element of NAT ;

 cluster (n -roots_of_1 ) -> non empty;

 correctness by Th22;

 cluster (n -roots_of_1 ) -> finite;

 correctness

 proof

 ( card (n -roots_of_1 )) = n by Th27;

 hence thesis;

 end;

 end

 theorem :: UNIROOTS:28



 Th28: for n,ni be non zero Element of NAT st ni divides n holds (ni -roots_of_1 ) c= (n -roots_of_1 )

 proof

 let n,ni be non zero Element of NAT ;

 assume ni divides n;

 then

 consider k be Nat such that

 A1: n = (ni * k) by NAT_D:def 3;

 reconsider k as Element of NAT by ORDINAL1:def 12;

 for x be object st x in (ni -roots_of_1 ) holds x in (n -roots_of_1 )

 proof

 let x be object such that

 A2: x in (ni -roots_of_1 );

 reconsider y = x as Element of F_Complex by A2;

 y is CRoot of ni, ( 1_ F_Complex ) by A2, Th21;

 then ( 1_ F_Complex ) = (( power F_Complex ) . (y,ni)) by COMPLFLD:def 2;

 then ( 1_ F_Complex ) = (( power F_Complex ) . ((( power F_Complex ) . (y,ni)),k)) by Th8;

 then ( 1_ F_Complex ) = (( power F_Complex ) . (y,n)) by A1, Th12;

 then y is CRoot of n, ( 1_ F_Complex ) by COMPLFLD:def 2;

 hence thesis;

 end;

 hence thesis;

 end;

 theorem :: UNIROOTS:29



 Th29: for R be Skew-Field, x be Element of ( MultGroup R), y be Element of R st y = x holds for k be Nat holds (( power ( MultGroup R)) . (x,k)) = (( power R) . (y,k))

 proof

 let R be Skew-Field, x be Element of ( MultGroup R), y be Element of R such that

 A1: y = x;

 defpred P[ Nat] means (( power ( MultGroup R)) . (x,$1)) = (( power R) . (y,$1));



 A2: for k be Nat st P[k] holds P[(k + 1)]

 proof

 let k be Nat such that

 A3: P[k];

 reconsider kk = k as Element of NAT by ORDINAL1:def 12;



 thus (( power ( MultGroup R)) . (x,(k + 1))) = ((( power ( MultGroup R)) . (x,kk)) * x) by GROUP_1:def 7

 .= ((( power R) . (y,kk)) * y) by A1, A3, Th16

 .= (( power R) . (y,(k + 1))) by GROUP_1:def 7;

 end;

 (( power ( MultGroup R)) . (x, 0 )) = ( 1_ ( MultGroup R)) & (( power R) . (y, 0 )) = ( 1_ R) by GROUP_1:def 7;

 then

 A4: P[ 0 ] by Th17;

 thus for k be Nat holds P[k] from NAT_1:sch 2( A4, A2);

 end;

 theorem :: UNIROOTS:30



 Th30: for n be non zero Element of NAT , x be Element of ( MultGroup F_Complex ) st x in (n -roots_of_1 ) holds not x is being_of_order_0

 proof

 set MGFC = ( MultGroup F_Complex );

 set cMGFC = the carrier of ( MultGroup F_Complex );

 set FC = F_Complex ;

 let n be non zero Element of NAT , x be Element of cMGFC;

 assume x in (n -roots_of_1 );

 then

 consider c be Element of FC such that

 A1: c = x and

 A2: c is CRoot of n, ( 1_ FC);



 A3: ( 1_ MGFC) = ( 1_ FC) by Th17;

 (( power FC) . (c,n)) = ( 1_ FC) by A2, COMPLFLD:def 2;

 then (x |^ n) = ( 1_ MGFC) by A1, A3, Th29;

 hence thesis;

 end;

 theorem :: UNIROOTS:31



 Th31: for n be non zero Element of NAT , k be Element of NAT , x be Element of ( MultGroup F_Complex ) st x = [**( cos (((2 * PI ) * k) / n)), ( sin (((2 * PI ) * k) / n))**] holds ( ord x) = (n div (k gcd n))

 proof

 let n be non zero Element of NAT , k be Element of NAT ;

 reconsider kgn = (k gcd n) as Element of NAT ;



 A1: (k gcd n) divides n by INT_2: 21;

 then

 consider vn be Nat such that

 A2: n = (kgn * vn) by NAT_D:def 3;

 (k gcd n) divides k by INT_2: 21;

 then

 consider i be 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: not x is 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, NAT_D: 7;

 end;

 reconsider y = x as Element of F_Complex by Th19;

 reconsider vn as Element of NAT by ORDINAL1:def 12;



 A9: n = ((kgn * vn) + 0 ) by A2;

 then

 A10: (n div kgn) = vn by A6, NAT_D:def 1;



 A11: for m be 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 be Nat such that

 A16: (k * m) = (n * j) by NAT_D:def 3;

 consider a,b be Integer such that

 A17: k = (kgn * a) and

 A18: n = (kgn * b) and

 A19: (a,b) are_coprime by INT_2: 23;

 0 <= a by A6, A17;

 then

 reconsider ai = a as Element of NAT by INT_1: 3;

 0 <= b by A18;

 then

 reconsider bi = b as Element of NAT by INT_1: 3;

 ((m * a) * kgn) = (j * (b * kgn)) by A17, A18, A16;

 then (m * a) = (((j * b) * kgn) / kgn) by A6, XCMPLX_1: 89;

 then (m * a) = (j * b) by A6, XCMPLX_1: 89;

 then

 A20: bi divides (m * ai) by NAT_D:def 3;

 m < bi by A6, A10, A14, A18, NAT_D: 18;

 hence contradiction by A13, A19, A20, INT_2: 25, NAT_D: 7;

 end;



 A21: ((((2 * PI ) * k) / n) * m) = (((2 * PI ) * k) / (n / m)) by XCMPLX_1: 82

 .= ((((2 * PI ) * k) * m) / n) by XCMPLX_1: 77;

 ((2 * PI ) * ((k * m) mod n)) < ((2 * PI ) * n) by COMPTRIG: 5, NAT_D: 1, XREAL_1: 68;

 then (((2 * PI ) * ((k * m) mod n)) / n) < (((2 * PI ) * n) / n) by XREAL_1: 74;

 then

 A22: (((2 * PI ) * ((k * m) mod n)) / n) < (2 * PI ) by XCMPLX_1: 89;



 A23: ( 1_ ( MultGroup F_Complex )) = [**1, 0 **] by Th17, COMPLFLD: 8;

 (x |^ m) = (( power F_Complex ) . (y,m)) by Th29

 .= (y |^ m) by COMPLFLD: 74

 .= [**( cos (((2 * PI ) * (k * m)) / n)), ( sin ((((2 * PI ) * k) * m) / n))**] by A4, A21, COMPTRIG: 53

 .= [**( cos (((2 * PI ) * ((k * m) mod n)) / n)), ( sin (((2 * PI ) * ((k * m) mod n)) / n))**] by Th10;

 then ( cos (((2 * PI ) * ((k * m) mod n)) / n)) = 1 by A12, A23, COMPLEX1: 77;

 hence contradiction by A15, A22, COMPTRIG: 5, COMPTRIG: 61;

 end;

 hence thesis by A6, A9, NAT_D:def 1;

 end;

 reconsider i as Element of NAT by ORDINAL1:def 12;



 A24: ((((2 * PI ) * k) / n) * vn) = (((2 * PI ) * (kgn * i)) / (n / vn)) by A3, XCMPLX_1: 82

 .= ((((2 * PI ) * (kgn * i)) * vn) / n) by XCMPLX_1: 77

 .= ((((2 * PI ) * i) * n) / n) by A2

 .= (((2 * PI ) * i) + 0 ) by XCMPLX_1: 89;

 (x |^ (n div kgn)) = (( power F_Complex ) . (y,vn)) by A10, Th29

 .= (y |^ vn) by COMPLFLD: 74

 .= [**( cos ((((2 * PI ) * k) / n) * vn)), ( sin ((((2 * PI ) * k) / n) * vn))**] by A4, COMPTRIG: 53

 .= [**( cos 0 ), ( sin (((2 * PI ) * i) + 0 ))**] by A24, COMPLEX2: 9

 .= (1 + ( 0 * )) 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 :: UNIROOTS:32



 Th32: for n be non zero Element of NAT holds (n -roots_of_1 ) c= the carrier of ( MultGroup F_Complex )

 proof

 let n be non zero Element of NAT ;

 set cMGFC = the carrier of ( MultGroup F_Complex );

 set FC = F_Complex ;

 let a be object;

 assume a in (n -roots_of_1 );

 then

 consider x be 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 :: UNIROOTS:33

 for n be non zero Element of NAT holds ex x be Element of ( MultGroup F_Complex ) st ( ord x) = n

 proof

 let n be non zero Element of NAT ;

 set x = [**( cos (((2 * PI ) * 1) / n)), ( sin (((2 * PI ) * 1) / n))**];

 (n -roots_of_1 ) c= the carrier of ( MultGroup F_Complex ) & x in (n -roots_of_1 ) by Th24, Th32;

 then

 reconsider y = x as Element of ( MultGroup F_Complex );

 ( ord y) = (n div (1 gcd n)) & (1 gcd n) = 1 by Th31, WSIERP_1: 8;

 hence thesis by NAT_2: 4;

 end;

 theorem :: UNIROOTS:34



 Th34: for n be non zero Element of NAT , x be Element of ( MultGroup F_Complex ) holds ( ord x) divides n iff x in (n -roots_of_1 )

 proof

 set FC = F_Complex ;

 let n be non zero Element of NAT , x be Element of ( MultGroup F_Complex );

 reconsider c = x as Element of FC by Th19;

 set MGFC = ( MultGroup F_Complex );



 A1: ( 1_ MGFC) = ( 1_ FC) by Th17;

 hereby

 assume ( ord x) divides n;

 then

 consider k be 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 be 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 :: UNIROOTS:35



 Th35: for n be non zero Element of NAT holds (n -roots_of_1 ) = { x where x be Element of ( MultGroup F_Complex ) : ( ord x) divides n }

 proof

 set cMGFC = the carrier of ( MultGroup F_Complex );

 set MGFC = ( MultGroup F_Complex );

 let n be non zero Element of NAT ;

 set R = { a where a be Element of F_Complex : a is CRoot of n, ( 1_ F_Complex ) };

 set S = { x where x be Element of ( MultGroup F_Complex ) : ( ord x) divides n };



 A1: (n -roots_of_1 ) = R;

 then

 A2: R c= cMGFC by Th32;

 now

 let a be object;

 hereby

 assume

 A3: a in R;

 then

 reconsider x = a as Element of MGFC by A2;

 ( ord x) divides n by A1, A3, Th34;

 hence a in S;

 end;

 assume a in S;

 then ex x be Element of MGFC st a = x & ( ord x) divides n;

 hence a in R by A1, Th34;

 end;

 hence thesis by TARSKI: 2;

 end;

 theorem :: UNIROOTS:36



 Th36: for n be non zero Element of NAT , x be set holds x in (n -roots_of_1 ) iff ex y be Element of ( MultGroup F_Complex ) st x = y & ( ord y) divides n

 proof

 set MGFC = ( MultGroup F_Complex );

 set cMGFC = the carrier of ( MultGroup F_Complex );

 let n be non zero Element of NAT , x be set;



 A1: (n -roots_of_1 ) c= cMGFC by Th32;

 hereby

 assume

 A2: x in (n -roots_of_1 );

 then

 reconsider a = x as Element of MGFC by A1;

 ( ord a) divides n by A2, Th34;

 hence ex y be Element of ( MultGroup F_Complex ) st x = y & ( ord y) divides n;

 end;

 thus thesis by Th34;

 end;

 definition

 let n be non zero Element of NAT ;

 :: UNIROOTS:def3

 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 be object st x in X holds (mru . x) in (n -roots_of_1 )

 proof

 let x be object such that

 A5: x in X;

 consider a,b be object such that

 A6: [a, b] = x by A5, RELAT_1:def 1;



 A7: b in (n -roots_of_1 ) by A5, A6, ZFMISC_1: 87;



 A8: a in (n -roots_of_1 ) by A5, A6, ZFMISC_1: 87;

 reconsider b as Element of COMPLEX by A7, COMPLFLD:def 1;

 reconsider a as Element of COMPLEX by A8, COMPLFLD:def 1;

 ( multcomplex . (a,b)) = (a * b) & (mru . [a, b]) = ( multcomplex . [a, b]) by A2, A4, A5, A6, BINOP_2:def 5, FUNCT_1: 47;

 hence thesis by A6, A8, A7, Th25;

 end;

 then

 reconsider uM = mru as BinOp of (n -roots_of_1 ) by A1, A3, FUNCT_2: 3, XBOOLE_1: 28;

 set H = multMagma (# (n -roots_of_1 ), uM #);

 reconsider 1F = ( 1_ F_Complex ) as Element of H by Th22;



 A9: ( 1_ F_Complex ) = [**( cos (((2 * PI ) * 0 qua Nat) / n)), ( sin (((2 * PI ) * 0 qua Nat) / n))**] by COMPLFLD: 8, SIN_COS: 31;



 A10: for s1 be Element of H holds (s1 * 1F) = s1 & (1F * s1) = s1 & ex s2 be Element of H st (s1 * s2) = ( 1_ F_Complex ) & (s2 * s1) = ( 1_ F_Complex )

 proof

 let s1 be Element of H;



 A11: ex s2 be 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 be 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 be Element of NAT st ((k + j) mod n) = 0

 proof

 set r = (k mod n);

 r < n by NAT_D: 1;

 then

 consider j be 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 be 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 be 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 be 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 :: UNIROOTS:37

 for n be non zero Element of NAT holds (n -th_roots_of_1 ) is Subgroup of ( MultGroup F_Complex )

 proof

 set MGFC = ( MultGroup F_Complex );

 set cMGFC = the carrier of ( MultGroup F_Complex );

 set FC = F_Complex ;

 let n be non zero Element of NAT ;

 set nth = (n -th_roots_of_1 );

 set cnth = the carrier of nth;



 A1: the carrier of nth = (n -roots_of_1 ) by Def3;

 then

 A2: the carrier of nth c= the carrier of MGFC by Th32;

 the multF of nth = (the multF of FC || (n -roots_of_1 )) & the multF of MGFC = (the multF of FC || cMGFC) by Def1, Def3;

 then the multF of nth = (the multF of MGFC || cnth) by A1, A2, RELAT_1: 74, ZFMISC_1: 96;

 hence thesis by A2, GROUP_2:def 5;

 end;

 begin

 definition

 let n be non zero Nat, L be left_unital non empty doubleLoopStr;

 :: UNIROOTS:def4

 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 be 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 be Nat st i >= (n + 1) holds (p . i) = ( 0. L)

 proof

 let i be Nat such that

 A5: i >= (n + 1);

 now



 A6: (n + 0 ) < (n + 1) by XREAL_1: 8;

 assume i = n;

 hence contradiction by A5, A6;

 end;

 hence thesis by A1, A5;

 end;

 hence thesis by ALGSEQ_1:def 1;

 end;

 end



 Lm4: ( unital_poly ( F_Complex ,1)) = <%( - ( 1_ F_Complex )), ( 1_ F_Complex )%>;

 theorem :: UNIROOTS:38



 Th38: for L be left_unital non empty doubleLoopStr holds for n be non zero Element of NAT holds (( unital_poly (L,n)) . 0 ) = ( - ( 1_ L)) & (( unital_poly (L,n)) . n) = ( 1_ L)

 proof

 let L be left_unital non empty doubleLoopStr, n be non zero Element of NAT ;

 set p = (( 0_. L) +* ( 0 ,( - ( 1_ L))));

 set q = (( 0_. L) +* (n,( 1_ L)));

 0 in NAT ;

 then

 A1: ( unital_poly (L,n)) = (q +* ( 0 ,( - ( 1_ L)))) & 0 in ( dom q) by FUNCT_7: 33, NORMSP_1: 12;

 n in NAT ;

 then n in ( dom p) by NORMSP_1: 12;

 hence thesis by A1, FUNCT_7: 31;

 end;

 theorem :: UNIROOTS:39



 Th39: for L be left_unital non empty doubleLoopStr holds for n be non zero Nat, i be Nat st i <> 0 & i <> n holds (( unital_poly (L,n)) . i) = ( 0. L)

 proof

 let L be left_unital non empty doubleLoopStr, n be non zero Nat;

 let i be Nat such that

 A1: i <> 0 and

 A2: i <> n;

 set p = (( 0_. L) +* ( 0 ,( - ( 1_ L))));



 A3: i in NAT by ORDINAL1:def 12;

 ((p +* (n,( 1_ L))) . i) = (p . i) by A2, FUNCT_7: 32

 .= (( 0_. L) . i) by A1, FUNCT_7: 32

 .= ( 0. L) by A3, FUNCOP_1: 7;

 hence thesis;

 end;

 theorem :: UNIROOTS:40



 Th40: for L be non degenerated well-unital non empty doubleLoopStr, n be non zero Element of NAT holds ( len ( unital_poly (L,n))) = (n + 1)

 proof

 let L be non degenerated well-unital non empty doubleLoopStr;

 let n be non zero Element of NAT ;



 A1: for m be Nat st m is_at_least_length_of ( unital_poly (L,n)) holds (n + 1) <= m

 proof

 let m be Nat such that

 A2: m is_at_least_length_of ( unital_poly (L,n));

 now

 assume m < (n + 1);

 then m <= n by NAT_1: 13;

 then (( unital_poly (L,n)) . n) = ( 0. L) by A2, ALGSEQ_1:def 2;

 hence contradiction by Th38;

 end;

 hence thesis;

 end;



 A3: (n + 1) in NAT by ORDINAL1:def 12;

 for i be Nat st i >= (n + 1) holds (( unital_poly (L,n)) . i) = ( 0. L)

 proof

 let i be Nat such that

 A4: i >= (n + 1);

 now



 A5: (n + 0 ) < (n + 1) by XREAL_1: 8;

 assume i = n;

 hence contradiction by A4, A5;

 end;

 hence thesis by A4, Th39;

 end;

 then (n + 1) is_at_least_length_of ( unital_poly (L,n)) by ALGSEQ_1:def 2;

 hence thesis by A1, ALGSEQ_1:def 3, A3;

 end;

 registration

 let L be non degenerated well-unital non empty doubleLoopStr, n be non zero Element of NAT ;

 cluster ( unital_poly (L,n)) -> non-zero;

 correctness

 proof

 ( len ( unital_poly (L,n))) = (n + 1) by Th40;

 hence thesis by UPROOTS: 17;

 end;

 end

 theorem :: UNIROOTS:41



 Th41: for n be non zero Element of NAT holds for x be Element of F_Complex holds ( eval (( unital_poly ( F_Complex ,n)),x)) = ((( power F_Complex ) . (x,n)) - 1)

 proof

 (1 - 1) = 0 ;

 then

 A1: (1 -' 1) = 0 by XREAL_1: 233;

 reconsider z2 = ( 1_ F_Complex ) as Element of COMPLEX by COMPLFLD:def 1;

 let n be non zero Element of NAT , x be Element of F_Complex ;

 set p = ( unital_poly ( F_Complex ,n));

 consider F be FinSequence of F_Complex such that

 A2: ( eval (p,x)) = ( Sum F) and

 A3: ( len F) = ( len p) and

 A4: for i be 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 be 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 be 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 be 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 be 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 be Nat st k in ( dom (R1 + R2)) holds ((R1 + R2) . k) = (F . k)

 proof

 let k be Nat such that

 A33: k in ( dom (R1 + R2));



 A34: k in ( Seg ( len F)) by A30, A33, FINSEQ_1:def 3;



 A35: k in ( dom F) by A31, A33, FINSEQ_1:def 3;



 A36: 1 <= k by A31, A33, FINSEQ_1: 1;



 A37: (( - ( 1_ F_Complex )) * ( 1_ F_Complex )) = ( - ( 1_ F_Complex ));

 now

 per cases ;

 suppose

 A38: k = 1;

 then (R2 . k) = ( 0. F_Complex ) by A6, A21, A28, A34;

 then

 A39: ((R1 + R2) . 1) = (( - ( 1_ F_Complex )) + ( 0. F_Complex )) by A29, A33, A38, FVSUM_1: 17;

 (F . 1) = ((p . 0 ) * (( power F_Complex ) . (x, 0 ))) by A4, A1, A35, A38

 .= ( - ( 1_ F_Complex )) by A10, A37, GROUP_1:def 7;

 hence thesis by A38, A39, COMPLFLD: 7;

 end;

 suppose

 A40: k <> 1;

 now

 per cases ;

 suppose

 A41: k = ( len F);

 ( len F) <> 0 by A3, A5, Th40;



 then

 A42: (F . ( len F)) = ((p . (( len F) -' 1)) * (( power F_Complex ) . (x,(( len F) -' 1)))) by A4, A12, FINSEQ_1: 3

 .= (( 1_ F_Complex ) * (( power F_Complex ) . (x,n))) by A8, Th38

 .= (( power F_Complex ) . (x,n));

 (R1 . ( len F)) = ( 0. F_Complex ) by A6, A14, A27, A34, A41;



 then ((R1 + R2) . ( len F)) = (( 0. F_Complex ) + (( power F_Complex ) . (x,n))) by A32, A33, A41, FVSUM_1: 17

 .= (( power F_Complex ) . (x,n)) by COMPLFLD: 7;

 hence thesis by A41, A42;

 end;

 suppose

 A43: k <> ( len F);

 A44:

 now

 assume (k -' 1) = n;

 then (k - 1) = n by A36, XREAL_1: 233;

 hence contradiction by A7, A43;

 end;

 1 < k by A36, A40, XXREAL_0: 1;

 then (1 + ( - 1)) < (k + ( - 1)) by XREAL_1: 8;

 then (1 - 1) < (k - 1);

 then 0 < (k -' 1) by A36, XREAL_1: 233;

 then (p . (k -' 1)) = ( 0. F_Complex ) by A44, Th39;

 then

 A45: (F . k) = (( 0. F_Complex ) * (( power F_Complex ) . (x,(k -' 1)))) by A4, A35;



 A46: (R2 . k) = ( 0. F_Complex ) by A21, A28, A34, A43;

 (R1 . k) = ( 0. F_Complex ) by A14, A27, A34, A40;

 then ((R1 + R2) . k) = (( 0. F_Complex ) + ( 0. F_Complex )) by A33, A46, FVSUM_1: 17;

 hence thesis by A45, COMPLFLD: 7;

 end;

 end;

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 then

 A47: (R1 + R2) = F by A12, A31, FINSEQ_1: 13;

 ( Sum null) = ( 0. F_Complex ) by MATRIX_3: 11;

 then ( Sum R1) = (( - ( 1_ F_Complex )) + ( 0. F_Complex )) & ( Sum R2) = (( 0. F_Complex ) + xn) by FVSUM_1: 71, FVSUM_1: 72;

 then ( - z2) = ( - ( 1_ F_Complex )) & ( Sum F) = (( - ( 1_ F_Complex )) + (( power F_Complex ) . (x,n))) by A47, COMPLFLD: 2, COMPLFLD: 7, FVSUM_1: 76;

 hence thesis by A2, COMPLFLD: 8;

 end;

 theorem :: UNIROOTS:42



 Th42: for n be non zero Element of NAT holds ( Roots ( unital_poly ( F_Complex ,n))) = (n -roots_of_1 )

 proof

 let n be non zero Element of NAT ;

 now

 set p = ( unital_poly ( F_Complex ,n));

 let x be object;

 hereby

 assume

 A1: x in ( Roots p);

 then

 reconsider x9 = x as Element of F_Complex ;

 x9 is_a_root_of p by A1, POLYNOM5:def 10;



 then ( 0. F_Complex ) = ( eval (p,x9)) by POLYNOM5:def 7

 .= ((( power F_Complex ) . (x9,n)) - 1) by Th41;

 then x9 is CRoot of n, ( 1_ F_Complex ) by COMPLFLD: 7, COMPLFLD: 8, COMPLFLD: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, COMPLFLD:def 2;

 then ((( power F_Complex ) . (x9,n)) - 1) = 0c ;

 then ( eval (p,x9)) = ( 0. F_Complex ) by Th41, COMPLFLD: 7;

 then x9 is_a_root_of p by POLYNOM5:def 7;

 hence x in ( Roots ( unital_poly ( F_Complex ,n))) by POLYNOM5:def 10;

 end;

 hence thesis by TARSKI: 2;

 end;

 theorem :: UNIROOTS:43



 Th43: for n be Element of NAT , z be Element of F_Complex st z is Real holds ex x be Real st x = z & (( power F_Complex ) . (z,n)) = (x |^ n)

 proof

 let n be Element of NAT ;

 let z be Element of F_Complex ;

 assume z is Real;

 then

 reconsider x = z as Real;

 per cases ;

 suppose

 A1: x = 0 ;

 then

 A2: z = ( 0. F_Complex ) by COMPLFLD:def 1;

 thus thesis

 proof

 per cases ;

 suppose

 A3: n = 0 ;



 then (( power F_Complex ) . (z,n)) = 1 by COMPLFLD: 8, GROUP_1:def 7

 .= (x |^ n) by A3, NEWTON: 4;

 hence thesis;

 end;

 suppose

 A4: n > 0 ;

 then

 A5: n >= ( 0 + 1) by NAT_1: 13;

 (( power F_Complex ) . (z,n)) = ( 0. F_Complex ) by A2, A4, VECTSP_1: 36

 .= (x |^ n) by A1, A5, COMPLFLD: 7, NEWTON: 11;

 hence thesis;

 end;

 end;

 end;

 suppose

 A6: x <> 0 ;

 defpred P[ Nat] means (( power F_Complex ) . (z,$1)) = (x |^ $1);



 A7: for n be Nat st P[n] holds P[(n + 1)]

 proof

 let n be Nat such that

 A8: P[n];

 reconsider nn = n as Element of NAT by ORDINAL1:def 12;

 (( power F_Complex ) . (z,(n + 1))) = ((( power F_Complex ) . (z,nn)) * z) by GROUP_1:def 7

 .= ((x #Z n) * x) by A8, PREPOWER: 36

 .= ((x #Z n) * (x #Z 1)) by PREPOWER: 35

 .= (x #Z (n + 1)) by A6, PREPOWER: 44

 .= (x |^ (n + 1)) by PREPOWER: 36;

 hence thesis;

 end;

 (( power F_Complex ) . (z, 0 )) = 1r by COMPLFLD: 8, GROUP_1:def 7

 .= (x #Z 0 ) by PREPOWER: 34

 .= (x |^ 0 ) by PREPOWER: 36;

 then

 A9: P[ 0 ];

 for n be Nat holds P[n] from NAT_1:sch 2( A9, A7);

 then (( power F_Complex ) . (z,n)) = (x |^ n);

 hence thesis;

 end;

 end;

 theorem :: UNIROOTS:44



 Th44: for n be non zero Element of NAT holds for x be Real holds ex y be Element of F_Complex st y = x & ( eval (( unital_poly ( F_Complex ,n)),y)) = ((x |^ n) - 1)

 proof

 let n be non zero Element of NAT , x be Real;

 x in COMPLEX by XCMPLX_0:def 2;

 then

 reconsider y = x as Element of F_Complex by COMPLFLD:def 1;

 ex x2 be 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 :: UNIROOTS:45



 Th45: for n be non zero Element of NAT holds ( BRoots ( unital_poly ( F_Complex ,n))) = (((n -roots_of_1 ),1) -bag )

 proof

 let n be non zero Element of NAT ;

 set p = ( unital_poly ( F_Complex ,n));



 A1: ( degree ( BRoots p)) = (( len p) -' 1) by UPROOTS: 59

 .= ((n + 1) -' 1) by Th40

 .= n by NAT_D: 34;



 A2: ( card (n -roots_of_1 )) = n by Th27;

 ( Roots p) = (n -roots_of_1 ) & ( support ( BRoots p)) = ( Roots p) by Th42, UPROOTS:def 9;

 hence thesis by A1, A2, UPROOTS: 13;

 end;

 theorem :: UNIROOTS:46



 Th46: for n be non zero Element of NAT holds ( unital_poly ( F_Complex ,n)) = ( poly_with_roots (((n -roots_of_1 ),1) -bag ))

 proof

 let n be non zero Element of NAT ;

 set p = ( unital_poly ( F_Complex ,n));

 ( len p) = (n + 1) by Th40;



 then (p . (( len p) -' 1)) = (p . n) by NAT_D: 34

 .= ( 1_ F_Complex ) by Th38;



 hence ( unital_poly ( F_Complex ,n)) = ( poly_with_roots ( BRoots ( unital_poly ( F_Complex ,n)))) by UPROOTS: 65

 .= ( poly_with_roots (((n -roots_of_1 ),1) -bag )) by Th45;

 end;

 theorem :: UNIROOTS:47



 Th47: for n be non zero Element of NAT , i be Element of F_Complex st i is Integer holds ( eval (( unital_poly ( F_Complex ,n)),i)) is Integer

 proof

 let n be non zero Element of NAT ;

 let i be Element of F_Complex such that

 A1: i is Integer;

 reconsider j = i as Integer by A1;

 ex y be Element of F_Complex st y = i & ( eval (( unital_poly ( F_Complex ,n)),y)) = ((j |^ n) - 1) by Th44;

 hence thesis;

 end;

 begin

 definition

 let d be non zero Nat;

 :: UNIROOTS:def5

 func cyclotomic_poly d -> Polynomial of F_Complex means

 : Def5: ex s be non empty finite Subset of F_Complex st s = { y where y be Element of ( MultGroup F_Complex ) : ( ord y) = d } & it = ( poly_with_roots ((s,1) -bag ));

 existence

 proof

 set cMGFC = the carrier of ( MultGroup F_Complex );

 reconsider d as non zero Element of NAT by ORDINAL1:def 12;

 defpred P[ Element of cMGFC] means ( ord $1) = d;

 set s = { y where y be 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 * )) = (( cos (((2 * PI ) * 1) / d)) + (( sin (((2 * PI ) * 1) / d)) * )) 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 be Element of cMGFC : ( ord y) divides d } by Th35;



 A4: s c= (d -roots_of_1 )

 proof

 let a be object;

 assume a in s;

 then ex y be 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 :: UNIROOTS:48



 Th48: ( cyclotomic_poly 1) = <%( - ( 1_ F_Complex )), ( 1_ F_Complex )%>

 proof

 set cMGFC = the carrier of ( MultGroup F_Complex );

 consider s be non empty finite Subset of F_Complex such that

 A1: s = { y where y be 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 be Element of cMGFC : ( ord x) divides 1 } by Th35;

 now

 let x be object;

 hereby

 assume x in s;

 then ex x1 be 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 be Element of cMGFC such that

 A4: x = x1 and

 A5: ( ord x1) divides 1 by A3;

 ( ord x1) = 1 by A5, WSIERP_1: 15;

 hence x in s by A1, A4;

 end;

 then s = (1 -roots_of_1 ) by TARSKI: 2;

 hence thesis by A2, Lm4, Th46;

 end;

 theorem :: UNIROOTS:49



 Th49: for n be non zero Element of NAT , f be FinSequence of the carrier of ( Polynom-Ring F_Complex ) st ( len f) = n & for i be non zero Element of NAT st i in ( dom f) holds ( not i divides n implies (f . i) = <%( 1_ F_Complex )%>) & (i divides n implies (f . i) = ( cyclotomic_poly i)) holds ( unital_poly ( F_Complex ,n)) = ( Product f)

 proof

 set cMGFC = the carrier of ( MultGroup F_Complex );

 let n be non zero Element of NAT , f be FinSequence of the carrier of ( Polynom-Ring F_Complex ) such that

 A1: ( len f) = n and

 A2: for i be non zero Element of NAT st i in ( dom f) holds ( not i divides n implies (f . i) = <%( 1_ F_Complex )%>) & (i divides n implies (f . i) = ( cyclotomic_poly i));

 defpred P[ Nat, set] means for fi be 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 be Element of ( MultGroup F_Complex ) : y in nr1 & ( ord y) <= $1 };

 A3:

 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 be FinSequence of ( Polynom-Ring F_Complex ) such that ( dom F) = ( Seg ( len f)) and

 A4: for i be Nat st i in ( Seg ( len f)) holds P[i, (F . i)] from FINSEQ_1:sch 5( A3);

 defpred R[ Nat] means ex t be finite Subset of F_Complex st t = MG($1) & (F . $1) = ( poly_with_roots ((t,1) -bag ));

 A5:

 now

 let i be Element of NAT ;

 MG(i) c= nr1

 proof

 let x be object;

 assume x in MG(i);

 then ex y be 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 be Element of ( MultGroup F_Complex ) : ( ord x) divides n } by Th35;



 A7: for i be Element of NAT st 1 <= i & i < ( len f) holds R[i] implies R[(i + 1)]

 proof

 let i be Element of NAT such that

 A8: 1 <= i and

 A9: i < ( len f) and

 A10: R[i];

 reconsider fi = (f | ( Seg i)) as FinSequence of the carrier of ( Polynom-Ring F_Complex ) by FINSEQ_1: 18;

 i in ( Seg ( len f)) by A8, A9, FINSEQ_1: 1;

 then

 A11: (F . i) = ( Product fi) by A4;

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



 A12: (i + 1) <= ( len f) by A9, NAT_1: 13;

 then (i + 1) = ( min ((i + 1),( len f))) by XXREAL_0:def 9;

 then

 A13: ( len fi1) = (i + 1) by FINSEQ_2: 21;

 1 <= (i + 1) by A8, NAT_1: 13;

 then

 A14: (i + 1) in ( Seg ( len f)) by A12, FINSEQ_1: 1;

 then

 A15: (i + 1) in ( dom f) by FINSEQ_1:def 3;

 (i + 1) in NAT by ORDINAL1:def 12;

 then

 reconsider sB = MG(+) as finite Subset of F_Complex by A5;

 take sB;

 thus sB = MG(+);

 set B = ((sB,1) -bag );

 consider sb be finite Subset of F_Complex such that

 A16: sb = MG(i) and

 A17: (F . i) = ( poly_with_roots ((sb,1) -bag )) by A10;



 A18: ((f | ( Seg (i + 1))) . (i + 1)) = (f . (i + 1)) by FINSEQ_1: 4, FUNCT_1: 49;

 then

 reconsider fi1d1 = (fi1 . (i + 1)) as Element of the carrier of ( Polynom-Ring F_Complex ) by A15, FINSEQ_2: 11;

 set b = ((sb,1) -bag );

 reconsider fi1d1p = fi1d1 as Polynomial of F_Complex by POLYNOM3:def 10;

 fi = (fi1 | ( Seg i)) by Lm2, NAT_1: 12;

 then fi1 = (fi ^ <*fi1d1*>) by A13, FINSEQ_3: 55;



 then

 A19: ( Product fi1) = (( Product fi) * fi1d1) by GROUP_4: 6

 .= (( poly_with_roots b) *' fi1d1p) by A17, A11, POLYNOM3:def 10;

 per cases ;

 suppose

 A20: not (i + 1) divides n;

 set eb = ( EmptyBag the carrier of F_Complex );

 now

 let x be object;

 hereby

 assume x in sB;

 then

 consider y be 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 be Element of cMGFC such that

 A24: x = y & y in nr1 and

 A25: ( ord y) <= i by A16;

 ( ord y) <= (i + 1) by A25, NAT_1: 12;

 hence x in sB by A24;

 end;

 then

 A26: sB = sb by TARSKI: 2;

 (f . (i + 1)) = <%( 1_ F_Complex )%> by A2, A15, A20

 .= ( poly_with_roots eb) by UPROOTS: 60;



 hence (F . (i + 1)) = (( poly_with_roots b) *' ( poly_with_roots eb)) by A4, A14, A18, A19

 .= ( poly_with_roots (b + eb)) by UPROOTS: 64

 .= ( poly_with_roots B) by A26, PRE_POLY: 53;

 end;

 suppose

 A27: (i + 1) divides n;

 consider scb be non empty finite Subset of F_Complex such that

 A28: scb = { y where y be Element of cMGFC : ( ord y) = (i + 1) } and

 A29: ( cyclotomic_poly (i + 1)) = ( poly_with_roots ((scb,1) -bag )) by Def5;

 now

 let x be object;

 hereby

 assume x in sB;

 then

 consider y be 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 be 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 be Element of cMGFC such that

 A36: x = y and

 A37: ( ord y) = (i + 1) by A28;

 y in nr1 by A6, A27, A37;

 hence x in sB by A36, A37;

 end;

 end;

 then

 A38: sB = (sb \/ scb) by TARSKI: 2;

 set cb = ((scb,1) -bag );



 A39: sb misses scb

 proof

 assume (sb /\ scb) <> {} ;

 then

 consider x be object such that

 A40: x in (sb /\ scb) by XBOOLE_0:def 1;

 x in scb by A40, XBOOLE_0:def 4;

 then

 A41: ex y2 be Element of cMGFC st x = y2 & ( ord y2) = (i + 1) by A28;

 x in sb by A40, XBOOLE_0:def 4;

 then ex y1 be 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() as finite Subset of F_Complex by A5;

 take t;

 thus t = MG();

 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 be non empty finite Subset of F_Complex such that

 A46: sB = { y where y be Element of cMGFC : ( ord y) = 1 } and

 A47: (F . 1) = ( poly_with_roots ((sB,1) -bag )) by Def5;

 now

 let x be object;

 hereby

 assume x in MG();

 then

 consider y be Element of cMGFC such that

 A48: x = y and

 A49: y in nr1 and

 A50: ( ord y) <= 1;

 not y is 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 be 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() by A51, A52;

 end;

 hence thesis by A47, TARSKI: 2;

 end;

 for i be Element of NAT st 1 <= i & i <= ( len f) holds R[i] from INT_1:sch 7( A43, A7);

 then

 A53: ex t be finite Subset of F_Complex st t = MG(len) & (F . ( len f)) = ( poly_with_roots ((t,1) -bag )) by A1, A42;

 set b = ((nr1,1) -bag );



 A54: f = (f | ( Seg ( len f))) by FINSEQ_3: 49;

 now

 let x be object;

 hereby

 assume

 A55: x in nr1;

 then

 consider y be 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 be Element of ( MultGroup F_Complex ) st y = x & y in nr1 & ( ord y) <= n;

 hence x in nr1;

 end;

 then

 A58: nr1 = sB by TARSKI: 2;



 thus ( unital_poly ( F_Complex ,n)) = ( poly_with_roots b) by Th46

 .= ( Product f) by A1, A4, A58, A53, A54, FINSEQ_1: 3;

 end;

 theorem :: UNIROOTS:50



 Th50: for n be non zero Element of NAT holds ex f be FinSequence of the carrier of ( Polynom-Ring F_Complex ), p be Polynomial of F_Complex st p = ( Product f) & ( dom f) = ( Seg n) & (for i be non zero Element of NAT st i in ( Seg n) holds ( not i divides n or i = n implies (f . i) = <%( 1_ F_Complex )%>) & (i divides n & i <> n implies (f . i) = ( cyclotomic_poly i))) & ( unital_poly ( F_Complex ,n)) = (( cyclotomic_poly n) *' p)

 proof

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

 let n be non zero Element of NAT ;

 defpred P[ set, set] means ex i be non zero Element of NAT st i = $1 & ( not i divides n implies $2 = <%( 1_ F_Complex )%>) & (i divides n implies $2 = ( cyclotomic_poly i));

 consider m be Nat such that

 A1: n = (m + 1) by NAT_1: 6;



 A2: for k be Nat st k in ( Seg n) holds ex x be Element of cPRFC st P[k, x]

 proof

 let k be Nat;

 assume k in ( Seg n);

 then

 reconsider i = k as non zero Element of NAT by FINSEQ_1: 1;

 per cases ;

 suppose

 A3: not i divides n;

 reconsider FC1 = <%( 1_ F_Complex )%> as Element of cPRFC by POLYNOM3:def 10;

 take FC1;

 take i;

 thus i = k;

 thus thesis by A3;

 end;

 suppose

 A4: i divides n;

 reconsider FC1 = ( cyclotomic_poly i) as Element of cPRFC by POLYNOM3:def 10;

 take FC1;

 take i;

 thus i = k;

 thus thesis by A4;

 end;

 end;

 consider f be FinSequence of cPRFC such that

 A5: ( dom f) = ( Seg n) and

 A6: for k be Nat st k in ( Seg n) holds P[k, (f /. k)] from RECDEF_1:sch 17( A2);

 reconsider fm = (f | ( Seg m)) as FinSequence of cPRFC by FINSEQ_1: 18;



 A7: ( len f) = n by A5, FINSEQ_1:def 3;

 A8:

 now

 let i be non zero Element of NAT ;

 assume

 A9: i in ( dom f);

 then

 A10: i <= n by A5, FINSEQ_1: 1;

 (ex j be non zero Element of NAT st j = i & ( not j divides n implies (f /. i) = <%( 1_ F_Complex )%>) & (j divides n implies (f /. i) = ( cyclotomic_poly j))) & 1 <= i by A5, A6, A9, FINSEQ_1: 1;

 hence ( not i divides n implies (f . i) = <%( 1_ F_Complex )%>) & (i divides n implies (f . i) = ( cyclotomic_poly i)) by A7, A10, FINSEQ_4: 15;

 end;

 reconsider FC1 = <%( 1_ F_Complex )%> as Element of cPRFC by POLYNOM3:def 10;

 <*FC1*> is FinSequence of cPRFC;

 then

 reconsider h = (fm ^ <* <%( 1_ F_Complex )%>*>) as FinSequence of cPRFC by FINSEQ_1: 75;

 reconsider p = ( Product h) as Polynomial of F_Complex by POLYNOM3:def 10;

 take h, p;

 thus p = ( Product h);



 A11: m <= n by A1, NAT_1: 13;

 then

 A12: ( len fm) = m by A7, FINSEQ_1: 17;

 reconsider cpn = ( cyclotomic_poly n) as Element of cPRFC by POLYNOM3:def 10;

 reconsider fn = (f | ( Seg n)) as FinSequence of cPRFC by FINSEQ_1: 18;

 1 <= n by NAT_1: 53;

 then

 A13: n in ( Seg n) by FINSEQ_1: 1;

 then

 A14: (f . n) = ( cyclotomic_poly n) by A5, A8;

 ( len <* <%( 1_ F_Complex )%>*>) = 1 by FINSEQ_1: 40;

 hence ( dom h) = ( Seg n) by A1, A12, FINSEQ_1:def 7;



 A15: ( dom fm) = ( Seg m) by A7, A11, FINSEQ_1: 17;

 thus for i be non zero Element of NAT st i in ( Seg n) holds ( not i divides n or i = n implies (h . i) = <%( 1_ F_Complex )%>) & (i divides n & i <> n implies (h . i) = ( cyclotomic_poly i))

 proof

 let i be non zero Element of NAT ;

 assume

 A16: i in ( Seg n);

 per cases ;

 suppose

 A17: i in ( Seg m);

 then

 A18: (fm . i) = (f . i) & i <= m by FINSEQ_1: 1, FUNCT_1: 49;

 (h . i) = (fm . i) by A15, A17, FINSEQ_1:def 7;

 hence thesis by A5, A1, A8, A16, A18, NAT_1: 13;

 end;

 suppose not i in ( Seg m);

 then not (1 <= i & i <= m) by FINSEQ_1: 1;

 then

 A19: n <= i by A1, A16, FINSEQ_1: 1, NAT_1: 13;



 A20: i <= n by A16, FINSEQ_1: 1;

 1 in ( Seg 1) by FINSEQ_1: 1;

 then 1 in ( dom <* <%( 1_ F_Complex )%>*>) by FINSEQ_1: 38;



 then (h . n) = ( <* <%( 1_ F_Complex )%>*> . 1) by A1, A12, FINSEQ_1:def 7

 .= <%( 1_ F_Complex )%> 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 :: UNIROOTS:51



 Th51: for d be non zero Element of NAT , i be Element of NAT holds ((( cyclotomic_poly d) . 0 ) = 1 or (( cyclotomic_poly d) . 0 ) = ( - 1)) & (( cyclotomic_poly d) . i) is integer

 proof

 deffunc cp( non zero Nat) = ( cyclotomic_poly $1);

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

 set cFC = the carrier of F_Complex ;

 defpred P[ non zero Element of NAT ] means (( cp($1) . 0 ) = 1 or ( cp($1) . 0 ) = ( - 1)) & for i be Element of NAT holds ( cp($1) . i) is integer;



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

 A2:

 now

 let k be non zero Element of NAT such that

 A3: for n be non zero Element of NAT st n < k holds P[n];



 A4: 1 <= k by Lm1;

 per cases by A4, XXREAL_0: 1;

 suppose

 A5: k = 1;

 now

 let i be Element of NAT ;

 per cases by NAT_1: 23;

 suppose i = 0 ;

 hence ( cp(k) . i) is integer by A1, A5, Th48, POLYNOM5: 38;

 end;

 suppose i = 1;

 hence ( cp(k) . i) is integer by A5, Th48, COMPLFLD: 8, POLYNOM5: 38;

 end;

 suppose i >= 2;

 hence ( cp(k) . i) is integer by A5, Th48, COMPLFLD: 7, POLYNOM5: 38;

 end;

 end;

 hence P[k] by A1, A5, Th48, POLYNOM5: 38;

 end;

 suppose

 A6: k > 1;

 consider f be FinSequence of cPRFC, p be Polynomial of F_Complex such that

 A7: p = ( Product f) and

 A8: ( dom f) = ( Seg k) and

 A9: for i be non zero Element of NAT st i in ( Seg k) holds ( not i divides k or i = k implies (f . i) = <%( 1_ F_Complex )%>) & (i divides k & i <> k implies (f . i) = cp(i)) and

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

 defpred G[ Nat, object] means ex g be FinSequence of cPRFC, p be Polynomial of F_Complex st g = (f | ( Seg $1)) & p = ( Product g) & $2 = p & ((p . 0 ) = 1 or (p . 0 ) = ( - 1)) & for j be Element of NAT holds (p . j) is integer;

 defpred H[ Nat] means $1 in ( Seg ( len f)) implies ex x be object st G[$1, x];



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



 A12: for l be Nat st H[l] holds H[(l + 1)]

 proof

 let l be Nat;

 assume

 A13: H[l];

 assume

 A14: (l + 1) in ( Seg ( len f));

 per cases ;

 suppose

 A15: l = 0 ;

 reconsider fl1 = (f . (l + 1)) as Element of cPRFC by A8, A11, A14, FINSEQ_2: 11;

 reconsider g = (f | ( Seg (l + 1))) as FinSequence of cPRFC by FINSEQ_1: 18;

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

 ( <*> cPRFC) = (f | ( Seg 0 ) qua set);



 then g = (( <*> cPRFC) ^ <*(f . (l + 1))*>) by A8, A11, A14, A15, FINSEQ_5: 10

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

 then

 A16: p = fl1 by FINSOP_1: 11;

 take p;

 take g;

 take p;

 thus g = (f | ( Seg (l + 1))) & p = ( Product g) & p = p;

 1 divides k by NAT_D: 6;

 then

 A17: (f . 1) = cp() 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 be 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 be FinSequence of cPRFC, p be 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 be Element of NAT holds (p . j) is integer by A20;

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

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

 then

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

 thus thesis

 proof

 per cases ;

 suppose not (l + 1) divides k or (l + 1) = k;

 then

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

 consider r be FinSequence of F_Complex such that

 A27: ( len r) = ( 0 + 1) and

 A28: (p1 . 0 ) = ( Sum r) and

 A29: for m be Element of NAT st m in ( dom r) holds (r . m) = ((p . (m -' 1)) * (fl1p . (( 0 + 1) -' m))) by A25, POLYNOM3:def 9;

 1 in ( dom r) by A27, FINSEQ_3: 25;

 then

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

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

 then

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

 1 in ( dom r) by A27, FINSEQ_3: 25;



 then

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

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

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

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

 thus (p1 . 0 ) = 1 or (p1 . 0 ) = ( - 1)

 proof

 per cases by A23;

 suppose (p . 0 ) = 1;

 hence thesis by A31;

 end;

 suppose (p . 0 ) = ( - 1);

 hence thesis by A31;

 end;

 end;

 let j be Element of NAT ;

 consider r be FinSequence of F_Complex such that ( len r) = (j + 1) and

 A32: (p1 . j) = ( Sum r) and

 A33: for m be Element of NAT st m in ( dom r) holds (r . m) = ((p . (m -' 1)) * (fl1p . ((j + 1) -' m))) by A25, POLYNOM3:def 9;

 for i be Element of NAT st i in ( dom r) holds (r . i) is integer

 proof

 let i be Element of NAT ;

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

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

 now



 A34: j1i = 0 or j1i >= ( 0 + 1) by NAT_1: 13;

 per cases by A34;

 case j1i = 0 ;

 hence (fl1p . j1i) = 1 by A26, COMPLFLD: 8, POLYNOM5: 32;

 end;

 case j1i >= 1;

 hence (fl1p . j1i) = 0 by A26, COMPLFLD: 7, POLYNOM5: 32;

 end;

 end;

 then

 reconsider fl1pj1i = (fl1p . ((j + 1) -' i)) as Integer;

 assume i in ( dom r);



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

 .= (pi1 * fl1pj1i);

 hence thesis;

 end;

 hence thesis by A32, Th4;

 end;

 suppose

 A35: (l + 1) divides k & (l + 1) <> k;

 consider r be FinSequence of F_Complex such that

 A36: ( len r) = ( 0 + 1) and

 A37: (p1 . 0 ) = ( Sum r) and

 A38: for m be Element of NAT st m in ( dom r) holds (r . m) = ((p . (m -' 1)) * (fl1p . (( 0 + 1) -' m))) by A25, POLYNOM3:def 9;

 1 in ( dom r) by A36, FINSEQ_3: 25;

 then

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

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

 then

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

 1 in ( dom r) by A36, FINSEQ_3: 25;



 then

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

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

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

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

 then

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



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



 A43: fl1p = cp(+) by A9, A11, A14, A35;

 then

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



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

 thus (p1 . 0 ) = 1 or (p1 . 0 ) = ( - 1)

 proof

 per cases by A23;

 suppose (p . 0 ) = 1;

 hence thesis by A3, A43, A41, A40;

 end;

 suppose (p . 0 ) = ( - 1);

 hence thesis by A40, A44;

 end;

 end;

 let j be Element of NAT ;

 consider r be FinSequence of F_Complex such that ( len r) = (j + 1) and

 A45: (p1 . j) = ( Sum r) and

 A46: for m be Element of NAT st m in ( dom r) holds (r . m) = ((p . (m -' 1)) * (fl1p . ((j + 1) -' m))) by A25, POLYNOM3:def 9;

 for i be Element of NAT st i in ( dom r) holds (r . i) is integer

 proof

 let i be Element of NAT ;

 (l + 1) in NAT by ORDINAL1:def 12;

 then

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

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

 assume i in ( dom r);



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

 .= (pi1 * fl1pj1i);

 hence thesis;

 end;

 hence thesis by A45, Th4;

 end;

 end;

 end;

 end;

 defpred C[ Nat] means ( cp(k) . $1) is integer;



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



 A48: H[ 0 ] by FINSEQ_1: 1;

 for l be Nat holds H[l] from NAT_1:sch 2( A48, A12);

 then

 A49: for l be Nat st l in ( Seg ( len f)) holds ex x be object st G[l, x];

 consider F be FinSequence such that ( dom F) = ( Seg ( len f)) and

 A50: for i be Nat st i in ( Seg ( len f)) holds G[i, (F . i)] from FINSEQ_1:sch 1( A49);

 consider g be FinSequence of cPRFC, p1 be Polynomial of F_Complex such that

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

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

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



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

 A55:

 now

 let m be Nat;

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

 consider r be FinSequence of cFC such that

 A56: ( len r) = (m + 1) and

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

 A58: for l be Element of NAT st l in ( dom r) holds (r . l) = ((p . (l -' 1)) * ( cp(k) . ((m1 + 1) -' l))) by A10, POLYNOM3:def 9;

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

 now

 per cases ;

 suppose m1 = 0 ;

 hence Src is integer by A1, A57, Th38;

 end;

 suppose m1 = k;

 hence Src is integer by A57, Th38, COMPLFLD: 8;

 end;

 suppose m1 <> 0 & m1 <> k;

 hence Src is integer by A57, Th39, COMPLFLD: 7;

 end;

 end;

 then

 reconsider Sr = Src as Integer;



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

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

 reconsider Ssc = ( Sum s) as Element of COMPLEX by COMPLFLD:def 1;

 assume

 A60: for n be Nat st n < m holds C[n];

 now

 let i be Element of NAT ;

 assume

 A61: i in ( dom s);

 per cases ;

 suppose ( len r) < 2;

 then s = {} by FINSEQ_6:def 4;

 hence (s . i) is integer;

 end;

 suppose

 A62: (1 + 1) <= ( len r);

 then

 A63: (( len s) + (1 + 1)) = (( len r) + 1) by FINSEQ_6:def 4;

 per cases ;

 suppose m = 0 ;

 hence (s . i) is integer by A56, A62;

 end;

 suppose

 A64: m > 0 ;

 i <> 0 by A61, FINSEQ_3: 25;

 then

 reconsider cpkmi = ( cp(k) . (m -' i)) as Integer by A60, A64, NAT_2: 9;

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

 i <> 0 by A61, FINSEQ_3: 25;

 then

 consider i1 be Nat such that

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



 A66: i <= ( len s) by A61, FINSEQ_3: 25;

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

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



 then

 A67: (r . (1 + i)) = ((p . ((1 + i) -' 1)) * ( cp(k) . ((m + 1) -' (1 + i)))) by A58

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

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

 .= (ppi * cpkmi) by NAT_D: 34;

 i1 < ( len s) by A66, A65, NAT_1: 13;



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

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

 hence (s . i) is integer by A67;

 end;

 end;

 end;

 then

 reconsider Ss = Ssc as Integer by Th4;



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

 then

 A69: 1 in ( dom r) by FINSEQ_3: 25;

 then

 reconsider r1 = (r . 1) as Element of cFC by FINSEQ_2: 11;

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

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

 then ( Sum r) = (r1 + ( Sum s)) by A59, FVSUM_1: 72;

 then r1c = (Sr - Ss);

 then

 reconsider r1i = r1 as Integer;



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

 .= ((p . 0 ) * ( cp(k) . m1)) by A47, NAT_D: 34;

 per cases by A7, A11, A51, A52, FINSEQ_3: 49;

 suppose (p . 0 ) = 1;

 hence C[m] by A70;

 end;

 suppose (p . 0 ) = ( - 1);



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

 .= ( - (( 1_ F_Complex ) * ( cp(k) . m1))) by VECTSP_1: 9

 .= ( - ( cp(k) . m1));



 then ( 0. F_Complex ) = (( - ( cp(k) . m1)) + ( - r1)) by RLVECT_1:def 10

 .= (( - r1) - ( cp(k) . m1));

 then ( - r1) = ( cp(k) . m) by VECTSP_1: 19;

 then ( - r1i) = ( cp(k) . m) by COMPLFLD: 2;

 hence C[m];

 end;

 end;



 A71: for i be Nat holds C[i] from NAT_1:sch 4( A55);

 consider r be FinSequence of cFC such that

 A72: ( len r) = ( 0 + 1) and

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

 A74: for l be Element of NAT st l in ( dom r) holds (r . l) = ((p . (l -' 1)) * ( cp(k) . (( 0 + 1) -' l))) by A10, POLYNOM3:def 9;



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

 then

 reconsider r1 = (r . 1) as Element of cFC by FINSEQ_2: 11;

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



 then

 A76: ( Sum r) = (r . 1) by RLVECT_1: 44

 .= ((p . 0 ) * ( cp(k) . 0 )) by A74, A47, A75;

 ( cp(k) . 0 ) = 1 or ( cp(k) . 0 ) = ( - 1)

 proof

 per cases by A7, A11, A51, A52, FINSEQ_3: 49;

 suppose (p . 0 ) = 1;

 hence thesis by A1, A73, A76, Th38;

 end;

 suppose (p . 0 ) = ( - 1);



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

 .= ( - (( 1_ F_Complex ) * ( cp(k) . 0 ))) by VECTSP_1: 9

 .= ( - ( cp(k) . 0 ));

 hence thesis by COMPLFLD: 8, RLVECT_1: 18;

 end;

 end;

 hence P[k] by A71;

 end;

 end;

 for d be non zero Element of NAT holds P[d] from CompIndNE( A2);

 hence thesis;

 end;

 theorem :: UNIROOTS:52



 Th52: for d be non zero Element of NAT , z be Element of F_Complex st z is Integer holds ( eval (( cyclotomic_poly d),z)) is Integer

 proof

 let d be non zero Element of NAT , z be Element of F_Complex such that

 A1: z is Integer;

 set phi = ( cyclotomic_poly d);

 consider F be FinSequence of F_Complex such that

 A2: ( eval (phi,z)) = ( Sum F) and ( len F) = ( len phi) and

 A3: for i be 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 be 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 :: UNIROOTS:53



 Th53: for n,ni be non zero Element of NAT , f be FinSequence of the carrier of ( Polynom-Ring F_Complex ), s be finite Subset of F_Complex st s = { y where y be Element of ( MultGroup F_Complex ) : ( ord y) divides n & not ( ord y) divides ni & ( ord y) <> n } & ( dom f) = ( Seg n) & for i be non zero Element of NAT st i in ( dom f) holds ( not i divides n or i divides ni or i = n implies (f . i) = <%( 1_ F_Complex )%>) & (i divides n & not i divides ni & i <> n implies (f . i) = ( cyclotomic_poly i)) holds ( Product f) = ( poly_with_roots ((s,1) -bag ))

 proof

 set cMGFC = the carrier of ( MultGroup F_Complex );

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

 let n,ni be non zero Element of NAT ;

 let f be FinSequence of cPRFC, s be finite Subset of F_Complex such that

 A1: s = { y where y be 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 be non zero Element of NAT st i in ( dom f) holds ( not i divides n or i divides ni or i = n implies (f . i) = <%( 1_ F_Complex )%>) & (i divides n & not i divides ni & i <> n implies (f . i) = ( cyclotomic_poly i));

 deffunc MG( Nat) = { y where y be Element of cMGFC : y in s & ( ord y) <= $1 };

 A4:

 now

 let i be Element of NAT ;

 MG(i) c= s

 proof

 let x be object;

 assume x in MG(i);

 then ex y be 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 be FinSequence of cPRFC st fi = (f | ( Seg $1)) holds $2 = ( Product fi);

 A6:

 now

 let i be 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 be FinSequence of cPRFC such that ( dom F) = ( Seg ( len f)) and

 A7: for i be Nat st i in ( Seg ( len f)) holds P[i, (F . i)] from FINSEQ_1:sch 5( A6);

 defpred R[ Nat] means ex t be finite Subset of F_Complex st t = MG($1) & (F . $1) = ( poly_with_roots ((t,1) -bag ));



 A8: for i be Element of NAT st 1 <= i & i < ( len f) holds R[i] implies R[(i + 1)]

 proof

 let i be Element of NAT such that

 A9: 1 <= i and

 A10: i < ( len f) and

 A11: R[i];

 reconsider fi = (f | ( Seg i)) as FinSequence of the carrier of ( Polynom-Ring F_Complex ) by FINSEQ_1: 18;

 i in ( Seg ( len f)) by A9, A10, FINSEQ_1: 1;

 then

 A12: (F . i) = ( Product fi) by A7;

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



 A13: (i + 1) <= ( len f) by A10, NAT_1: 13;

 then (i + 1) = ( min ((i + 1),( len f))) by XXREAL_0:def 9;

 then

 A14: ( len fi1) = (i + 1) by FINSEQ_2: 21;

 (i + 1) in NAT by ORDINAL1:def 12;

 then

 reconsider sB = MG(+) as finite Subset of F_Complex by A4;

 take sB;

 thus sB = MG(+);

 set B = ((sB,1) -bag );

 consider sb be finite Subset of F_Complex such that

 A15: sb = MG(i) and

 A16: (F . i) = ( poly_with_roots ((sb,1) -bag )) by A11;

 1 <= (i + 1) by A9, NAT_1: 13;

 then

 A17: (i + 1) in ( Seg ( len f)) by A13, FINSEQ_1: 1;

 then

 A18: (i + 1) in ( dom f) by FINSEQ_1:def 3;



 A19: ((f | ( Seg (i + 1))) . (i + 1)) = (f . (i + 1)) by FINSEQ_1: 4, FUNCT_1: 49;

 then

 reconsider fi1d1 = (fi1 . (i + 1)) as Element of the carrier of ( Polynom-Ring F_Complex ) by A18, FINSEQ_2: 11;

 reconsider fi1d1p = fi1d1 as Polynomial of F_Complex by POLYNOM3:def 10;



 A20: (F . (i + 1)) = ( Product fi1) by A7, A17;

 set b = ((sb,1) -bag );

 fi = (fi1 | ( Seg i)) by Lm2, NAT_1: 12;

 then fi1 = (fi ^ <*fi1d1*>) by A14, FINSEQ_3: 55;

 then ( Product fi1) = (( Product fi) * fi1d1) by GROUP_4: 6;

 then

 A21: ( Product fi1) = (( poly_with_roots b) *' fi1d1p) by A12, A16, POLYNOM3:def 10;

 per cases ;

 suppose

 A22: not (i + 1) divides n or (i + 1) divides ni or (i + 1) = n;

 A23:

 now

 let x be object;

 hereby

 assume x in sB;

 then

 consider y be Element of ( MultGroup F_Complex ) such that

 A24: x = y and

 A25: y in s and

 A26: ( ord y) <= (i + 1);

 ex y1 be 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 be Element of ( MultGroup F_Complex ) such that

 A27: x = y & y in s and

 A28: ( ord y) <= i by A15;

 ( ord y) <= (i + 1) by A28, NAT_1: 12;

 hence x in sB by A27;

 end;

 (f . (i + 1)) = <%( 1_ F_Complex )%> by A3, A18, A22;



 then (F . (i + 1)) = ( poly_with_roots b) by A20, A19, A21, UPROOTS: 32

 .= ( poly_with_roots B) by A23, TARSKI: 2;

 hence thesis;

 end;

 suppose

 A29: (i + 1) divides n & not (i + 1) divides ni & (i + 1) <> n;

 consider scb be non empty finite Subset of F_Complex such that

 A30: scb = { y where y be Element of cMGFC : ( ord y) = (i + 1) } and

 A31: ( cyclotomic_poly (i + 1)) = ( poly_with_roots ((scb,1) -bag )) by Def5;

 now

 let x be object;

 hereby

 assume x in sB;

 then

 consider y be 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 be 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 be Element of cMGFC such that

 A38: x = y and

 A39: ( ord y) = (i + 1) by A30;

 y in s by A1, A29, A39;

 hence x in sB by A38, A39;

 end;

 end;

 then

 A40: sB = (sb \/ scb) by TARSKI: 2;

 set cb = ((scb,1) -bag );



 A41: sb misses scb

 proof

 assume (sb /\ scb) <> {} ;

 then

 consider x be object such that

 A42: x in (sb /\ scb) by XBOOLE_0:def 1;

 x in scb by A42, XBOOLE_0:def 4;

 then

 A43: ex y2 be Element of cMGFC st x = y2 & ( ord y2) = (i + 1) by A30;

 x in sb by A42, XBOOLE_0:def 4;

 then ex y1 be Element of cMGFC st x = y1 & y1 in s & ( ord y1) <= i by A15;

 hence contradiction by A43, NAT_1: 13;

 end;

 (f . (i + 1)) = ( poly_with_roots cb) by A3, A18, A29, A31;



 then (F . (i + 1)) = (( poly_with_roots b) *' ( poly_with_roots cb)) by A7, A17, A19, A21

 .= ( poly_with_roots (b + cb)) by UPROOTS: 64

 .= ( poly_with_roots B) by A40, A41, UPROOTS: 10;

 hence thesis;

 end;

 end;

 now

 let x be object;

 hereby

 assume

 A44: x in s;

 then

 consider y be 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 be Element of ( MultGroup F_Complex ) st y = x & y in s & ( ord y) <= n;

 hence x in s;

 end;

 then

 A47: s = sB by TARSKI: 2;



 A48: ( 0 + 1) <= n by NAT_1: 13;



 A49: R[1]

 proof

 reconsider t = MG() as finite Subset of F_Complex by A4;

 take t;

 thus t = MG();

 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 be object such that

 A52: x in t;

 consider y be Element of cMGFC such that x = y and

 A53: y in s and

 A54: ( ord y) <= 1 by A52;

 consider y1 be 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 be 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 be 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 be finite Subset of F_Complex st S = MG(len) & (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 :: UNIROOTS:54



 Th54: for n,ni be non zero Element of NAT st ni < n & ni divides n holds ex f be FinSequence of the carrier of ( Polynom-Ring F_Complex ), p be Polynomial of F_Complex st p = ( Product f) & ( dom f) = ( Seg n) & (for i be non zero Element of NAT st i in ( Seg n) holds ( not i divides n or i divides ni or i = n implies (f . i) = <%( 1_ F_Complex )%>) & (i divides n & not i divides ni & i <> n implies (f . i) = ( cyclotomic_poly i))) & ( unital_poly ( F_Complex ,n)) = ((( unital_poly ( F_Complex ,ni)) *' ( cyclotomic_poly n)) *' p)

 proof

 set cMGFC = the carrier of ( MultGroup F_Complex );

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

 let n,ni be non zero Element of NAT such that

 A1: ni < n and

 A2: ni divides n;

 set rbp = { y where y be Element of cMGFC : ( ord y) divides n & not ( ord y) divides ni & ( ord y) <> n };

 rbp c= (n -roots_of_1 )

 proof

 let x be object;

 assume x in rbp;

 then ex y be 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 be non zero Nat st $1 = d & ( not d divides n or d divides ni or d = n implies $2 = <%( 1_ F_Complex )%>) & (d divides n & not d divides ni & d <> n implies $2 = ( cyclotomic_poly d));

 A4:

 now

 let i be Nat;

 assume

 A5: i in ( Seg n);

 then

 A6: i is non zero by FINSEQ_1: 1;

 per cases ;

 suppose

 A7: not i divides n or i divides ni or i = n;

 <%( 1_ F_Complex )%> is Element of cPRFC by POLYNOM3:def 10;

 hence ex x be Element of cPRFC st P[i, x] by A6, A7;

 end;

 suppose

 A8: i divides n & not i divides ni & i <> n;

 reconsider i9 = i as non zero Element of NAT by A5, FINSEQ_1: 1;

 ( cyclotomic_poly i9) is Element of cPRFC by POLYNOM3:def 10;

 hence ex x be Element of cPRFC st P[i, x] by A8;

 end;

 end;

 consider f be FinSequence of cPRFC such that

 A9: ( dom f) = ( Seg n) and

 A10: for i be Nat st i in ( Seg n) holds P[i, (f . i)] from FINSEQ_1:sch 5( A4);

 A11:

 now

 let i be non zero Element of NAT ;

 assume i in ( Seg n);

 then ex d be non zero Nat st i = d & ( not d divides n or d divides ni or d = n implies (f . i) = <%( 1_ F_Complex )%>) & (d divides n & not d divides ni & d <> n implies (f . i) = ( cyclotomic_poly d)) by A10;

 hence ( not i divides n or i divides ni or i = n implies (f . i) = <%( 1_ F_Complex )%>) & (i divides n & not i divides ni & i <> n implies (f . i) = ( cyclotomic_poly i));

 end;

 then ( Product f) = ( poly_with_roots bp) by A9, Th53;

 then

 reconsider p = ( Product f) as Polynomial of F_Complex ;

 take f;

 take p;

 thus p = ( Product f);

 thus ( dom f) = ( Seg n) by A9;

 thus for i be non zero Element of NAT st i in ( Seg n) holds ( not i divides n or i divides ni or i = n implies (f . i) = <%( 1_ F_Complex )%>) & (i divides n & not i divides ni & i <> n implies (f . i) = ( cyclotomic_poly i)) by A11;

 set b = (((n -roots_of_1 ),1) -bag ), bi = (((ni -roots_of_1 ),1) -bag );

 consider rbn be non empty finite Subset of F_Complex such that

 A12: rbn = { y where y be 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 be object such that

 A14: x in ((ni -roots_of_1 ) /\ rbn) by XBOOLE_0:def 1;

 x in rbn by A14, XBOOLE_0:def 4;

 then

 A15: ex y1 be 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 be Element of cMGFC st x = y & ( ord y) divides ni by Th36;

 hence contradiction by A1, A15, NAT_D: 7;

 end;

 then

 A16: (bi + bn) = ((((ni -roots_of_1 ) \/ rbn),1) -bag ) by UPROOTS: 10;

 set rbibn = ((ni -roots_of_1 ) \/ rbn);

 reconsider rbibn as finite Subset of F_Complex ;



 A17: (ni -roots_of_1 ) c= (n -roots_of_1 ) by A2, Th28;

 now

 let x be object;

 hereby

 assume

 A18: x in (n -roots_of_1 );

 then

 reconsider y = x as Element of cMGFC by A3;



 A19: ( ord y) divides n by A18, Th34;

 per cases ;

 suppose ( ord y) = n;

 then y in rbn by A12;

 then y in rbibn by XBOOLE_0:def 3;

 hence x in (rbibn \/ rbp) by XBOOLE_0:def 3;

 end;

 suppose ( ord y) <> n & not ( ord y) divides ni;

 then y in rbp by A19;

 hence x in (rbibn \/ rbp) by XBOOLE_0:def 3;

 end;

 suppose ( ord y) <> n & ( ord y) divides ni;

 then x in (ni -roots_of_1 ) by Th34;

 then x in rbibn by XBOOLE_0:def 3;

 hence x in (rbibn \/ rbp) by XBOOLE_0:def 3;

 end;

 end;

 assume x in (rbibn \/ rbp);

 then

 A20: x in rbibn or x in rbp by XBOOLE_0:def 3;

 per cases by A20, XBOOLE_0:def 3;

 suppose x in (ni -roots_of_1 );

 hence x in (n -roots_of_1 ) by A17;

 end;

 suppose x in rbn;

 then ex y be 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 be Element of cMGFC st x = y & ( ord y) divides n & ( not ( ord y) divides ni) & ( ord y) <> n;

 hence x in (n -roots_of_1 ) by Th34;

 end;

 end;

 then

 A21: (n -roots_of_1 ) = (rbibn \/ rbp) by TARSKI: 2;

 set bibn = ((rbibn,1) -bag );



 A22: ( unital_poly ( F_Complex ,ni)) = ( poly_with_roots bi) by Th46;

 rbibn misses rbp

 proof

 assume (rbibn /\ rbp) <> {} ;

 then

 consider x be object such that

 A23: x in (rbibn /\ rbp) by XBOOLE_0:def 1;

 x in rbp by A23, XBOOLE_0:def 4;

 then

 A24: ex y be 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 be Element of cMGFC st x = y & ( ord y) divides ni by Th36;

 hence contradiction by A24;

 end;

 suppose x in rbn;

 then ex y be 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 :: UNIROOTS:55



 Th55: for i be Integer, c be Element of F_Complex , f be FinSequence of the carrier of ( Polynom-Ring F_Complex ), p be Polynomial of F_Complex st p = ( Product f) & c = i & for i be non zero Element of NAT st i in ( dom f) holds (f . i) = <%( 1_ F_Complex )%> or (f . i) = ( cyclotomic_poly i) holds ( eval (p,c)) is integer

 proof



 A1: ( 1_. F_Complex ) = (( 1_ F_Complex ) * ( 1_. F_Complex )) by POLYNOM5: 27

 .= <%( 1_ F_Complex )%> by POLYNOM5: 29;

 let i be Integer, c be Element of F_Complex , f be FinSequence of the carrier of ( Polynom-Ring F_Complex ), p be Polynomial of F_Complex such that

 A2: p = ( Product f) and

 A3: c = i and

 A4: for i be non zero Element of NAT st i in ( dom f) holds (f . i) = <%( 1_ F_Complex )%> or (f . i) = ( cyclotomic_poly i);



 A5: ( eval (( 1_. F_Complex ),c)) = 1 by COMPLFLD: 8, POLYNOM4: 18;

 per cases ;

 suppose ( len f) = 0 ;

 then f = ( <*> the carrier of ( Polynom-Ring F_Complex ));



 then p = ( 1_ ( Polynom-Ring F_Complex )) by A2, GROUP_4: 8

 .= ( 1. ( Polynom-Ring F_Complex ));

 hence thesis by A5, POLYNOM3:def 10;

 end;

 suppose

 A6: 0 < ( len f);

 defpred P[ Nat, set] means for fi be 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 be FinSequence of the carrier of ( Polynom-Ring F_Complex ) such that ( dom F) = ( Seg ( len f)) and

 A9: for i be Nat st i in ( Seg ( len f)) holds P[i, (F . i)] from FINSEQ_1:sch 5( A8);

 defpred R[ Nat] means ex r be Polynomial of F_Complex st r = (F . $1) & ( eval (r,c)) is integer;

 A10:

 now

 let i be Element of NAT such that

 A11: 1 <= i and

 A12: i < ( len f);



 A13: i in ( Seg ( len f)) by A11, A12, FINSEQ_1: 1;

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



 A14: (i + 1) <= ( len f) by A12, NAT_1: 13;

 then (i + 1) = ( min ((i + 1),( len f))) by XXREAL_0:def 9;

 then

 A15: ( len fi1) = (i + 1) by FINSEQ_2: 21;

 1 <= (i + 1) by A11, NAT_1: 13;

 then

 A16: (i + 1) in ( Seg ( len f)) by A14, FINSEQ_1: 1;

 then

 A17: (i + 1) in ( dom f) by FINSEQ_1:def 3;

 reconsider fi = (f | ( Seg i)) as FinSequence of the carrier of ( Polynom-Ring F_Complex ) by FINSEQ_1: 18;

 assume

 A18: R[i];



 A19: ((f | ( Seg (i + 1))) . (i + 1)) = (f . (i + 1)) by FINSEQ_1: 4, FUNCT_1: 49;

 then

 reconsider fi1d1 = (fi1 . (i + 1)) as Element of the carrier of ( Polynom-Ring F_Complex ) by A17, FINSEQ_2: 11;

 reconsider pfi1 = ( Product fi1), pfi = ( Product fi) as Polynomial of F_Complex by POLYNOM3:def 10;

 reconsider fi1d1p = fi1d1 as Polynomial of F_Complex by POLYNOM3:def 10;

 fi = (fi1 | ( Seg i)) by Lm2, NAT_1: 12;

 then fi1 = (fi ^ <*fi1d1*>) by A15, FINSEQ_3: 55;

 then

 A20: ( Product fi1) = (( Product fi) * fi1d1) by GROUP_4: 6;

 thus R[(i + 1)]

 proof

 reconsider epfi = ( eval (pfi,c)), efi1d1p = ( eval (fi1d1p,c)) as Element of COMPLEX by COMPLFLD:def 1;

 now

 reconsider i1 = (i + 1) as non zero Element of NAT by ORDINAL1:def 12;

 per cases by A4, A17;

 suppose (f . i1) = <%( 1_ F_Complex )%>;

 hence ( eval (fi1d1p,c)) is integer by A5, A1, FINSEQ_1: 4, FUNCT_1: 49;

 end;

 suppose (f . i1) = ( cyclotomic_poly i1);

 hence ( eval (fi1d1p,c)) is integer by A3, A19, Th52;

 end;

 end;

 then

 reconsider iefi1d1p = efi1d1p as Integer;

 reconsider iepfi = epfi as Integer by A9, A18, A13;

 take pfi1;

 thus pfi1 = (F . (i + 1)) by A9, A16;

 pfi1 = (pfi *' fi1d1p) by A20, POLYNOM3:def 10;



 then ( eval (pfi1,c)) = (( eval (pfi,c)) * ( eval (fi1d1p,c))) by POLYNOM4: 24

 .= (iepfi * iefi1d1p);

 hence thesis;

 end;

 end;



 A21: ( 0 + 1) <= ( len f) by A6, NAT_1: 13;

 then

 A22: 1 in ( Seg ( len f)) by FINSEQ_1: 1;



 A23: R[1]

 proof

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



 A24: 1 in ( dom f) by A22, FINSEQ_1:def 3;

 then

 reconsider fd1 = (f . 1) as Element of the carrier of ( Polynom-Ring F_Complex ) by FINSEQ_2: 11;

 reconsider fd1 as Polynomial of F_Complex by POLYNOM3:def 10;

 take fd1;

 f1 = <*(f . 1)*> by A21, Th1;



 hence fd1 = ( Product f1) by FINSOP_1: 11

 .= (F . 1) by A9, A22;

 per cases by A4, A24;

 suppose (f . 1) = <%( 1_ F_Complex )%>;

 hence thesis by A1, COMPLFLD: 8, POLYNOM4: 18;

 end;

 suppose (f . 1) = ( cyclotomic_poly 1);

 hence thesis by A3, Th52;

 end;

 end;

 for i be Element of NAT st 1 <= i & i <= ( len f) holds R[i] from INT_1:sch 7( A23, A10);

 then ex r be 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 :: UNIROOTS:56



 Th56: for n be non zero Element of NAT , j,k,q be Integer, qc be Element of F_Complex st qc = q & j = ( eval (( cyclotomic_poly n),qc)) & k = ( eval (( unital_poly ( F_Complex ,n)),qc)) holds j divides k

 proof

 let n be non zero Element of NAT , j,k,q be Integer, qc be Element of F_Complex such that

 A1: qc = q and

 A2: j = ( eval (( cyclotomic_poly n),qc)) and

 A3: k = ( eval (( unital_poly ( F_Complex ,n)),qc));

 set jfc = ( eval (( cyclotomic_poly n),qc));

 per cases by NAT_1: 53;

 suppose n = 1;

 hence thesis by A2, A3, Th48;

 end;

 suppose

 A4: n > 1;

 set eup1fc = ( eval (( unital_poly ( F_Complex ,1)),qc));

 reconsider eup1 = eup1fc as Integer by A1, Th47;

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

 A5: p = ( Product f) and

 A6: ( dom f) = ( Seg n) & for i be non zero Element of NAT st i in ( Seg n) holds ( not i divides n or i divides 1 or i = n implies (f . i) = <%( 1_ F_Complex )%>) & (i divides n & not i divides 1 & i <> n implies (f . i) = ( cyclotomic_poly i)) and

 A7: ( unital_poly ( F_Complex ,n)) = ((( unital_poly ( F_Complex ,1)) *' ( cyclotomic_poly n)) *' p) by A4, Th54, NAT_D: 6;

 set epfc = ( eval (p,qc));

 now

 let i be non zero Element of NAT ;

 assume

 A8: i in ( dom f);

 per cases ;

 suppose not i divides n or i divides 1 or i = n;

 hence (f . i) = <%( 1_ F_Complex )%> or (f . i) = ( cyclotomic_poly i) by A6, A8;

 end;

 suppose i divides n & not i divides 1 & i <> n;

 hence (f . i) = <%( 1_ F_Complex )%> or (f . i) = ( cyclotomic_poly i) by A6, A8;

 end;

 end;

 then

 reconsider ep = epfc as Integer by A1, A5, Th55;

 k = (( eval ((( unital_poly ( F_Complex ,1)) *' ( cyclotomic_poly n)),qc)) * epfc) by A3, A7, POLYNOM4: 24;

 then k = ((eup1fc * jfc) * epfc) by POLYNOM4: 24;

 then k = ((eup1 * ep) * j) by A2;

 hence thesis by INT_1:def 3;

 end;

 end;

 theorem :: UNIROOTS:57



 Th57: for n,ni be non zero Element of NAT , q be Integer st ni < n & ni divides n holds for qc be Element of F_Complex st qc = q holds for j,k,l be Integer st j = ( eval (( cyclotomic_poly n),qc)) & k = ( eval (( unital_poly ( F_Complex ,n)),qc)) & l = ( eval (( unital_poly ( F_Complex ,ni)),qc)) holds j divides (k div l)

 proof

 let n,ni be non zero Element of NAT , q be Integer such that

 A1: ni < n & ni divides n;

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

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

 A2: p = ( Product f) and

 A3: ( dom f) = ( Seg n) & for i be non zero Element of NAT st i in ( Seg n) holds ( not i divides n or i divides ni or i = n implies (f . i) = <%( 1_ F_Complex )%>) & (i divides n & not i divides ni & i <> n implies (f . i) = ( cyclotomic_poly i)) and

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

 A5:

 now

 let i be non zero Element of NAT such that

 A6: i in ( dom f);

 per cases ;

 suppose not i divides n or i divides ni or i = n;

 hence (f . i) = <%( 1_ F_Complex )%> or (f . i) = ( cyclotomic_poly i) by A3, A6;

 end;

 suppose i divides n & not i divides ni & i <> n;

 hence (f . i) = <%( 1_ F_Complex )%> or (f . i) = ( cyclotomic_poly i) by A3, A6;

 end;

 end;

 let qc be Element of F_Complex ;

 assume qc = q;

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

 then

 consider m be 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 :: UNIROOTS:58

 for n,q be non zero Element of NAT , qc be Element of F_Complex st qc = q holds for j be Integer st j = ( eval (( cyclotomic_poly n),qc)) holds j divides ((q |^ n) - 1)

 proof

 let n,q be non zero Element of NAT ;

 let qc be Element of F_Complex such that

 A1: qc = q;



 A2: ex y1 be 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 :: UNIROOTS:59

 for n,ni,q be non zero Element of NAT st ni < n & ni divides n holds for qc be Element of F_Complex st qc = q holds for j be Integer st j = ( eval (( cyclotomic_poly n),qc)) holds j divides (((q |^ n) - 1) div ((q |^ ni) - 1))

 proof

 let n,ni,q be non zero Element of NAT such that

 A1: ni < n & ni divides n;

 let qc be Element of F_Complex such that

 A2: qc = q;



 A3: (ex y1 be Element of F_Complex st y1 = q & ( eval (( unital_poly ( F_Complex ,n)),y1)) = ((q |^ n) - 1)) & ex y2 be 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 :: UNIROOTS:60

 for n be non zero Element of NAT st 1 < n holds for q be Element of NAT st 1 < q holds for qc be Element of F_Complex st qc = q holds for i be Integer st i = ( eval (( cyclotomic_poly n),qc)) holds |.i.| > (q - 1)

 proof

 set MGFC = ( MultGroup F_Complex );

 set cMGFC = the carrier of ( MultGroup F_Complex );

 let n be non zero Element of NAT such that

 A1: 1 < n;

 consider S be non empty finite Subset of F_Complex such that

 A2: S = { y where y be 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 be FinSequence such that

 A6: ( len p1) = ( len fs) & for i be Nat st i in ( dom p1) holds (p1 . i) = F(i) from FINSEQ_1:sch 2;



 A7: for i be Element of NAT , c be 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 be 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 be object st x in ( rng p1) holds x in REAL

 proof

 let x be object;

 assume x in ( rng p1);

 then

 consider i be Nat such that

 A10: i in ( dom p1) and

 A11: (p1 . i) = x by FINSEQ_2: 10;

 i in ( dom fs) by A6, A10, FINSEQ_3: 29;

 then (fs /. i) = (( canFS S) . i) by PARTFUN1:def 6;

 then x = F(i) by A7, A10, A11;

 hence thesis by XREAL_0:def 1;

 end;

 then ( rng p1) c= REAL ;

 then

 reconsider ps = p1 as non empty FinSequence of REAL by A6, FINSEQ_1:def 4;

 ( len fs) = ( card S) by FINSEQ_1: 93;

 then

 A12: |.( eval (( cyclotomic_poly n),qc)).| = ( Product ps) by A3, A6, A7, Th3;



 A13: ( rng fs) = S by FUNCT_2:def 3;



 A14: for i be 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 be Element of MGFC st (fs /. i) = y & ( ord y) = n by A2, A13;

 A19:

 now

 assume

 A20: (fs /. i) = [**1, 0 **];

 ( 1_ ( MultGroup F_Complex )) = [**1, 0 **] by Th17, COMPLFLD: 8;

 hence contradiction by A1, A18, A20, GROUP_1: 42;

 end;

 (fs /. i) in (n -roots_of_1 ) by A18, Th34;

 then |.(fs /. i).| = 1 by Th23;

 hence thesis by A4, A16, A19, Th6;

 end;

 reconsider qi = q as Integer;

 (1 + 1) <= qi by A4, INT_1: 7;

 then

 A21: ((1 + 1) + ( - 1)) <= (qi + ( - 1)) by XREAL_1: 7;

 let i be Integer;

 reconsider x = (q - 1) as Real;

 assume i = ( eval (( cyclotomic_poly n),qc));

 then |.i.| > x by A21, A12, A14, Th7;

 hence |.i.| > (q - 1);

 end;