:: UNIROOTS semantic presentation begin Lm1: for k being Element of NAT holds ( not k is empty iff 1 <= k ) proof let k be Element of NAT ; ::_thesis: ( not k is empty iff 1 <= k ) hereby ::_thesis: ( 1 <= k implies not k is empty ) assume not k is empty ; ::_thesis: 1 <= k then 0 + 1 <= k by NAT_1:13; hence 1 <= k ; ::_thesis: verum end; assume 1 <= k ; ::_thesis: not k is empty hence not k is empty ; ::_thesis: verum end; scheme :: UNIROOTS:sch 1 CompIndNE{ P1[ non empty Nat] } : for k being non empty Element of NAT holds P1[k] provided A1: for k being non empty Element of NAT st ( for n being non empty Element of NAT st n < k holds P1[n] ) holds P1[k] proof let k be non empty Element of NAT ; ::_thesis: P1[k] defpred S1[ Nat] means ex m being non empty Element of NAT st ( m = $1 & P1[m] ); A2: now__::_thesis:_for_k_being_Nat_st_k_>=_1_&_(_for_n_being_Nat_st_n_>=_1_&_n_<_k_holds_ S1[n]_)_holds_ S1[k] let k be Nat; ::_thesis: ( k >= 1 & ( for n being Nat st n >= 1 & n < k holds S1[n] ) implies S1[k] ) assume that A3: k >= 1 and A4: for n being Nat st n >= 1 & n < k holds S1[n] ; ::_thesis: S1[k] reconsider m = k as non empty Element of NAT by A3, ORDINAL1:def_12; now__::_thesis:_for_n_being_non_empty_Element_of_NAT_st_n_<_m_holds_ P1[n] let n be non empty Element of NAT ; ::_thesis: ( n < m implies P1[n] ) assume A5: n < m ; ::_thesis: P1[n] n >= 1 by Lm1; then S1[n] by A4, A5; hence P1[n] ; ::_thesis: verum end; then P1[m] by A1; hence S1[k] ; ::_thesis: verum end; A6: for k being Nat st k >= 1 holds S1[k] from NAT_1:sch_9(A2); k >= 1 by Lm1; then ex m being non empty Element of NAT st ( m = k & P1[m] ) by A6; hence P1[k] ; ::_thesis: verum end; theorem Th1: :: UNIROOTS:1 for f being FinSequence st 1 <= len f holds f | (Seg 1) = <*(f . 1)*> proof let f be FinSequence; ::_thesis: ( 1 <= len f implies f | (Seg 1) = <*(f . 1)*> ) assume 1 <= len f ; ::_thesis: f | (Seg 1) = <*(f . 1)*> 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 f | (Seg 1) = <*(f . 1)*> by A2, FINSEQ_1:40; ::_thesis: verum end; Lm2: for f being FinSequence for n, i being Element of NAT st i <= n holds (f | (Seg n)) | (Seg i) = f | (Seg i) proof let f be FinSequence; ::_thesis: for n, i being Element of NAT st i <= n holds (f | (Seg n)) | (Seg i) = f | (Seg i) let n, i be Element of NAT ; ::_thesis: ( i <= n implies (f | (Seg n)) | (Seg i) = f | (Seg i) ) assume i <= n ; ::_thesis: (f | (Seg n)) | (Seg i) = f | (Seg i) then Seg i c= Seg n by FINSEQ_1:5; hence (f | (Seg n)) | (Seg i) = f | (Seg i) by RELAT_1:74; ::_thesis: verum end; theorem Th2: :: UNIROOTS:2 for f being FinSequence of F_Complex for g being FinSequence of REAL st len f = len g & ( for i being Element of NAT st i in dom f holds |.(f /. i).| = g . i ) holds |.(Product f).| = Product g proof defpred S1[ Element of NAT ] means for f being FinSequence of F_Complex for g being FinSequence of REAL st len f = len g & ( for i being Element of NAT st i in dom f holds |.(f /. i).| = g . i ) & $1 = len f holds |.(Product f).| = Product g; set cFC = the carrier of F_Complex; set FC = F_Complex ; A1: for i being Element of NAT st S1[i] holds S1[i + 1] proof let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] ) assume A2: S1[i] ; ::_thesis: S1[i + 1] let f be FinSequence of F_Complex; ::_thesis: for g being FinSequence of REAL st len f = len g & ( for i being Element of NAT st i in dom f holds |.(f /. i).| = g . i ) & i + 1 = len f holds |.(Product f).| = Product g let g be FinSequence of REAL ; ::_thesis: ( len f = len g & ( for i being Element of NAT st i in dom f holds |.(f /. i).| = g . i ) & i + 1 = len f implies |.(Product f).| = Product g ) assume that A3: len f = len g and A4: for i being Element of NAT st i in dom f holds |.(f /. i).| = g . i and A5: i + 1 = len f ; ::_thesis: |.(Product f).| = Product g consider g1 being FinSequence of REAL , r being Real such that A6: g = g1 ^ <*r*> by A3, A5, FINSEQ_2:19; A7: len g = (len g1) + (len <*r*>) by A6, FINSEQ_1:22 .= (len g1) + 1 by FINSEQ_1:39 ; then A8: g . (len f) = r by A3, A6, FINSEQ_1:42; consider f1 being FinSequence of F_Complex, c being Element of the carrier of F_Complex 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__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_f1_holds_ |.(f1_/._i).|_=_g1_._i let i be Element of NAT ; ::_thesis: ( i in dom f1 implies |.(f1 /. i).| = g1 . i ) A13: dom f1 c= dom f by A9, FINSEQ_1:26; assume A14: i in dom f1 ; ::_thesis: |.(f1 /. i).| = g1 . i 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 ; ::_thesis: verum 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 ; ::_thesis: verum end; A18: S1[ 0 ] proof let f be FinSequence of F_Complex; ::_thesis: for g being FinSequence of REAL st len f = len g & ( for i being Element of NAT st i in dom f holds |.(f /. i).| = g . i ) & 0 = len f holds |.(Product f).| = Product g let g be FinSequence of REAL ; ::_thesis: ( len f = len g & ( for i being Element of NAT st i in dom f holds |.(f /. i).| = g . i ) & 0 = len f implies |.(Product f).| = Product g ) assume that A19: len f = len g and for i being Element of NAT st i in dom f holds |.(f /. i).| = g . i and A20: 0 = len f ; ::_thesis: |.(Product f).| = Product g 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 |.(Product f).| = Product g by A22, COMPLEX1:48, RVSUM_1:94; ::_thesis: verum end; A23: for i being Element of NAT holds S1[i] from NAT_1:sch_1(A18, A1); let f be FinSequence of F_Complex; ::_thesis: for g being FinSequence of REAL st len f = len g & ( for i being Element of NAT st i in dom f holds |.(f /. i).| = g . i ) holds |.(Product f).| = Product g let g be FinSequence of REAL ; ::_thesis: ( len f = len g & ( for i being Element of NAT st i in dom f holds |.(f /. i).| = g . i ) implies |.(Product f).| = Product g ) assume ( len f = len g & ( for i being Element of NAT st i in dom f holds |.(f /. i).| = g . i ) ) ; ::_thesis: |.(Product f).| = Product g hence |.(Product f).| = Product g by A23; ::_thesis: verum end; theorem Th3: :: UNIROOTS:3 for s being non empty finite Subset of F_Complex for x being Element of F_Complex for r being FinSequence of REAL st len r = card s & ( for i being Element of NAT for c being Element of F_Complex st i in dom r & c = (canFS s) . i holds r . i = |.(x - c).| ) holds |.(eval ((poly_with_roots ((s,1) -bag)),x)).| = Product r proof set FC = F_Complex ; let s be non empty finite Subset of F_Complex; ::_thesis: for x being Element of F_Complex for r being FinSequence of REAL st len r = card s & ( for i being Element of NAT for c being Element of F_Complex st i in dom r & c = (canFS s) . i holds r . i = |.(x - c).| ) holds |.(eval ((poly_with_roots ((s,1) -bag)),x)).| = Product r let x be Element of F_Complex; ::_thesis: for r being FinSequence of REAL st len r = card s & ( for i being Element of NAT for c being Element of F_Complex st i in dom r & c = (canFS s) . i holds r . i = |.(x - c).| ) holds |.(eval ((poly_with_roots ((s,1) -bag)),x)).| = Product r let r be FinSequence of REAL ; ::_thesis: ( len r = card s & ( for i being Element of NAT for c being Element of F_Complex st i in dom r & c = (canFS s) . i holds r . i = |.(x - c).| ) implies |.(eval ((poly_with_roots ((s,1) -bag)),x)).| = Product r ) assume that A1: len r = card s and A2: for i being Element of NAT for c being Element of F_Complex st i in dom r & c = (canFS s) . i holds r . i = |.(x - c).| ; ::_thesis: |.(eval ((poly_with_roots ((s,1) -bag)),x)).| = Product r defpred S1[ set , set ] means ex c being Element of F_Complex st ( c = (canFS s) . $1 & $2 = eval (<%(- c),(1_ F_Complex)%>,x) ); len (canFS s) = card s by UPROOTS:3; then A3: dom (canFS s) = Seg (card s) by FINSEQ_1:def_3; A4: for k being Element of NAT st k in Seg (card s) holds ex y being Element of F_Complex st S1[k,y] proof let k be Element of NAT ; ::_thesis: ( k in Seg (card s) implies ex y being Element of F_Complex st S1[k,y] ) assume A5: k in Seg (card s) ; ::_thesis: ex y being Element of F_Complex st S1[k,y] set c = (canFS s) . k; (canFS s) . k in s by A3, A5, FINSEQ_2:11; then reconsider c = (canFS s) . k as Element of F_Complex ; reconsider fi = eval (<%(- c),(1_ F_Complex)%>,x) as Element of F_Complex ; take fi ; ::_thesis: S1[k,fi] take c ; ::_thesis: ( c = (canFS s) . k & fi = eval (<%(- c),(1_ F_Complex)%>,x) ) thus ( c = (canFS s) . k & fi = eval (<%(- c),(1_ F_Complex)%>,x) ) ; ::_thesis: verum end; consider f being FinSequence of F_Complex such that A6: dom f = Seg (card s) and A7: for k being Element of NAT st k in Seg (card s) holds S1[k,f /. k] from RECDEF_1:sch_17(A4); A8: now__::_thesis:_for_i_being_Element_of_NAT_ for_c_being_Element_of_F_Complex_st_i_in_dom_f_&_c_=_(canFS_s)_._i_holds_ f_._i_=_eval_(<%(-_c),(1__F_Complex)%>,x) let i be Element of NAT ; ::_thesis: for c being Element of F_Complex st i in dom f & c = (canFS s) . i holds f . i = eval (<%(- c),(1_ F_Complex)%>,x) let c be Element of F_Complex; ::_thesis: ( i in dom f & c = (canFS s) . i implies f . i = eval (<%(- c),(1_ F_Complex)%>,x) ) assume that A9: i in dom f and A10: c = (canFS s) . i ; ::_thesis: f . i = eval (<%(- c),(1_ F_Complex)%>,x) ex c1 being Element of F_Complex 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; ::_thesis: verum end; A11: dom r = Seg (card s) by A1, FINSEQ_1:def_3; A12: for i being Element of NAT st i in dom f holds |.(f /. i).| = r . i proof let i be Element of NAT ; ::_thesis: ( i in dom f implies |.(f /. i).| = r . i ) set c = (canFS s) . i; assume A13: i in dom f ; ::_thesis: |.(f /. i).| = r . i then (canFS s) . i in s by A3, A6, FINSEQ_2:11; then reconsider c = (canFS s) . i as Element of F_Complex ; 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 |.(f /. i).| = r . i by A2, A11, A6, A13; ::_thesis: verum 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 |.(eval ((poly_with_roots ((s,1) -bag)),x)).| = Product r by A15, A12, Th2; ::_thesis: verum end; theorem Th4: :: UNIROOTS:4 for f being FinSequence of F_Complex st ( for i being Element of NAT st i in dom f holds f . i is integer ) holds Sum f is integer proof set FC = F_Complex ; let f be FinSequence of F_Complex; ::_thesis: ( ( for i being Element of NAT st i in dom f holds f . i is integer ) implies Sum f is integer ) assume A1: for i being Element of NAT st i in dom f holds f . i is integer ; ::_thesis: Sum f is integer defpred S1[ Element of NAT ] means for f being FinSequence of F_Complex st len f = $1 & ( for i being Element of NAT st i in dom f holds f . i is integer ) holds Sum f is integer ; A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A3: S1[n] ; ::_thesis: S1[n + 1] let f be FinSequence of F_Complex; ::_thesis: ( len f = n + 1 & ( for i being Element of NAT st i in dom f holds f . i is integer ) implies Sum f is integer ) assume that A4: len f = n + 1 and A5: for i being Element of NAT st i in dom f holds f . i is integer ; ::_thesis: Sum f is integer consider g being FinSequence of F_Complex, c being Element of F_Complex such that A6: f = g ^ <*c*> by A4, FINSEQ_2:19; A7: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_g_holds_ g_._i_is_integer let i be Element of NAT ; ::_thesis: ( i in dom g implies g . i is integer ) A8: dom g c= dom f by A6, FINSEQ_1:26; assume A9: i in dom g ; ::_thesis: g . i is integer then f . i = g . i by A6, FINSEQ_1:def_7; hence g . i is integer by A5, A9, A8; ::_thesis: verum 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 Sum f is integer ; ::_thesis: verum end; A11: len f is Element of NAT ; A12: S1[ 0 ] proof let f be FinSequence of F_Complex; ::_thesis: ( len f = 0 & ( for i being Element of NAT st i in dom f holds f . i is integer ) implies Sum f is integer ) assume len f = 0 ; ::_thesis: ( ex i being Element of NAT st ( i in dom f & not f . i is integer ) or Sum f is integer ) then f = <*> the carrier of F_Complex ; hence ( ex i being Element of NAT st ( i in dom f & not f . i is integer ) or Sum f is integer ) by COMPLFLD:7, RLVECT_1:43; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A12, A2); hence Sum f is integer by A1, A11; ::_thesis: verum end; theorem :: UNIROOTS:5 for x, y being Element of F_Complex for r1, r2 being Real st r1 = x & r2 = y holds ( r1 * r2 = x * y & r1 + r2 = x + y ) ; theorem Th6: :: UNIROOTS:6 for q being Real st q > 0 holds for r being Element of F_Complex st |.r.| = 1 & r <> [**1,0**] holds |.([**q,0**] - r).| > q - 1 proof let q be Real; ::_thesis: ( q > 0 implies for r being Element of F_Complex st |.r.| = 1 & r <> [**1,0**] holds |.([**q,0**] - r).| > q - 1 ) assume A1: q > 0 ; ::_thesis: for r being Element of F_Complex st |.r.| = 1 & r <> [**1,0**] holds |.([**q,0**] - r).| > q - 1 let r be Element of F_Complex; ::_thesis: ( |.r.| = 1 & r <> [**1,0**] implies |.([**q,0**] - r).| > q - 1 ) assume that A2: |.r.| = 1 and A3: r <> [**1,0**] ; ::_thesis: |.([**q,0**] - r).| > q - 1 set b = Im r; set a = Re r; A4: ((Re r) ^2) + ((Im r) ^2) = 1 ^2 by A2, COMPTRIG:3; A5: now__::_thesis:_not_Re_r_=_1 assume A6: Re r = 1 ; ::_thesis: contradiction then Im r = 0 by A4; hence contradiction by A3, A6, COMPLEX1:13; ::_thesis: verum end; Re r <= 1 by A2, COMPLEX1:54; then Re r < 1 by A5, XXREAL_0:1; then 2 * q > (2 * q) * (Re r) by A1, XREAL_1:157; then - ((2 * q) * (Re r)) > - (2 * q) by XREAL_1:24; then (- (2 * q)) + (q ^2) < (- ((2 * q) * (Re r))) + (q ^2) by XREAL_1:8; then A7: ((q ^2) - ((2 * q) * (Re r))) + 1 > ((q ^2) - (2 * q)) + 1 by XREAL_1:8; reconsider qc = [**q,0**] as Element of F_Complex ; A8: ( Re [**(q - (Re r)),(- (Im r))**] = q - (Re r) & Im [**(q - (Re r)),(- (Im r))**] = - (Im r) ) by COMPLEX1:12; |.(qc - r).| ^2 = |.([**q,0**] - [**(Re r),(Im r)**]).| ^2 by COMPLEX1:13 .= |.[**(q - (Re r)),(0 - (Im r))**].| ^2 by POLYNOM5:6 .= ((q - (Re r)) ^2) + ((Im r) ^2) by A8, COMPTRIG:3 .= ((q ^2) - ((2 * q) * (Re r))) + 1 by A4 ; then ( |.(qc - r).| >= 0 & |.(qc - r).| ^2 > (q - 1) ^2 ) by A7, COMPLEX1:46; hence |.([**q,0**] - r).| > q - 1 by SQUARE_1:48; ::_thesis: verum end; theorem Th7: :: UNIROOTS:7 for ps being non empty FinSequence of REAL for x being Real st x >= 1 & ( for i being Element of NAT st i in dom ps holds ps . i > x ) holds Product ps > x proof let ps be non empty FinSequence of REAL ; ::_thesis: for x being Real st x >= 1 & ( for i being Element of NAT st i in dom ps holds ps . i > x ) holds Product ps > x let x be Real; ::_thesis: ( x >= 1 & ( for i being Element of NAT st i in dom ps holds ps . i > x ) implies Product ps > x ) assume that A1: x >= 1 and A2: for j being Element of NAT st j in dom ps holds ps . j > x ; ::_thesis: Product ps > x consider ps1 being FinSequence, y being set such that A3: ps = ps1 ^ <*y*> by FINSEQ_1:46; <*y*> is FinSequence of REAL by A3, FINSEQ_1:36; then rng <*y*> c= REAL by FINSEQ_1:def_4; then {y} c= REAL by FINSEQ_1:38; then reconsider y2 = y as Real by ZFMISC_1:31; defpred S1[ Element of NAT ] means for f being FinSequence of REAL st len f = $1 & ( for j being Element of NAT st j in dom f holds f . j > x ) holds (Product f) * y2 > x; A4: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A5: S1[k] ; ::_thesis: S1[k + 1] let f be FinSequence of REAL ; ::_thesis: ( len f = k + 1 & ( for j being Element of NAT st j in dom f holds f . j > x ) implies (Product f) * y2 > x ) assume that A6: len f = k + 1 and A7: for j being Element of NAT st j in dom f holds f . j > x ; ::_thesis: (Product f) * y2 > x f <> {} by A6; then consider v being FinSequence, w being set such that A8: f = v ^ <*w*> by FINSEQ_1:46; reconsider f1 = v, f2 = <*w*> as FinSequence of REAL by A8, FINSEQ_1:36; rng f2 c= REAL ; then {w} c= REAL by FINSEQ_1:38; then reconsider m = w as Real by ZFMISC_1:31; k + 1 = (len f1) + (len f2) by A6, A8, FINSEQ_1:22; then A9: k + 1 = (len f1) + 1 by FINSEQ_1:39; then A10: f . (len f) = m by A6, A8, FINSEQ_1:42; len f in Seg (len f) by A6, FINSEQ_1:3; then A11: len f in dom f by FINSEQ_1:def_3; then m > 1 by A1, A7, A10, XXREAL_0:2; then A12: x * m > x by A1, XREAL_1:155; A13: for j being Element of NAT st j in dom f1 holds f1 . j > x proof A14: dom f1 c= dom f by A8, FINSEQ_1:26; let j be Element of NAT ; ::_thesis: ( j in dom f1 implies f1 . j > x ) assume A15: j in dom f1 ; ::_thesis: f1 . j > x f . j = f1 . j by A8, A15, FINSEQ_1:def_7; hence f1 . j > x by A7, A15, A14; ::_thesis: verum 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 (Product f) * y2 > x by A12, XXREAL_0:2; ::_thesis: verum end; len ps in Seg (len ps) by FINSEQ_1:3; then A17: len ps in dom ps by FINSEQ_1:def_3; reconsider q = ps1 as FinSequence of REAL by A3, FINSEQ_1:36; A18: for j being Element of NAT st j in dom q holds q . j > x proof A19: dom q c= dom ps by A3, FINSEQ_1:26; let j be Element of NAT ; ::_thesis: ( j in dom q implies q . j > x ) assume A20: j in dom q ; ::_thesis: q . j > x ps . j = q . j by A3, A20, FINSEQ_1:def_7; hence q . j > x by A2, A20, A19; ::_thesis: verum 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: S1[ 0 ] proof let f be FinSequence of REAL ; ::_thesis: ( len f = 0 & ( for j being Element of NAT st j in dom f holds f . j > x ) implies (Product f) * y2 > x ) assume that A24: len f = 0 and for j being Element of NAT st j in dom f holds f . j > x ; ::_thesis: (Product f) * y2 > x f = <*> REAL by A24; then Product f = 1 by RVSUM_1:94; hence (Product f) * y2 > x by A2, A22, A17; ::_thesis: verum end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A23, A4); then (Product q) * y2 > x by A18, A21; hence Product ps > x by A3, RVSUM_1:96; ::_thesis: verum end; theorem Th8: :: UNIROOTS:8 for n being Element of NAT holds 1_ F_Complex = (power F_Complex) . ((1_ F_Complex),n) proof let n be Element of NAT ; ::_thesis: 1_ F_Complex = (power F_Complex) . ((1_ F_Complex),n) 1_ F_Complex = [**1,0**] by COMPLFLD:8; then (power F_Complex) . ((1_ F_Complex),n) = [**(1 to_power n),0**] by HAHNBAN1:29 .= 1_ F_Complex by COMPLFLD:8, POWER:26 ; hence 1_ F_Complex = (power F_Complex) . ((1_ F_Complex),n) ; ::_thesis: verum end; theorem Th9: :: UNIROOTS:9 for n, i being Element of NAT holds ( cos (((2 * PI) * i) / n) = cos (((2 * PI) * (i mod n)) / n) & sin (((2 * PI) * i) / n) = sin (((2 * PI) * (i mod n)) / n) ) proof let n, i be Element of NAT ; ::_thesis: ( cos (((2 * PI) * i) / n) = cos (((2 * PI) * (i mod n)) / n) & sin (((2 * PI) * i) / n) = sin (((2 * PI) * (i mod n)) / n) ) set j = i div n; percases ( n <> 0 or n = 0 ) ; supposeA1: n <> 0 ; ::_thesis: ( cos (((2 * PI) * i) / n) = cos (((2 * PI) * (i mod n)) / n) & sin (((2 * PI) * i) / n) = sin (((2 * PI) * (i mod n)) / n) ) then i = (n * (i div n)) + (i mod n) by NAT_D:2; then A2: ((2 * PI) * i) / n = (((2 * PI) * (n * (i div n))) + ((2 * PI) * (i mod n))) / n .= (((2 * PI) * (n * (i div n))) / (n * 1)) + (((2 * PI) * (i mod n)) / n) by XCMPLX_1:62 .= ((((2 * PI) / n) * (n * (i div n))) / 1) + (((2 * PI) * (i mod n)) / n) by XCMPLX_1:83 .= (((2 * PI) * (1 / n)) * (n * (i div n))) + (((2 * PI) * (i mod n)) / n) by XCMPLX_1:99 .= ((2 * PI) * ((1 / n) * ((i div n) * n))) + (((2 * PI) * (i mod n)) / n) .= ((2 * PI) * ((i div n) * 1)) + (((2 * PI) * (i mod n)) / n) by A1, XCMPLX_1:90 .= ((2 * PI) * (i div n)) + (((2 * PI) * (i mod n)) / n) ; then A3: sin (((2 * PI) * i) / n) = ((sin (((2 * PI) * (i div n)) + 0)) * (cos (((2 * PI) * (i mod n)) / n))) + ((cos (((2 * PI) * (i div n)) + 0)) * (sin (((2 * PI) * (i mod n)) / n))) by SIN_COS:75 .= ((sin . (((2 * PI) * (i div n)) + 0)) * (cos (((2 * PI) * (i mod n)) / n))) + ((cos (((2 * PI) * (i div n)) + 0)) * (sin (((2 * PI) * (i mod n)) / n))) by SIN_COS:def_17 .= ((sin . (((2 * PI) * (i div n)) + 0)) * (cos (((2 * PI) * (i mod n)) / n))) + ((cos . (((2 * PI) * (i div n)) + 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) * (i div n)) + 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) * (i div n)) + 0)) * (cos (((2 * PI) * (i mod n)) / n))) - ((sin (((2 * PI) * (i div n)) + 0)) * (sin (((2 * PI) * (i mod n)) / n))) by A2, SIN_COS:75 .= ((cos . (((2 * PI) * (i div n)) + 0)) * (cos (((2 * PI) * (i mod n)) / n))) - ((sin (((2 * PI) * (i div n)) + 0)) * (sin (((2 * PI) * (i mod n)) / n))) by SIN_COS:def_19 .= ((cos . (((2 * PI) * (i div n)) + 0)) * (cos (((2 * PI) * (i mod n)) / n))) - ((sin . (((2 * PI) * (i div n)) + 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) * (i div n)) + 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 ( cos (((2 * PI) * i) / n) = cos (((2 * PI) * (i mod n)) / n) & sin (((2 * PI) * i) / n) = sin (((2 * PI) * (i mod n)) / n) ) by A3; ::_thesis: verum end; supposeA4: n = 0 ; ::_thesis: ( cos (((2 * PI) * i) / n) = cos (((2 * PI) * (i mod n)) / n) & sin (((2 * PI) * i) / n) = sin (((2 * PI) * (i mod n)) / n) ) then ((2 * PI) * i) / n = 0 by XCMPLX_1:49; hence ( cos (((2 * PI) * i) / n) = cos (((2 * PI) * (i mod n)) / n) & sin (((2 * PI) * i) / n) = sin (((2 * PI) * (i mod n)) / n) ) by A4, XCMPLX_1:49; ::_thesis: verum end; end; end; theorem Th10: :: UNIROOTS:10 for n, i being Element of NAT holds [**(cos (((2 * PI) * i) / n)),(sin (((2 * PI) * i) / n))**] = [**(cos (((2 * PI) * (i mod n)) / n)),(sin (((2 * PI) * (i mod n)) / n))**] proof let n, i be Element of NAT ; ::_thesis: [**(cos (((2 * PI) * i) / n)),(sin (((2 * PI) * i) / n))**] = [**(cos (((2 * PI) * (i mod n)) / n)),(sin (((2 * PI) * (i mod n)) / n))**] [**(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 [**(cos (((2 * PI) * i) / n)),(sin (((2 * PI) * i) / n))**] = [**(cos (((2 * PI) * (i mod n)) / n)),(sin (((2 * PI) * (i mod n)) / n))**] ; ::_thesis: verum end; theorem Th11: :: UNIROOTS:11 for n, i, j being Element of NAT holds [**(cos (((2 * PI) * i) / n)),(sin (((2 * PI) * i) / n))**] * [**(cos (((2 * PI) * j) / n)),(sin (((2 * PI) * j) / n))**] = [**(cos (((2 * PI) * ((i + j) mod n)) / n)),(sin (((2 * PI) * ((i + j) mod n)) / n))**] proof let n, i, j be Element of NAT ; ::_thesis: [**(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))**] (((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 [**(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))**] ; ::_thesis: verum end; theorem Th12: :: UNIROOTS:12 for L being non empty unital associative multMagma for x being Element of L for n, m being Element of NAT holds (power L) . (x,(n * m)) = (power L) . (((power L) . (x,n)),m) proof let L be non empty unital associative multMagma ; ::_thesis: for x being Element of L for n, m being Element of NAT holds (power L) . (x,(n * m)) = (power L) . (((power L) . (x,n)),m) let x be Element of L; ::_thesis: for n, m being Element of NAT holds (power L) . (x,(n * m)) = (power L) . (((power L) . (x,n)),m) let n be Element of NAT ; ::_thesis: for m being Element of NAT holds (power L) . (x,(n * m)) = (power L) . (((power L) . (x,n)),m) defpred S1[ Element of NAT ] means (power L) . (x,(n * $1)) = (power L) . (((power L) . (x,n)),$1); set pL = power L; A1: for m being Element of NAT st S1[m] holds S1[m + 1] proof let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] ) assume A2: S1[m] ; ::_thesis: S1[m + 1] thus (power L) . (x,(n * (m + 1))) = (power L) . (x,((n * m) + (n * 1))) .= ((power L) . (x,(n * m))) * ((power L) . (x,n)) by POLYNOM2:1 .= (power L) . (((power L) . (x,n)),(m + 1)) by A2, GROUP_1:def_7 ; ::_thesis: verum end; (power L) . (x,(n * 0)) = 1_ L by GROUP_1:def_7 .= (power L) . (((power L) . (x,n)),0) by GROUP_1:def_7 ; then A3: S1[ 0 ] ; thus for m being Element of NAT holds S1[m] from NAT_1:sch_1(A3, A1); ::_thesis: verum end; theorem Th13: :: UNIROOTS:13 for n being Element of NAT for x being Element of F_Complex st x is Integer holds (power F_Complex) . (x,n) is Integer proof let n be Element of NAT ; ::_thesis: for x being Element of F_Complex st x is Integer holds (power F_Complex) . (x,n) is Integer let x be Element of F_Complex; ::_thesis: ( x is Integer implies (power F_Complex) . (x,n) is Integer ) assume A1: x is Integer ; ::_thesis: (power F_Complex) . (x,n) is Integer defpred S1[ Element of NAT ] means (power F_Complex) . (x,$1) is Integer; A2: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] reconsider i1 = x as Integer by A1; let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume S1[k] ; ::_thesis: S1[k + 1] then reconsider i2 = (power F_Complex) . (x,k) as Integer ; ((power F_Complex) . (x,k)) * x = i1 * i2 ; hence S1[k + 1] by GROUP_1:def_7; ::_thesis: verum end; A3: S1[ 0 ] by COMPLFLD:8, GROUP_1:def_7; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A3, A2); hence (power F_Complex) . (x,n) is Integer ; ::_thesis: verum end; theorem Th14: :: UNIROOTS:14 for F being FinSequence of F_Complex st ( for i being Element of NAT st i in dom F holds F . i is Integer ) holds Sum F is Integer proof defpred S1[ Element of NAT ] means for F being FinSequence of F_Complex st len F = $1 & ( for i being Element of NAT st i in dom F holds F . i is Integer ) holds Sum F is Integer; let G be FinSequence of F_Complex; ::_thesis: ( ( for i being Element of NAT st i in dom G holds G . i is Integer ) implies Sum G is Integer ) assume A1: for i being Element of NAT st i in dom G holds G . i is Integer ; ::_thesis: Sum G is Integer A2: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: S1[k] ; ::_thesis: S1[k + 1] let F be FinSequence of F_Complex; ::_thesis: ( len F = k + 1 & ( for i being Element of NAT st i in dom F holds F . i is Integer ) implies Sum F is Integer ) assume that A4: len F = k + 1 and A5: for i being Element of NAT st i in dom F holds F . i is Integer ; ::_thesis: Sum F is Integer F <> {} by A4; then consider G being FinSequence, x being set such that A6: F = G ^ <*x*> by FINSEQ_1:46; len F in Seg (len F) by A4, FINSEQ_1:3; then A7: len F in dom F by FINSEQ_1:def_3; reconsider f2 = <*x*> as FinSequence of F_Complex by A6, FINSEQ_1:36; reconsider f1 = G as FinSequence of F_Complex by A6, FINSEQ_1:36; rng f2 c= the carrier of F_Complex by FINSEQ_1:def_4; then {x} c= the carrier of F_Complex by FINSEQ_1:38; then reconsider m = x as Element of F_Complex by ZFMISC_1:31; k + 1 = (len f1) + (len f2) by A4, A6, FINSEQ_1:22; then A8: k + 1 = (len f1) + 1 by FINSEQ_1:39; then F . (len F) = m by A4, A6, FINSEQ_1:42; then reconsider i2 = m as Integer by A5, A7; for j being Element of NAT st j in dom f1 holds f1 . j is Integer proof A9: dom f1 c= dom F by A6, FINSEQ_1:26; let j be Element of NAT ; ::_thesis: ( j in dom f1 implies f1 . j is Integer ) assume A10: j in dom f1 ; ::_thesis: f1 . j is Integer F . j = f1 . j by A6, A10, FINSEQ_1:def_7; hence f1 . j is Integer by A5, A10, A9; ::_thesis: verum 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 Sum F is Integer ; ::_thesis: verum end; A11: S1[ 0 ] proof let F be FinSequence of F_Complex; ::_thesis: ( len F = 0 & ( for i being Element of NAT st i in dom F holds F . i is Integer ) implies Sum F is Integer ) assume that A12: len F = 0 and for i being Element of NAT st i in dom F holds F . i is Integer ; ::_thesis: Sum F 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 Sum F is Integer by COMPLFLD:7, FVSUM_1:74; ::_thesis: verum end; A13: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A11, A2); len G = len G ; hence Sum G is Integer by A1, A13; ::_thesis: verum end; Lm3: Z_3 is finite by MOD_2:def_20; registration cluster non empty non degenerated non trivial finite right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital V175() left_unital V185() V186() V187() domRing-like for doubleLoopStr ; existence ex b1 being Field st b1 is finite by Lm3, MOD_2:27; cluster non empty non degenerated non trivial finite right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital V175() left_unital V185() V186() V187() for doubleLoopStr ; existence ex b1 being Skew-Field st b1 is finite by Lm3, MOD_2:27; end; begin definition let R be Skew-Field; func MultGroup R -> strict Group means :Def1: :: UNIROOTS:def 1 ( the carrier of it = NonZero R & the multF of it = the multF of R || the carrier of it ); existence ex b1 being strict Group st ( the carrier of b1 = NonZero R & the multF of b1 = the multF of R || the carrier of b1 ) proof set ccs = NonZero R; set cR = the carrier of R; reconsider ccs = NonZero R as non empty set ; set mcs = the multF of R || ccs; [:ccs,ccs:] c= [: the carrier of R, the carrier of R:] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:ccs,ccs:] or x in [: the carrier of R, the carrier of R:] ) assume x in [:ccs,ccs:] ; ::_thesis: x in [: the carrier of R, the carrier of R:] then ex a, b being set st ( a in ccs & b in ccs & x = [a,b] ) by ZFMISC_1:def_2; hence x in [: the carrier of R, the carrier of R:] by ZFMISC_1:def_2; ::_thesis: verum end; then reconsider mcs = the multF of R || ccs as Function of [:ccs,ccs:], the carrier of R by FUNCT_2:32; rng mcs c= ccs proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng mcs or y in ccs ) assume y in rng mcs ; ::_thesis: y in ccs then consider x being set such that A1: x in dom mcs and A2: y = mcs . x by FUNCT_1:def_3; A3: dom mcs = [:ccs,ccs:] by FUNCT_2:def_1; then consider a, b being set such that A4: a in ccs and A5: b in ccs and A6: x = [a,b] by A1, ZFMISC_1:def_2; reconsider a = a, b = b as Element of the carrier of R 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 y in ccs by A2, A8, XBOOLE_0:def_5; ::_thesis: verum end; then reconsider mcs = 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__::_thesis:_for_a,_b_being_Element_of_the_carrier_of_R for_c,_d_being_Element_of_the_carrier_of_cs_st_a_=_c_&_b_=_d_holds_ a_*_b_=_c_*_d let a, b be Element of the carrier of R; ::_thesis: for c, d being Element of the carrier of cs st a = c & b = d holds a * b = c * d let c, d be Element of the carrier of cs; ::_thesis: ( a = c & b = d implies a * b = c * d ) assume A10: ( a = c & b = d ) ; ::_thesis: a * b = c * d [c,d] in [:ccs,ccs:] by ZFMISC_1:def_2; hence a * b = c * d by A10, FUNCT_1:49; ::_thesis: verum 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 the carrier of cs by A11, XBOOLE_0:def_5; take e ; :: according to GROUP_1:def_2 ::_thesis: for b1 being Element of the carrier of cs holds ( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of cs st ( b1 * b2 = e & b2 * b1 = e ) ) let h be Element of the carrier of cs; ::_thesis: ( h * e = h & e * h = h & ex b1 being Element of the carrier of cs st ( h * b1 = e & b1 * h = e ) ) h in ccs ; then reconsider h9 = h as Scalar of R ; thus h * e = h9 * (1_ R) by A9 .= h by VECTSP_1:def_4 ; ::_thesis: ( e * h = h & ex b1 being Element of the carrier of cs st ( h * b1 = e & b1 * h = e ) ) thus e * h = (1_ R) * h9 by A9 .= h by VECTSP_1:def_8 ; ::_thesis: ex b1 being Element of the carrier of cs st ( h * b1 = e & b1 * h = e ) 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 the carrier of cs by XBOOLE_0:def_5; take g ; ::_thesis: ( h * g = e & g * h = e ) thus h * g = h9 * (h9 ") by A9 .= e by A13, VECTSP_2:9 ; ::_thesis: g * h = e thus g * h = (h9 ") * h9 by A9 .= e by A13, VECTSP_2:9 ; ::_thesis: verum end; cs is associative proof let x, y, z be Element of the carrier of cs; :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z) A14: z in the carrier of cs ; ( x in the carrier of cs & y in the carrier of cs ) ; then reconsider x9 = x, y9 = y, z9 = z as Element of the carrier of R 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 ; ::_thesis: verum end; hence ex b1 being strict Group st ( the carrier of b1 = NonZero R & the multF of b1 = the multF of R || the carrier of b1 ) by A12; ::_thesis: verum end; uniqueness for b1, b2 being strict Group st the carrier of b1 = NonZero R & the multF of b1 = the multF of R || the carrier of b1 & the carrier of b2 = NonZero R & the multF of b2 = the multF of R || the carrier of b2 holds b1 = b2 ; end; :: deftheorem Def1 defines MultGroup UNIROOTS:def_1_:_ for R being Skew-Field for b2 being strict Group holds ( b2 = MultGroup R iff ( the carrier of b2 = NonZero R & the multF of b2 = the multF of R || the carrier of b2 ) ); theorem :: UNIROOTS:15 for R being Skew-Field holds the carrier of R = the carrier of (MultGroup R) \/ {(0. R)} proof let R be Skew-Field; ::_thesis: the carrier of R = the carrier of (MultGroup R) \/ {(0. R)} NonZero R = the carrier of (MultGroup R) by Def1; hence the carrier of R = the carrier of (MultGroup R) \/ {(0. R)} by XBOOLE_1:45; ::_thesis: verum end; theorem Th16: :: UNIROOTS:16 for R being Skew-Field for a, b being Element of R for c, d being Element of (MultGroup R) st a = c & b = d holds c * d = a * b proof let R be Skew-Field; ::_thesis: for a, b being Element of R for c, d being Element of (MultGroup R) st a = c & b = d holds c * d = a * b let a, b be Element of R; ::_thesis: for c, d being Element of (MultGroup R) st a = c & b = d holds c * d = a * b let c, d be Element of (MultGroup R); ::_thesis: ( a = c & b = d implies c * d = a * b ) assume A1: ( a = c & b = d ) ; ::_thesis: c * d = a * b set cMGR = the carrier of (MultGroup R); A2: [c,d] in [: the carrier of (MultGroup R), the carrier of (MultGroup R):] by ZFMISC_1:def_2; thus c * d = ( the multF of R || the carrier of (MultGroup R)) . (c,d) by Def1 .= a * b by A1, A2, FUNCT_1:49 ; ::_thesis: verum end; theorem Th17: :: UNIROOTS:17 for R being Skew-Field holds 1_ R = 1_ (MultGroup R) proof let R be Skew-Field; ::_thesis: 1_ R = 1_ (MultGroup R) 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__::_thesis:_for_h_being_Element_of_(MultGroup_R)_holds_ (_h_*_uR_=_h_&_uR_*_h_=_h_) let h be Element of (MultGroup R); ::_thesis: ( h * uR = h & uR * h = h ) reconsider g = h as Element of R by A1, XBOOLE_0:def_5; g * (1_ R) = g by VECTSP_1:def_4; hence h * uR = h by Th16; ::_thesis: uR * h = h (1_ R) * g = g by VECTSP_1:def_8; hence uR * h = h by Th16; ::_thesis: verum end; hence 1_ R = 1_ (MultGroup R) by GROUP_1:def_4; ::_thesis: verum end; registration let R be finite Skew-Field; cluster MultGroup R -> finite strict ; correctness coherence MultGroup R is finite ; proof the carrier of (MultGroup R) = NonZero R by Def1; hence MultGroup R is finite ; ::_thesis: verum end; end; theorem :: UNIROOTS:18 for R being finite Skew-Field holds card (MultGroup R) = (card R) - 1 proof let R be finite Skew-Field; ::_thesis: card (MultGroup R) = (card R) - 1 set G = MultGroup R; the carrier of (MultGroup R) = NonZero R by Def1; then card the carrier of (MultGroup R) = (card R) - (card {(0. R)}) by CARD_2:44; hence card (MultGroup R) = (card R) - 1 by CARD_1:30; ::_thesis: verum end; theorem Th19: :: UNIROOTS:19 for R being Skew-Field for s being set st s in the carrier of (MultGroup R) holds s in the carrier of R proof let R be Skew-Field; ::_thesis: for s being set st s in the carrier of (MultGroup R) holds s in the carrier of R let s be set ; ::_thesis: ( s in the carrier of (MultGroup R) implies s in the carrier of R ) assume s in the carrier of (MultGroup R) ; ::_thesis: s in the carrier of R then s in NonZero R by Def1; hence s in the carrier of R ; ::_thesis: verum end; theorem :: UNIROOTS:20 for R being Skew-Field holds the carrier of (MultGroup R) c= the carrier of R proof let R be Skew-Field; ::_thesis: the carrier of (MultGroup R) c= the carrier of R let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in the carrier of (MultGroup R) or s in the carrier of R ) assume s in the carrier of (MultGroup R) ; ::_thesis: s in the carrier of R then s in NonZero R by Def1; hence s in the carrier of R ; ::_thesis: verum end; begin definition let n be non empty Element of NAT ; funcn -roots_of_1 -> Subset of F_Complex equals :: UNIROOTS:def 2 { x where x is Element of F_Complex : x is CRoot of n, 1_ F_Complex } ; coherence { x where x is Element of F_Complex : x is CRoot of n, 1_ F_Complex } is Subset of F_Complex proof set H = { x where x is Element of F_Complex : x is CRoot of n, 1_ F_Complex } ; for x being set st x in { x where x is Element of F_Complex : x is CRoot of n, 1_ F_Complex } holds x in the carrier of F_Complex proof let x be set ; ::_thesis: ( x in { x where x is Element of F_Complex : x is CRoot of n, 1_ F_Complex } implies x in the carrier of F_Complex ) assume x in { x where x is Element of F_Complex : x is CRoot of n, 1_ F_Complex } ; ::_thesis: x in the carrier of F_Complex then ex y being Element of F_Complex st ( y = x & y is CRoot of n, 1_ F_Complex ) ; hence x in the carrier of F_Complex ; ::_thesis: verum end; hence { x where x is Element of F_Complex : x is CRoot of n, 1_ F_Complex } is Subset of F_Complex by TARSKI:def_3; ::_thesis: verum end; end; :: deftheorem defines -roots_of_1 UNIROOTS:def_2_:_ for n being non empty Element of NAT holds n -roots_of_1 = { x where x is Element of F_Complex : x is CRoot of n, 1_ F_Complex } ; theorem Th21: :: UNIROOTS:21 for n being non empty Element of NAT for x being Element of F_Complex holds ( x in n -roots_of_1 iff x is CRoot of n, 1_ F_Complex ) proof let n be non empty Element of NAT ; ::_thesis: for x being Element of F_Complex holds ( x in n -roots_of_1 iff x is CRoot of n, 1_ F_Complex ) let x be Element of F_Complex; ::_thesis: ( x in n -roots_of_1 iff x is CRoot of n, 1_ F_Complex ) hereby ::_thesis: ( x is CRoot of n, 1_ F_Complex implies x in n -roots_of_1 ) assume x in n -roots_of_1 ; ::_thesis: x is CRoot of n, 1_ F_Complex then ex y being Element of F_Complex st ( y = x & y is CRoot of n, 1_ F_Complex ) ; hence x is CRoot of n, 1_ F_Complex ; ::_thesis: verum end; thus ( x is CRoot of n, 1_ F_Complex implies x in n -roots_of_1 ) ; ::_thesis: verum end; theorem Th22: :: UNIROOTS:22 for n being non empty Element of NAT holds 1_ F_Complex in n -roots_of_1 proof let n be non empty Element of NAT ; ::_thesis: 1_ F_Complex in n -roots_of_1 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 1_ F_Complex in n -roots_of_1 ; ::_thesis: verum end; theorem Th23: :: UNIROOTS:23 for n being non empty Element of NAT for x being Element of F_Complex st x in n -roots_of_1 holds |.x.| = 1 proof let n be non empty Element of NAT ; ::_thesis: for x being Element of F_Complex st x in n -roots_of_1 holds |.x.| = 1 let x be Element of F_Complex; ::_thesis: ( x in n -roots_of_1 implies |.x.| = 1 ) assume A1: x in n -roots_of_1 ; ::_thesis: |.x.| = 1 A2: now__::_thesis:_not_x_=_0._F_Complex assume x = 0. F_Complex ; ::_thesis: contradiction then (power F_Complex) . (x,n) <> 1_ F_Complex by VECTSP_1:36; then x is not CRoot of n, 1_ F_Complex by COMPLFLD:def_2; hence contradiction by A1, Th21; ::_thesis: verum end; then A3: |.x.| > 0 by COMPLFLD:59; x is CRoot of n, 1_ F_Complex by A1, Th21; then (power F_Complex) . (x,n) = 1_ F_Complex by COMPLFLD:def_2; then A4: 1 = |.x.| to_power n by A2, COMPLFLD:60, POLYNOM5:7; assume A5: |.x.| <> 1 ; ::_thesis: contradiction percases ( |.x.| < 1 or |.x.| > 1 ) by A5, XXREAL_0:1; supposeA6: |.x.| < 1 ; ::_thesis: contradiction reconsider n9 = n as Rational ; |.x.| #Q n9 < 1 by A3, A6, PREPOWER:65; hence contradiction by A4, A3, PREPOWER:49; ::_thesis: verum end; suppose |.x.| > 1 ; ::_thesis: contradiction hence contradiction by A4, POWER:35; ::_thesis: verum end; end; end; theorem Th24: :: UNIROOTS:24 for n being non empty Element of NAT for x being Element of F_Complex holds ( x in n -roots_of_1 iff ex k being Element of NAT st x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] ) proof let n be non empty Element of NAT ; ::_thesis: for x being Element of F_Complex holds ( x in n -roots_of_1 iff ex k being Element of NAT st x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] ) let x be Element of F_Complex; ::_thesis: ( x in n -roots_of_1 iff ex k being Element of NAT st x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] ) hereby ::_thesis: ( ex k being Element of NAT st x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] implies x in n -roots_of_1 ) assume A1: x in n -roots_of_1 ; ::_thesis: ex k being Element of NAT st x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] A2: now__::_thesis:_not_x_=_0._F_Complex assume x = 0. F_Complex ; ::_thesis: contradiction then (power F_Complex) . (x,n) <> 1_ F_Complex by VECTSP_1:36; then x is not CRoot of n, 1_ F_Complex by COMPLFLD:def_2; hence contradiction by A1, Th21; ::_thesis: verum end; then ( 0 <= Arg x & Arg x < 2 * PI ) by COMPLFLD:7, COMPTRIG:def_1; then A3: 0 + (- 1) <= ((n * (Arg x)) / (2 * PI)) + (- 1) by XREAL_1:7; x is CRoot of n, 1_ F_Complex by A1, Th21; then (power F_Complex) . (x,n) = 1_ F_Complex by COMPLFLD:def_2; then A4: 1 = |.x.| to_power n by A2, COMPLFLD:60, POLYNOM5:7; A5: now__::_thesis:_not_|.x.|_<>_1 A6: |.x.| > 0 by A2, COMPLFLD:59; assume A7: |.x.| <> 1 ; ::_thesis: contradiction percases ( |.x.| < 1 or |.x.| > 1 ) by A7, XXREAL_0:1; supposeA8: |.x.| < 1 ; ::_thesis: contradiction reconsider n9 = n as Rational ; |.x.| #Q n9 < 1 by A6, A8, PREPOWER:65; hence contradiction by A4, A6, PREPOWER:49; ::_thesis: verum end; suppose |.x.| > 1 ; ::_thesis: contradiction hence contradiction by A4, POWER:35; ::_thesis: verum end; end; end; set m2 = [\((n * (Arg x)) / (2 * PI))/]; reconsider z = x as Element of COMPLEX by XCMPLX_0:def_2; consider r being real number such that A9: r = ((2 * PI) * (- [\((n * (Arg x)) / (2 * PI))/])) + (n * (Arg x)) and A10: ( 0 <= r & r < 2 * PI ) by COMPLEX2:1, COMPTRIG:5; ((n * (Arg x)) / (2 * PI)) - 1 < [\((n * (Arg x)) / (2 * PI))/] by INT_1:def_6; then not [\((n * (Arg x)) / (2 * PI))/] <= - 1 by A3, XXREAL_0:2; then (- 1) + 1 <= [\((n * (Arg x)) / (2 * PI))/] 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 being Element of NAT st x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] by A5, A14; ::_thesis: verum end; now__::_thesis:_(_ex_k_being_Element_of_NAT_st_x_=_[**(cos_(((2_*_PI)_*_k)_/_n)),(sin_(((2_*_PI)_*_k)_/_n))**]_implies_x_in_n_-roots_of_1_) reconsider z = 1_ F_Complex as Element of COMPLEX by XCMPLX_0:def_2; set 1F = Arg (1_ F_Complex); given k being Element of NAT such that A15: x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] ; ::_thesis: x in n -roots_of_1 0 + 1 <= n by NAT_1:13; then n -root 1 = 1 by POWER:6; then x = ((n -root |.z.|) * (cos (((Arg (1_ F_Complex)) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg (1_ F_Complex)) + ((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 ; ::_thesis: verum end; hence ( ex k being Element of NAT st x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] implies x in n -roots_of_1 ) ; ::_thesis: verum end; theorem Th25: :: UNIROOTS:25 for n being non empty Element of NAT for x, y being Element of COMPLEX st x in n -roots_of_1 & y in n -roots_of_1 holds x * y in n -roots_of_1 proof let n be non empty Element of NAT ; ::_thesis: for x, y being Element of COMPLEX st x in n -roots_of_1 & y in n -roots_of_1 holds x * y in n -roots_of_1 let x, y be Element of COMPLEX ; ::_thesis: ( x in n -roots_of_1 & y in n -roots_of_1 implies x * y in n -roots_of_1 ) assume that A1: x in n -roots_of_1 and A2: y in n -roots_of_1 ; ::_thesis: x * y in n -roots_of_1 reconsider a = x as Element of F_Complex by COMPLFLD:def_1; consider i being Element of NAT such that A3: a = [**(cos (((2 * PI) * i) / n)),(sin (((2 * PI) * i) / n))**] by A1, Th24; reconsider b = y as Element of F_Complex by COMPLFLD:def_1; consider j being Element of NAT such that A4: b = [**(cos (((2 * PI) * j) / n)),(sin (((2 * PI) * j) / n))**] by A2, Th24; a * b = [**(cos (((2 * PI) * ((i + j) mod n)) / n)),(sin (((2 * PI) * ((i + j) mod n)) / n))**] by A3, A4, Th11; hence x * y in n -roots_of_1 by Th24; ::_thesis: verum end; theorem Th26: :: UNIROOTS:26 for n being non empty Element of NAT holds n -roots_of_1 = { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } proof let n be non empty Element of NAT ; ::_thesis: n -roots_of_1 = { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } set X = { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } ; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_n_-roots_of_1_implies_x_in__{__[**(cos_(((2_*_PI)_*_k)_/_n)),(sin_(((2_*_PI)_*_k)_/_n))**]_where_k_is_Element_of_NAT_:_k_<_n__}__)_&_(_x_in__{__[**(cos_(((2_*_PI)_*_k)_/_n)),(sin_(((2_*_PI)_*_k)_/_n))**]_where_k_is_Element_of_NAT_:_k_<_n__}__implies_x_in_n_-roots_of_1_)_) let x be set ; ::_thesis: ( ( x in n -roots_of_1 implies x in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } ) & ( x in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } implies x in n -roots_of_1 ) ) hereby ::_thesis: ( x in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } implies x in n -roots_of_1 ) assume A1: x in n -roots_of_1 ; ::_thesis: x in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } then reconsider a = x as Element of F_Complex ; consider k being Element of NAT such that A2: a = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] by A1, Th24; A3: k mod n < n by NAT_D:1; a = [**(cos (((2 * PI) * (k mod n)) / n)),(sin (((2 * PI) * (k mod n)) / n))**] by A2, Th10; hence x in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } by A3; ::_thesis: verum end; assume x in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } ; ::_thesis: x in n -roots_of_1 then ex k being Element of NAT st ( x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] & k < n ) ; hence x in n -roots_of_1 by Th24; ::_thesis: verum end; hence n -roots_of_1 = { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } by TARSKI:1; ::_thesis: verum end; theorem Th27: :: UNIROOTS:27 for n being non empty Element of NAT holds card (n -roots_of_1) = n proof let n be non empty Element of NAT ; ::_thesis: card (n -roots_of_1) = n set X = { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } ; defpred S1[ set , set ] means ex j being Element of NAT st ( j = $1 & $2 = [**(cos (((2 * PI) * (j -' 1)) / n)),(sin (((2 * PI) * (j -' 1)) / n))**] ); A1: { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } = n -roots_of_1 by Th26; [**(cos (((2 * PI) * 0) / n)),(sin (((2 * PI) * 0) / n))**] in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } ; then reconsider Y = { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } as non empty set ; A2: for x being set st x in Seg n holds ex y being set st ( y in Y & S1[x,y] ) proof let x be set ; ::_thesis: ( x in Seg n implies ex y being set st ( y in Y & S1[x,y] ) ) assume A3: x in Seg n ; ::_thesis: ex y being set st ( y in Y & S1[x,y] ) reconsider a = x as Element of NAT by A3; a <= n by A3, FINSEQ_1:1; then a < n + 1 by NAT_1:13; then A4: a - 1 < (n + 1) - 1 by XREAL_1:14; consider b being Element of NAT such that A5: b = a -' 1 ; 1 <= a by A3, FINSEQ_1:1; then a -' 1 < n by A4, XREAL_1:233; then [**(cos (((2 * PI) * b) / n)),(sin (((2 * PI) * b) / n))**] in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } by A5; hence ex y being set st ( y in Y & S1[x,y] ) by A5; ::_thesis: verum end; consider F being Function of (Seg n),Y such that A6: for x being set st x in Seg n holds S1[x,F . x] from FUNCT_2:sch_1(A2); for c being set st c in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } holds ex x being set st ( x in Seg n & c = F . x ) proof let c be set ; ::_thesis: ( c in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } implies ex x being set st ( x in Seg n & c = F . x ) ) assume c in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } ; ::_thesis: ex x being set st ( x in Seg n & c = F . x ) then consider k being Element of NAT such that A7: c = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] and A8: k < n ; A9: (k + 1) -' 1 = k by NAT_D:34; ( 0 + 1 <= k + 1 & k + 1 <= n ) by A8, INT_1:7; then A10: k + 1 in Seg n by FINSEQ_1:1; then ex j being Element of NAT st ( j = k + 1 & F . (k + 1) = [**(cos (((2 * PI) * (j -' 1)) / n)),(sin (((2 * PI) * (j -' 1)) / n))**] ) by A6; hence ex x being set st ( x in Seg n & c = F . x ) by A7, A10, A9; ::_thesis: verum end; then A11: rng F = { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } by FUNCT_2:10; A12: dom F = Seg n by FUNCT_2:def_1; for x1, x2 being set st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds x1 = x2 proof let x1, x2 be set ; ::_thesis: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 implies x1 = x2 ) assume that A13: x1 in dom F and A14: x2 in dom F and A15: F . x1 = F . x2 ; ::_thesis: x1 = x2 A16: x1 in Seg n by A13, FUNCT_2:def_1; then consider j being Element of NAT such that A17: j = x1 and A18: F . x1 = [**(cos (((2 * PI) * (j -' 1)) / n)),(sin (((2 * PI) * (j -' 1)) / n))**] by A6; set a1 = ((2 * PI) * (j -' 1)) / n; A19: 1 <= j by A16, A17, FINSEQ_1:1; j <= n by A16, A17, FINSEQ_1:1; then j - 1 < n by XREAL_1:146, XXREAL_0:2; then j -' 1 < n by A19, XREAL_1:233; then (j -' 1) / n < n / n by XREAL_1:74; then (j -' 1) / n < 1 by XCMPLX_1:60; then ((j -' 1) / n) * (2 * PI) < 1 * (2 * PI) by COMPTRIG:5, XREAL_1:68; then A20: ((2 * PI) * (j -' 1)) / n < 2 * PI by XCMPLX_1:74; A21: x2 in Seg n by A14, FUNCT_2:def_1; then consider k being Element of NAT such that A22: k = x2 and A23: F . x2 = [**(cos (((2 * PI) * (k -' 1)) / n)),(sin (((2 * PI) * (k -' 1)) / n))**] by A6; set a2 = ((2 * PI) * (k -' 1)) / n; A24: 1 <= k by A21, A22, FINSEQ_1:1; k <= n by A21, A22, FINSEQ_1:1; then k - 1 < n by XREAL_1:146, XXREAL_0:2; then k -' 1 < n by A24, XREAL_1:233; then (k -' 1) / n < n / n by XREAL_1:74; then (k -' 1) / n < 1 by XCMPLX_1:60; then ((k -' 1) / n) * (2 * PI) < 1 * (2 * PI) by COMPTRIG:5, XREAL_1:68; then A25: ((2 * PI) * (k -' 1)) / n < 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 ((2 * PI) * (j -' 1)) / n = ((2 * PI) * (k -' 1)) / n 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 x1 = x2 by A17, A22, A24, XREAL_1:235; ::_thesis: verum 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 { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } by A11, CARD_1:5; hence card (n -roots_of_1) = n by A1, FINSEQ_1:57; ::_thesis: verum end; registration let n be non empty Element of NAT ; clustern -roots_of_1 -> non empty ; correctness coherence not n -roots_of_1 is empty ; by Th22; clustern -roots_of_1 -> finite ; correctness coherence n -roots_of_1 is finite ; proof card (n -roots_of_1) = n by Th27; hence n -roots_of_1 is finite ; ::_thesis: verum end; end; theorem Th28: :: UNIROOTS:28 for n, ni being non empty Element of NAT st ni divides n holds ni -roots_of_1 c= n -roots_of_1 proof let n, ni be non empty Element of NAT ; ::_thesis: ( ni divides n implies ni -roots_of_1 c= n -roots_of_1 ) assume ni divides n ; ::_thesis: ni -roots_of_1 c= n -roots_of_1 then consider k being Nat such that A1: n = ni * k by NAT_D:def_3; reconsider k = k as Element of NAT by ORDINAL1:def_12; for x being set st x in ni -roots_of_1 holds x in n -roots_of_1 proof let x be set ; ::_thesis: ( x in ni -roots_of_1 implies x in n -roots_of_1 ) assume A2: x in ni -roots_of_1 ; ::_thesis: x in n -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 x in n -roots_of_1 ; ::_thesis: verum end; hence ni -roots_of_1 c= n -roots_of_1 by TARSKI:def_3; ::_thesis: verum end; theorem Th29: :: UNIROOTS:29 for R being Skew-Field for x being Element of (MultGroup R) for y being Element of R st y = x holds for k being Element of NAT holds (power (MultGroup R)) . (x,k) = (power R) . (y,k) proof let R be Skew-Field; ::_thesis: for x being Element of (MultGroup R) for y being Element of R st y = x holds for k being Element of NAT holds (power (MultGroup R)) . (x,k) = (power R) . (y,k) let x be Element of (MultGroup R); ::_thesis: for y being Element of R st y = x holds for k being Element of NAT holds (power (MultGroup R)) . (x,k) = (power R) . (y,k) let y be Element of R; ::_thesis: ( y = x implies for k being Element of NAT holds (power (MultGroup R)) . (x,k) = (power R) . (y,k) ) assume A1: y = x ; ::_thesis: for k being Element of NAT holds (power (MultGroup R)) . (x,k) = (power R) . (y,k) defpred S1[ Element of NAT ] means (power (MultGroup R)) . (x,$1) = (power R) . (y,$1); A2: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: S1[k] ; ::_thesis: S1[k + 1] thus (power (MultGroup R)) . (x,(k + 1)) = ((power (MultGroup R)) . (x,k)) * x by GROUP_1:def_7 .= ((power R) . (y,k)) * y by A1, A3, Th16 .= (power R) . (y,(k + 1)) by GROUP_1:def_7 ; ::_thesis: verum end; ( (power (MultGroup R)) . (x,0) = 1_ (MultGroup R) & (power R) . (y,0) = 1_ R ) by GROUP_1:def_7; then A4: S1[ 0 ] by Th17; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A2); ::_thesis: verum end; theorem Th30: :: UNIROOTS:30 for n being non empty Element of NAT for x being 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 empty Element of NAT ; ::_thesis: for x being Element of (MultGroup F_Complex) st x in n -roots_of_1 holds not x is being_of_order_0 let x be Element of the carrier of (MultGroup F_Complex); ::_thesis: ( x in n -roots_of_1 implies not x is being_of_order_0 ) assume x in n -roots_of_1 ; ::_thesis: not x is being_of_order_0 then consider c being Element of F_Complex such that A1: c = x and A2: c is CRoot of n, 1_ F_Complex ; A3: 1_ (MultGroup F_Complex) = 1_ F_Complex by Th17; (power F_Complex) . (c,n) = 1_ F_Complex by A2, COMPLFLD:def_2; then x |^ n = 1_ (MultGroup F_Complex) by A1, A3, Th29; hence not x is being_of_order_0 by GROUP_1:def_10; ::_thesis: verum end; theorem Th31: :: UNIROOTS:31 for n being non empty Element of NAT for k being Element of NAT for x being Element of (MultGroup F_Complex) st x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] holds ord x = n div (k gcd n) proof let n be non empty Element of NAT ; ::_thesis: for k being Element of NAT for x being Element of (MultGroup F_Complex) st x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] holds ord x = n div (k gcd n) let k be Element of NAT ; ::_thesis: for x being Element of (MultGroup F_Complex) st x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] holds ord x = n div (k gcd n) reconsider kgn = k gcd n as Element of NAT ; A1: k gcd n divides n by INT_2:21; then consider vn being Nat such that A2: n = kgn * vn by NAT_D:def_3; k gcd n divides k by INT_2:21; then consider i being Nat such that A3: k = kgn * i by NAT_D:def_3; let x be Element of (MultGroup F_Complex); ::_thesis: ( x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] implies ord x = n div (k gcd n) ) assume A4: x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] ; ::_thesis: ord x = n div (k gcd 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__::_thesis:_not_n_div_kgn_=_0 assume n div kgn = 0 ; ::_thesis: contradiction then n = (kgn * 0) + (n mod kgn) by NAT_D:2, NEWTON:58; hence contradiction by A1, A6, NAT_D:1, NAT_D:7; ::_thesis: verum end; reconsider y = x as Element of F_Complex by Th19; reconsider vn = vn as Element of NAT by ORDINAL1:def_12; A8: not vn is empty by A2; A9: n = (kgn * vn) + 0 by A2; then A10: n div kgn = vn by A6, NAT_D:def_1; A11: for m being Nat st x |^ m = 1_ (MultGroup F_Complex) & m <> 0 holds n div kgn <= m proof let m be Nat; ::_thesis: ( x |^ m = 1_ (MultGroup F_Complex) & m <> 0 implies n div kgn <= m ) assume that A12: x |^ m = 1_ (MultGroup F_Complex) and A13: m <> 0 ; ::_thesis: n div kgn <= m reconsider m = m as Element of NAT by ORDINAL1:def_12; now__::_thesis:_not_m_<_vn assume A14: m < vn ; ::_thesis: contradiction A15: now__::_thesis:_not_(k_*_m)_mod_n_=_0 assume (k * m) mod n = 0 ; ::_thesis: contradiction then n divides k * m by PEPIN:6; then consider j being Nat such that A16: k * m = n * j by NAT_D:def_3; consider a, b being Integer such that A17: k = kgn * a and A18: n = kgn * b and A19: a,b are_relative_prime by INT_2:23; 0 <= a by A6, A17; then reconsider ai = a as Element of NAT by INT_1:3; 0 <= b by A18; then reconsider bi = b as Element of NAT by INT_1:3; (m * a) * kgn = j * (b * kgn) by A17, A18, A16; then m * a = ((j * b) * kgn) / kgn by A6, XCMPLX_1:89; then m * a = j * b by A6, XCMPLX_1:89; then A20: bi divides m * ai by NAT_D:def_3; m < bi by A6, A10, A14, A18, NAT_D:18; hence contradiction by A13, A19, A20, INT_2:25, NAT_D:7; ::_thesis: verum end; A21: (((2 * PI) * k) / n) * m = ((2 * PI) * k) / (n / m) by XCMPLX_1:82 .= (((2 * PI) * k) * m) / n by XCMPLX_1:77 ; (2 * PI) * ((k * m) mod n) < (2 * PI) * n by COMPTRIG:5, NAT_D:1, XREAL_1:68; then ((2 * PI) * ((k * m) mod n)) / n < ((2 * PI) * n) / n by XREAL_1:74; then A22: ((2 * PI) * ((k * m) mod n)) / n < 2 * PI by XCMPLX_1:89; A23: 1_ (MultGroup F_Complex) = [**1,0**] by Th17, COMPLFLD:8; x |^ m = (power F_Complex) . (y,m) by Th29 .= y |^ m by A13, COMPLFLD:74 .= [**(cos (((2 * PI) * (k * m)) / n)),(sin ((((2 * PI) * k) * m) / n))**] by A4, A21, COMPTRIG:53 .= [**(cos (((2 * PI) * ((k * m) mod n)) / n)),(sin (((2 * PI) * ((k * m) mod n)) / n))**] by Th10 ; then cos (((2 * PI) * ((k * m) mod n)) / n) = 1 by A12, A23, COMPLEX1:77; hence contradiction by A15, A22, COMPTRIG:5, COMPTRIG:61; ::_thesis: verum end; hence n div kgn <= m by A6, A9, NAT_D:def_1; ::_thesis: verum end; reconsider i = i as Element of NAT by ORDINAL1:def_12; A24: (((2 * PI) * k) / n) * vn = ((2 * PI) * (kgn * i)) / (n / vn) by A3, XCMPLX_1:82 .= (((2 * PI) * (kgn * i)) * vn) / n by XCMPLX_1:77 .= (((2 * PI) * i) * n) / n by A2 .= ((2 * PI) * i) + 0 by XCMPLX_1:89 ; x |^ (n div kgn) = (power F_Complex) . (y,vn) by A10, Th29 .= y |^ vn by A8, COMPLFLD:74 .= [**(cos ((((2 * PI) * k) / n) * vn)),(sin ((((2 * PI) * k) / n) * vn))**] by A4, COMPTRIG:53 .= [**(cos 0),(sin (((2 * PI) * i) + 0))**] by A24, COMPLEX2:9 .= 1 + (0 * ) by COMPLEX2:8, SIN_COS:31 .= 1_ (MultGroup F_Complex) by Th17, COMPLFLD:8 ; hence ord x = n div (k gcd n) by A7, A5, A11, GROUP_1:def_11; ::_thesis: verum end; theorem Th32: :: UNIROOTS:32 for n being non empty Element of NAT holds n -roots_of_1 c= the carrier of (MultGroup F_Complex) proof let n be non empty Element of NAT ; ::_thesis: n -roots_of_1 c= the carrier of (MultGroup F_Complex) set cMGFC = the carrier of (MultGroup F_Complex); set FC = F_Complex ; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in n -roots_of_1 or a in the carrier of (MultGroup F_Complex) ) assume a in n -roots_of_1 ; ::_thesis: a in the carrier of (MultGroup F_Complex) then consider x being Element of F_Complex such that A1: a = x and A2: x is CRoot of n, 1_ F_Complex ; (power F_Complex) . (x,n) = 1_ F_Complex by A2, COMPLFLD:def_2; then x <> 0. F_Complex by VECTSP_1:36; then A3: not x in {(0. F_Complex)} by TARSKI:def_1; the carrier of (MultGroup F_Complex) = NonZero F_Complex by Def1; hence a in the carrier of (MultGroup F_Complex) by A1, A3, XBOOLE_0:def_5; ::_thesis: verum end; theorem :: UNIROOTS:33 for n being non empty Element of NAT ex x being Element of (MultGroup F_Complex) st ord x = n proof let n be non empty Element of NAT ; ::_thesis: ex x being Element of (MultGroup F_Complex) st ord x = n set x = [**(cos (((2 * PI) * 1) / n)),(sin (((2 * PI) * 1) / n))**]; ( n -roots_of_1 c= the carrier of (MultGroup F_Complex) & [**(cos (((2 * PI) * 1) / n)),(sin (((2 * PI) * 1) / n))**] in n -roots_of_1 ) by Th24, Th32; then reconsider y = [**(cos (((2 * PI) * 1) / n)),(sin (((2 * PI) * 1) / n))**] as Element of (MultGroup F_Complex) ; ( ord y = n div (1 gcd n) & 1 gcd n = 1 ) by Th31, WSIERP_1:8; hence ex x being Element of (MultGroup F_Complex) st ord x = n by NAT_2:4; ::_thesis: verum end; theorem Th34: :: UNIROOTS:34 for n being non empty Element of NAT for x being Element of (MultGroup F_Complex) holds ( ord x divides n iff x in n -roots_of_1 ) proof set FC = F_Complex ; let n be non empty Element of NAT ; ::_thesis: for x being Element of (MultGroup F_Complex) holds ( ord x divides n iff x in n -roots_of_1 ) let x be Element of (MultGroup F_Complex); ::_thesis: ( ord x divides n iff x in n -roots_of_1 ) reconsider c = x as Element of F_Complex by Th19; set MGFC = MultGroup F_Complex; A1: 1_ (MultGroup F_Complex) = 1_ F_Complex by Th17; hereby ::_thesis: ( x in n -roots_of_1 implies ord x divides n ) assume ord x divides n ; ::_thesis: x in n -roots_of_1 then consider k being Nat such that A2: n = (ord x) * k by NAT_D:def_3; x |^ (ord x) = 1_ (MultGroup F_Complex) by GROUP_1:41; then (x |^ (ord x)) |^ k = 1_ (MultGroup F_Complex) by GROUP_1:31; then x |^ n = 1_ (MultGroup F_Complex) by A2, GROUP_1:35; then (power F_Complex) . (c,n) = 1_ F_Complex by A1, Th29; then c is CRoot of n, 1_ F_Complex by COMPLFLD:def_2; hence x in n -roots_of_1 ; ::_thesis: verum end; assume x in n -roots_of_1 ; ::_thesis: ord x divides n then consider c being Element of F_Complex such that A3: c = x and A4: c is CRoot of n, 1_ F_Complex ; (power F_Complex) . (c,n) = 1_ F_Complex by A4, COMPLFLD:def_2; then x |^ n = 1_ (MultGroup F_Complex) by A1, A3, Th29; hence ord x divides n by GROUP_1:44; ::_thesis: verum end; theorem Th35: :: UNIROOTS:35 for n being non empty Element of NAT holds n -roots_of_1 = { x where x is Element of (MultGroup F_Complex) : ord x divides n } proof set cMGFC = the carrier of (MultGroup F_Complex); set MGFC = MultGroup F_Complex; let n be non empty Element of NAT ; ::_thesis: n -roots_of_1 = { x where x is Element of (MultGroup F_Complex) : ord x divides n } set R = { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } ; set S = { x where x is Element of (MultGroup F_Complex) : ord x divides n } ; A1: n -roots_of_1 = { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } ; then A2: { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } c= the carrier of (MultGroup F_Complex) by Th32; now__::_thesis:_for_a_being_set_holds_ (_(_a_in__{__a_where_a_is_Element_of_F_Complex_:_a_is_CRoot_of_n,_1__F_Complex__}__implies_a_in__{__x_where_x_is_Element_of_(MultGroup_F_Complex)_:_ord_x_divides_n__}__)_&_(_a_in__{__x_where_x_is_Element_of_(MultGroup_F_Complex)_:_ord_x_divides_n__}__implies_a_in__{__a_where_a_is_Element_of_F_Complex_:_a_is_CRoot_of_n,_1__F_Complex__}__)_) let a be set ; ::_thesis: ( ( a in { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } implies a in { x where x is Element of (MultGroup F_Complex) : ord x divides n } ) & ( a in { x where x is Element of (MultGroup F_Complex) : ord x divides n } implies a in { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } ) ) hereby ::_thesis: ( a in { x where x is Element of (MultGroup F_Complex) : ord x divides n } implies a in { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } ) assume A3: a in { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } ; ::_thesis: a in { x where x is Element of (MultGroup F_Complex) : ord x divides n } then reconsider x = a as Element of (MultGroup F_Complex) by A2; ord x divides n by A1, A3, Th34; hence a in { x where x is Element of (MultGroup F_Complex) : ord x divides n } ; ::_thesis: verum end; assume a in { x where x is Element of (MultGroup F_Complex) : ord x divides n } ; ::_thesis: a in { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } then ex x being Element of (MultGroup F_Complex) st ( a = x & ord x divides n ) ; hence a in { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } by A1, Th34; ::_thesis: verum end; hence n -roots_of_1 = { x where x is Element of (MultGroup F_Complex) : ord x divides n } by TARSKI:1; ::_thesis: verum end; theorem Th36: :: UNIROOTS:36 for n being non empty Element of NAT for x being set holds ( x in n -roots_of_1 iff ex y being Element of (MultGroup F_Complex) st ( x = y & ord y divides n ) ) proof set MGFC = MultGroup F_Complex; set cMGFC = the carrier of (MultGroup F_Complex); let n be non empty Element of NAT ; ::_thesis: for x being set holds ( x in n -roots_of_1 iff ex y being Element of (MultGroup F_Complex) st ( x = y & ord y divides n ) ) let x be set ; ::_thesis: ( x in n -roots_of_1 iff ex y being Element of (MultGroup F_Complex) st ( x = y & ord y divides n ) ) A1: n -roots_of_1 c= the carrier of (MultGroup F_Complex) by Th32; hereby ::_thesis: ( ex y being Element of (MultGroup F_Complex) st ( x = y & ord y divides n ) implies x in n -roots_of_1 ) assume A2: x in n -roots_of_1 ; ::_thesis: ex y being Element of (MultGroup F_Complex) st ( x = y & ord y divides n ) then reconsider a = x as Element of (MultGroup F_Complex) by A1; ord a divides n by A2, Th34; hence ex y being Element of (MultGroup F_Complex) st ( x = y & ord y divides n ) ; ::_thesis: verum end; thus ( ex y being Element of (MultGroup F_Complex) st ( x = y & ord y divides n ) implies x in n -roots_of_1 ) by Th34; ::_thesis: verum end; definition let n be non empty Element of NAT ; funcn -th_roots_of_1 -> strict Group means :Def3: :: UNIROOTS:def 3 ( the carrier of it = n -roots_of_1 & the multF of it = the multF of F_Complex || (n -roots_of_1) ); existence ex b1 being strict Group st ( the carrier of b1 = n -roots_of_1 & the multF of b1 = the multF of F_Complex || (n -roots_of_1) ) 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 [:(n -roots_of_1),(n -roots_of_1):] c= [:COMPLEX,COMPLEX:] by ZFMISC_1:96; then A1: [:(n -roots_of_1),(n -roots_of_1):] c= dom multcomplex by FUNCT_2:def_1; A2: multcomplex = the multF of F_Complex by COMPLFLD:def_1; then A3: dom ( the multF of F_Complex || (n -roots_of_1)) = (dom multcomplex) /\ [:(n -roots_of_1),(n -roots_of_1):] by RELAT_1:61; then A4: dom ( the multF of F_Complex || (n -roots_of_1)) = [:(n -roots_of_1),(n -roots_of_1):] by A1, XBOOLE_1:28; for x being set st x in [:(n -roots_of_1),(n -roots_of_1):] holds ( the multF of F_Complex || (n -roots_of_1)) . x in n -roots_of_1 proof let x be set ; ::_thesis: ( x in [:(n -roots_of_1),(n -roots_of_1):] implies ( the multF of F_Complex || (n -roots_of_1)) . x in n -roots_of_1 ) assume A5: x in [:(n -roots_of_1),(n -roots_of_1):] ; ::_thesis: ( the multF of F_Complex || (n -roots_of_1)) . x in n -roots_of_1 consider a, b being set such that A6: [a,b] = x by A5, RELAT_1:def_1; A7: b in n -roots_of_1 by A5, A6, ZFMISC_1:87; A8: a in n -roots_of_1 by A5, A6, ZFMISC_1:87; reconsider b = b as Element of COMPLEX by A7, COMPLFLD:def_1; reconsider a = a as Element of COMPLEX by A8, COMPLFLD:def_1; ( multcomplex . (a,b) = a * b & ( the multF of F_Complex || (n -roots_of_1)) . [a,b] = multcomplex . [a,b] ) by A2, A4, A5, A6, BINOP_2:def_5, FUNCT_1:47; hence ( the multF of F_Complex || (n -roots_of_1)) . x in n -roots_of_1 by A6, A8, A7, Th25; ::_thesis: verum end; then reconsider uM = the multF of F_Complex || (n -roots_of_1) 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 multMagma(# (n -roots_of_1),uM #) by Th22; A9: 1_ F_Complex = [**(cos (((2 * PI) * 0) / n)),(sin (((2 * PI) * 0) / n))**] by COMPLFLD:8, SIN_COS:31; A10: for s1 being Element of multMagma(# (n -roots_of_1),uM #) holds ( s1 * 1F = s1 & 1F * s1 = s1 & ex s2 being Element of multMagma(# (n -roots_of_1),uM #) st ( s1 * s2 = 1_ F_Complex & s2 * s1 = 1_ F_Complex ) ) proof let s1 be Element of multMagma(# (n -roots_of_1),uM #); ::_thesis: ( s1 * 1F = s1 & 1F * s1 = s1 & ex s2 being Element of multMagma(# (n -roots_of_1),uM #) st ( s1 * s2 = 1_ F_Complex & s2 * s1 = 1_ F_Complex ) ) A11: ex s2 being Element of multMagma(# (n -roots_of_1),uM #) st ( s1 * s2 = 1_ F_Complex & s2 * s1 = 1_ F_Complex ) proof s1 in the carrier of F_Complex by TARSKI:def_3; then consider k being Element of NAT such that A12: s1 = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] by Th24; reconsider e1 = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] as Element of F_Complex ; ex j being Element of NAT st (k + j) mod n = 0 proof set r = k mod n; k mod n < n by NAT_D:1; then consider j being Nat such that A13: (k mod n) + j = n by NAT_1:10; k = (n * (k div n)) + (k mod n) 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 ex j being Element of NAT st (k + j) mod n = 0 by NAT_D:13; ::_thesis: verum end; then consider j being Element of NAT such that A14: (k + j) mod n = 0 ; set ss2 = [**(cos (((2 * PI) * j) / n)),(sin (((2 * PI) * j) / n))**]; reconsider s2 = [**(cos (((2 * PI) * j) / n)),(sin (((2 * PI) * j) / n))**] as Element of multMagma(# (n -roots_of_1),uM #) 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 ( the multF of F_Complex || (n -roots_of_1)) ) 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 ( the multF of F_Complex || (n -roots_of_1)) ) by A4, Th11, ZFMISC_1:87; then s1 * s2 = 1_ F_Complex by A12, A14, COMPLFLD:8, FUNCT_1:47, SIN_COS:31; hence ex s2 being Element of multMagma(# (n -roots_of_1),uM #) st ( s1 * s2 = 1_ F_Complex & s2 * s1 = 1_ F_Complex ) by A15; ::_thesis: verum end; ( s1 * 1F = s1 & 1F * s1 = s1 ) proof A16: ( [s1,1F] in dom ( the multF of F_Complex || (n -roots_of_1)) & [1F,s1] in dom ( the multF of F_Complex || (n -roots_of_1)) ) by A4, ZFMISC_1:87; reconsider e1 = s1 as Element of F_Complex by TARSKI:def_3; consider k being Element of NAT such that A17: e1 = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] by Th24; A18: (1_ F_Complex) * e1 = [**(cos (((2 * PI) * ((k + 0) mod n)) / n)),(sin (((2 * PI) * ((k + 0) mod n)) / n))**] by A9, A17, Th11 .= s1 by A17, Th10 ; e1 * (1_ F_Complex) = [**(cos (((2 * PI) * ((k + 0) mod n)) / n)),(sin (((2 * PI) * ((k + 0) mod n)) / n))**] by A9, A17, Th11 .= s1 by A17, Th10 ; hence ( s1 * 1F = s1 & 1F * s1 = s1 ) by A18, A16, FUNCT_1:47; ::_thesis: verum end; hence ( s1 * 1F = s1 & 1F * s1 = s1 & ex s2 being Element of multMagma(# (n -roots_of_1),uM #) st ( s1 * s2 = 1_ F_Complex & s2 * s1 = 1_ F_Complex ) ) by A11; ::_thesis: verum end; A19: rng uM c= n -roots_of_1 by RELAT_1:def_19; for r, s, t being Element of multMagma(# (n -roots_of_1),uM #) holds (r * s) * t = r * (s * t) proof set mc = multcomplex ; let r, s, t be Element of multMagma(# (n -roots_of_1),uM #); ::_thesis: (r * s) * t = r * (s * t) 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 ( the multF of F_Complex || (n -roots_of_1)) by A4, ZFMISC_1:87; then ( the multF of F_Complex || (n -roots_of_1)) . [r,s] in rng ( the multF of F_Complex || (n -roots_of_1)) by FUNCT_1:3; then A23: [(( the multF of F_Complex || (n -roots_of_1)) . [r,s]),t] in dom ( the multF of F_Complex || (n -roots_of_1)) by A4, A19, ZFMISC_1:87; A24: [s,t] in dom ( the multF of F_Complex || (n -roots_of_1)) by A4, ZFMISC_1:87; then ( the multF of F_Complex || (n -roots_of_1)) . [s,t] in rng ( the multF of F_Complex || (n -roots_of_1)) by FUNCT_1:3; then A25: [r,(( the multF of F_Complex || (n -roots_of_1)) . [s,t])] in dom ( the multF of F_Complex || (n -roots_of_1)) by A4, A19, ZFMISC_1:87; ( the multF of F_Complex || (n -roots_of_1)) . [s,t] = multcomplex . [s,t] by A2, A24, FUNCT_1:47; then A26: ( the multF of F_Complex || (n -roots_of_1)) . [r,(( the multF of F_Complex || (n -roots_of_1)) . [s,t])] = multcomplex . (r,(multcomplex . (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; ( the multF of F_Complex || (n -roots_of_1)) . [r,s] = multcomplex . [r,s] by A2, A22, FUNCT_1:47; then ( the multF of F_Complex || (n -roots_of_1)) . [(( the multF of F_Complex || (n -roots_of_1)) . [r,s]),t] = multcomplex . ((multcomplex . (r,s)),t) by A2, A23, FUNCT_1:47; hence (r * s) * t = r * (s * t) by A20, A21, A27, A26, BINOP_1:def_3; ::_thesis: verum end; then multMagma(# (n -roots_of_1),uM #) is Group by A10, GROUP_1:1; hence ex b1 being strict Group st ( the carrier of b1 = n -roots_of_1 & the multF of b1 = the multF of F_Complex || (n -roots_of_1) ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict Group st the carrier of b1 = n -roots_of_1 & the multF of b1 = the multF of F_Complex || (n -roots_of_1) & the carrier of b2 = n -roots_of_1 & the multF of b2 = the multF of F_Complex || (n -roots_of_1) holds b1 = b2 ; end; :: deftheorem Def3 defines -th_roots_of_1 UNIROOTS:def_3_:_ for n being non empty Element of NAT for b2 being strict Group holds ( b2 = n -th_roots_of_1 iff ( the carrier of b2 = n -roots_of_1 & the multF of b2 = the multF of F_Complex || (n -roots_of_1) ) ); theorem :: UNIROOTS:37 for n being non empty Element of NAT holds n -th_roots_of_1 is Subgroup of MultGroup F_Complex proof set MGFC = MultGroup F_Complex; set cMGFC = the carrier of (MultGroup F_Complex); set FC = F_Complex ; let n be non empty Element of NAT ; ::_thesis: n -th_roots_of_1 is Subgroup of MultGroup F_Complex set nth = n -th_roots_of_1 ; set cnth = the carrier of (n -th_roots_of_1); A1: the carrier of (n -th_roots_of_1) = n -roots_of_1 by Def3; then A2: the carrier of (n -th_roots_of_1) c= the carrier of (MultGroup F_Complex) by Th32; ( the multF of (n -th_roots_of_1) = the multF of F_Complex || (n -roots_of_1) & the multF of (MultGroup F_Complex) = the multF of F_Complex || the carrier of (MultGroup F_Complex) ) by Def1, Def3; then the multF of (n -th_roots_of_1) = the multF of (MultGroup F_Complex) || the carrier of (n -th_roots_of_1) by A1, A2, RELAT_1:74, ZFMISC_1:96; hence n -th_roots_of_1 is Subgroup of MultGroup F_Complex by A2, GROUP_2:def_5; ::_thesis: verum end; begin definition let n be non empty Nat; let L be non empty left_unital doubleLoopStr ; func unital_poly (L,n) -> Polynomial of L equals :: UNIROOTS:def 4 ((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L)); coherence ((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L)) is Polynomial of L proof set p = ((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L)); A1: for i being Nat st i <> 0 & i <> n holds (((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L))) . i = 0. L proof set q = (0_. L) +* (0,(- (1_ L))); let i be Nat; ::_thesis: ( i <> 0 & i <> n implies (((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L))) . i = 0. L ) assume that A2: i <> 0 and A3: i <> n ; ::_thesis: (((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L))) . i = 0. L A4: i in NAT by ORDINAL1:def_12; (((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L))) . i = ((0_. L) +* (0,(- (1_ L)))) . i by A3, FUNCT_7:32 .= (0_. L) . i by A2, FUNCT_7:32 .= 0. L by A4, FUNCOP_1:7 ; hence (((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L))) . i = 0. L ; ::_thesis: verum end; for i being Nat st i >= n + 1 holds (((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L))) . i = 0. L proof let i be Nat; ::_thesis: ( i >= n + 1 implies (((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L))) . i = 0. L ) assume A5: i >= n + 1 ; ::_thesis: (((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L))) . i = 0. L now__::_thesis:_not_i_=_n A6: n + 0 < n + 1 by XREAL_1:8; assume i = n ; ::_thesis: contradiction hence contradiction by A5, A6; ::_thesis: verum end; hence (((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L))) . i = 0. L by A1, A5; ::_thesis: verum end; hence ((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L)) is Polynomial of L by ALGSEQ_1:def_1; ::_thesis: verum end; end; :: deftheorem defines unital_poly UNIROOTS:def_4_:_ for n being non empty Nat for L being non empty left_unital doubleLoopStr holds unital_poly (L,n) = ((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L)); Lm4: unital_poly (F_Complex,1) = <%(- (1_ F_Complex)),(1_ F_Complex)%> by POLYNOM5:def_4; theorem Th38: :: UNIROOTS:38 for L being non empty left_unital doubleLoopStr for n being non empty Element of NAT holds ( (unital_poly (L,n)) . 0 = - (1_ L) & (unital_poly (L,n)) . n = 1_ L ) proof let L be non empty left_unital doubleLoopStr ; ::_thesis: for n being non empty Element of NAT holds ( (unital_poly (L,n)) . 0 = - (1_ L) & (unital_poly (L,n)) . n = 1_ L ) let n be non empty Element of NAT ; ::_thesis: ( (unital_poly (L,n)) . 0 = - (1_ L) & (unital_poly (L,n)) . n = 1_ L ) set p = (0_. L) +* (0,(- (1_ L))); set q = (0_. L) +* (n,(1_ L)); 0 in NAT ; then A1: ( unital_poly (L,n) = ((0_. L) +* (n,(1_ L))) +* (0,(- (1_ L))) & 0 in dom ((0_. L) +* (n,(1_ L))) ) by FUNCT_7:33, NORMSP_1:12; n in NAT ; then n in dom ((0_. L) +* (0,(- (1_ L)))) by NORMSP_1:12; hence ( (unital_poly (L,n)) . 0 = - (1_ L) & (unital_poly (L,n)) . n = 1_ L ) by A1, FUNCT_7:31; ::_thesis: verum end; theorem Th39: :: UNIROOTS:39 for L being non empty left_unital doubleLoopStr for n being non empty Nat for i being Nat st i <> 0 & i <> n holds (unital_poly (L,n)) . i = 0. L proof let L be non empty left_unital doubleLoopStr ; ::_thesis: for n being non empty Nat for i being Nat st i <> 0 & i <> n holds (unital_poly (L,n)) . i = 0. L let n be non empty Nat; ::_thesis: for i being Nat st i <> 0 & i <> n holds (unital_poly (L,n)) . i = 0. L let i be Nat; ::_thesis: ( i <> 0 & i <> n implies (unital_poly (L,n)) . i = 0. L ) assume that A1: i <> 0 and A2: i <> n ; ::_thesis: (unital_poly (L,n)) . i = 0. L set p = (0_. L) +* (0,(- (1_ L))); A3: i in NAT by ORDINAL1:def_12; (((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L))) . i = ((0_. L) +* (0,(- (1_ L)))) . i by A2, FUNCT_7:32 .= (0_. L) . i by A1, FUNCT_7:32 .= 0. L by A3, FUNCOP_1:7 ; hence (unital_poly (L,n)) . i = 0. L ; ::_thesis: verum end; theorem Th40: :: UNIROOTS:40 for L being non empty non degenerated well-unital doubleLoopStr for n being non empty Element of NAT holds len (unital_poly (L,n)) = n + 1 proof let L be non empty non degenerated well-unital doubleLoopStr ; ::_thesis: for n being non empty Element of NAT holds len (unital_poly (L,n)) = n + 1 let n be non empty Element of NAT ; ::_thesis: len (unital_poly (L,n)) = n + 1 A1: for m being Nat st m is_at_least_length_of unital_poly (L,n) holds n + 1 <= m proof let m be Nat; ::_thesis: ( m is_at_least_length_of unital_poly (L,n) implies n + 1 <= m ) assume A2: m is_at_least_length_of unital_poly (L,n) ; ::_thesis: n + 1 <= m now__::_thesis:_not_m_<_n_+_1 assume m < n + 1 ; ::_thesis: contradiction 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; ::_thesis: verum end; hence n + 1 <= m ; ::_thesis: verum end; for i being Nat st i >= n + 1 holds (unital_poly (L,n)) . i = 0. L proof let i be Nat; ::_thesis: ( i >= n + 1 implies (unital_poly (L,n)) . i = 0. L ) assume A3: i >= n + 1 ; ::_thesis: (unital_poly (L,n)) . i = 0. L now__::_thesis:_not_i_=_n A4: n + 0 < n + 1 by XREAL_1:8; assume i = n ; ::_thesis: contradiction hence contradiction by A3, A4; ::_thesis: verum end; hence (unital_poly (L,n)) . i = 0. L by A3, Th39; ::_thesis: verum end; then n + 1 is_at_least_length_of unital_poly (L,n) by ALGSEQ_1:def_2; hence len (unital_poly (L,n)) = n + 1 by A1, ALGSEQ_1:def_3; ::_thesis: verum end; registration let L be non empty non degenerated well-unital doubleLoopStr ; let n be non empty Element of NAT ; cluster unital_poly (L,n) -> non-zero ; correctness coherence unital_poly (L,n) is non-zero ; proof len (unital_poly (L,n)) = n + 1 by Th40; hence unital_poly (L,n) is non-zero by UPROOTS:17; ::_thesis: verum end; end; theorem Th41: :: UNIROOTS:41 for n being non empty Element of NAT for x being Element of F_Complex holds eval ((unital_poly (F_Complex,n)),x) = ((power F_Complex) . (x,n)) - 1 proof 1 - 1 = 0 ; then A1: 1 -' 1 = 0 by XREAL_1:233; reconsider z2 = 1_ F_Complex as Element of COMPLEX by COMPLFLD:def_1; let n be non empty Element of NAT ; ::_thesis: for x being Element of F_Complex holds eval ((unital_poly (F_Complex,n)),x) = ((power F_Complex) . (x,n)) - 1 let x be Element of F_Complex; ::_thesis: eval ((unital_poly (F_Complex,n)),x) = ((power F_Complex) . (x,n)) - 1 set p = unital_poly (F_Complex,n); consider F being FinSequence of F_Complex such that A2: eval ((unital_poly (F_Complex,n)),x) = Sum F and A3: len F = len (unital_poly (F_Complex,n)) and A4: for i being Element of NAT st i in dom F holds F . i = ((unital_poly (F_Complex,n)) . (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: (unital_poly (F_Complex,n)) . 0 = - (1_ F_Complex) by Th38; set xn = (power F_Complex) . (x,n); set null = ((len F) -' 1) |-> (0. F_Complex); A11: len (((len F) -' 1) |-> (0. F_Complex)) = (len F) -' 1 by CARD_1:def_7; set tR2 = (((len F) -' 1) |-> (0. F_Complex)) ^ <*((power F_Complex) . (x,n))*>; set tR1 = <*(- (1_ F_Complex))*> ^ (((len F) -' 1) |-> (0. F_Complex)); A12: dom F = Seg (len F) by FINSEQ_1:def_3; reconsider R1 = <*(- (1_ F_Complex))*> ^ (((len F) -' 1) |-> (0. F_Complex)) as Tuple of len F, the carrier of F_Complex by A9; reconsider R1 = R1 as Element of (len F) -tuples_on the carrier of F_Complex by FINSEQ_2:131; reconsider R2 = (((len F) -' 1) |-> (0. F_Complex)) ^ <*((power F_Complex) . (x,n))*> as Tuple of len F, the carrier of F_Complex by A9; reconsider R2 = R2 as Element of (len F) -tuples_on the carrier of F_Complex by FINSEQ_2:131; A13: for i being Element of NAT st i in dom (((len F) -' 1) |-> (0. F_Complex)) holds (((len F) -' 1) |-> (0. F_Complex)) . i = 0. F_Complex proof let i be Element of NAT ; ::_thesis: ( i in dom (((len F) -' 1) |-> (0. F_Complex)) implies (((len F) -' 1) |-> (0. F_Complex)) . i = 0. F_Complex ) assume i in dom (((len F) -' 1) |-> (0. F_Complex)) ; ::_thesis: (((len F) -' 1) |-> (0. F_Complex)) . i = 0. F_Complex then i in Seg ((len F) -' 1) by FUNCOP_1:13; hence (((len F) -' 1) |-> (0. F_Complex)) . i = 0. F_Complex by FUNCOP_1:7; ::_thesis: verum end; A14: for i being Nat st i <> 1 & i in dom R1 holds R1 . i = 0. F_Complex proof let i be Nat; ::_thesis: ( i <> 1 & i in dom R1 implies R1 . i = 0. F_Complex ) assume that A15: i <> 1 and A16: i in dom R1 ; ::_thesis: R1 . i = 0. F_Complex A17: dom <*(- (1_ F_Complex))*> = Seg 1 by FINSEQ_1:def_8; now__::_thesis:_not_i_in_dom_<*(-_(1__F_Complex))*> assume i in dom <*(- (1_ F_Complex))*> ; ::_thesis: contradiction then ( 1 <= i & i <= 1 ) by A17, FINSEQ_1:1; hence contradiction by A15, XXREAL_0:1; ::_thesis: verum end; then consider j being Nat such that A18: j in dom (((len F) -' 1) |-> (0. F_Complex)) and A19: i = (len <*(- (1_ F_Complex))*>) + j by A16, FINSEQ_1:25; (((len F) -' 1) |-> (0. F_Complex)) . j = 0. F_Complex by A13, A18; hence R1 . i = 0. F_Complex by A18, A19, FINSEQ_1:def_7; ::_thesis: verum end; len ((((len F) -' 1) |-> (0. F_Complex)) ^ <*((power F_Complex) . (x,n))*>) = (len (((len F) -' 1) |-> (0. F_Complex))) + (len <*((power F_Complex) . (x,n))*>) by FINSEQ_1:22; then A20: len ((((len F) -' 1) |-> (0. F_Complex)) ^ <*((power F_Complex) . (x,n))*>) = len F by A11, A9, FINSEQ_1:39; A21: for i being Element of NAT st i in dom R2 & i <> len F holds R2 . i = 0. F_Complex proof let i be Element of NAT ; ::_thesis: ( i in dom R2 & i <> len F implies R2 . i = 0. F_Complex ) assume that A22: i in dom R2 and A23: i <> len F ; ::_thesis: R2 . i = 0. F_Complex 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 (((len F) -' 1) |-> (0. F_Complex)) by A11, FINSEQ_1:def_3; then R2 . i = (((len F) -' 1) |-> (0. F_Complex)) . i by FINSEQ_1:def_7; hence R2 . i = 0. F_Complex by A13, A26; ::_thesis: verum end; len R1 = len F by CARD_1:def_7; then A27: dom R1 = Seg (len F) by FINSEQ_1:def_3; len R2 = len F by CARD_1:def_7; then A28: dom R2 = Seg (len F) by FINSEQ_1:def_3; A29: R1 . 1 = - (1_ F_Complex) by FINSEQ_1:41; A30: len (R1 + R2) = len F by CARD_1:def_7; then A31: dom (R1 + R2) = Seg (len F) by FINSEQ_1:def_3; A32: R2 . (len F) = (power F_Complex) . (x,n) by A11, A9, FINSEQ_1:42; for k being Nat st k in dom (R1 + R2) holds (R1 + R2) . k = F . k proof let k be Nat; ::_thesis: ( k in dom (R1 + R2) implies (R1 + R2) . k = F . k ) assume A33: k in dom (R1 + R2) ; ::_thesis: (R1 + R2) . k = F . k A34: k in Seg (len F) by A30, A33, FINSEQ_1:def_3; A35: k in dom F by A31, A33, FINSEQ_1:def_3; A36: 1 <= k by A31, A33, FINSEQ_1:1; A37: (- (1_ F_Complex)) * (1_ F_Complex) = - (1_ F_Complex) by COMPLFLD:8; now__::_thesis:_(R1_+_R2)_._k_=_F_._k percases ( k = 1 or k <> 1 ) ; supposeA38: k = 1 ; ::_thesis: (R1 + R2) . k = F . k 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 = ((unital_poly (F_Complex,n)) . 0) * ((power F_Complex) . (x,0)) by A4, A1, A35, A38 .= - (1_ F_Complex) by A10, A37, GROUP_1:def_7 ; hence (R1 + R2) . k = F . k by A38, A39, COMPLFLD:7; ::_thesis: verum end; supposeA40: k <> 1 ; ::_thesis: (R1 + R2) . k = F . k now__::_thesis:_(R1_+_R2)_._k_=_F_._k percases ( k = len F or k <> len F ) ; supposeA41: k = len F ; ::_thesis: (R1 + R2) . k = F . k len F <> 0 by A3, A5, Th40; then A42: F . (len F) = ((unital_poly (F_Complex,n)) . ((len F) -' 1)) * ((power F_Complex) . (x,((len F) -' 1))) by A4, A12, FINSEQ_1:3 .= (1_ F_Complex) * ((power F_Complex) . (x,n)) by A8, Th38 .= (power F_Complex) . (x,n) by VECTSP_1:def_8 ; R1 . (len F) = 0. F_Complex by A6, A14, A27, A34, A41; then (R1 + R2) . (len F) = (0. F_Complex) + ((power F_Complex) . (x,n)) by A32, A33, A41, FVSUM_1:17 .= (power F_Complex) . (x,n) by COMPLFLD:7 ; hence (R1 + R2) . k = F . k by A41, A42; ::_thesis: verum end; supposeA43: k <> len F ; ::_thesis: (R1 + R2) . k = F . k A44: now__::_thesis:_not_k_-'_1_=_n assume k -' 1 = n ; ::_thesis: contradiction then k - 1 = n by A36, XREAL_1:233; hence contradiction by A7, A43; ::_thesis: verum 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 (unital_poly (F_Complex,n)) . (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 (R1 + R2) . k = F . k by A45, COMPLFLD:7; ::_thesis: verum end; end; end; hence (R1 + R2) . k = F . k ; ::_thesis: verum end; end; end; hence (R1 + R2) . k = F . k ; ::_thesis: verum end; then A47: R1 + R2 = F by A12, A31, FINSEQ_1:13; Sum (((len F) -' 1) |-> (0. F_Complex)) = 0. F_Complex by MATRIX_3:11; then ( Sum R1 = (- (1_ F_Complex)) + (0. F_Complex) & Sum R2 = (0. F_Complex) + ((power F_Complex) . (x,n)) ) 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 eval ((unital_poly (F_Complex,n)),x) = ((power F_Complex) . (x,n)) - 1 by A2, COMPLFLD:8; ::_thesis: verum end; theorem Th42: :: UNIROOTS:42 for n being non empty Element of NAT holds Roots (unital_poly (F_Complex,n)) = n -roots_of_1 proof let n be non empty Element of NAT ; ::_thesis: Roots (unital_poly (F_Complex,n)) = n -roots_of_1 now__::_thesis:_for_x_being_set_holds_ (_(_x_in_Roots_(unital_poly_(F_Complex,n))_implies_x_in_n_-roots_of_1_)_&_(_x_in_n_-roots_of_1_implies_x_in_Roots_(unital_poly_(F_Complex,n))_)_) set p = unital_poly (F_Complex,n); let x be set ; ::_thesis: ( ( x in Roots (unital_poly (F_Complex,n)) implies x in n -roots_of_1 ) & ( x in n -roots_of_1 implies x in Roots (unital_poly (F_Complex,n)) ) ) hereby ::_thesis: ( x in n -roots_of_1 implies x in Roots (unital_poly (F_Complex,n)) ) assume A1: x in Roots (unital_poly (F_Complex,n)) ; ::_thesis: x in n -roots_of_1 then reconsider x9 = x as Element of F_Complex ; x9 is_a_root_of unital_poly (F_Complex,n) by A1, POLYNOM5:def_9; then 0. F_Complex = eval ((unital_poly (F_Complex,n)),x9) by POLYNOM5:def_6 .= ((power F_Complex) . (x9,n)) - 1 by Th41 ; then x9 is CRoot of n, 1_ F_Complex by COMPLFLD:7, COMPLFLD:8, COMPLFLD:def_2; hence x in n -roots_of_1 ; ::_thesis: verum end; assume A2: x in n -roots_of_1 ; ::_thesis: x in Roots (unital_poly (F_Complex,n)) 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 ((unital_poly (F_Complex,n)),x9) = 0. F_Complex by Th41, COMPLFLD:7; then x9 is_a_root_of unital_poly (F_Complex,n) by POLYNOM5:def_6; hence x in Roots (unital_poly (F_Complex,n)) by POLYNOM5:def_9; ::_thesis: verum end; hence Roots (unital_poly (F_Complex,n)) = n -roots_of_1 by TARSKI:1; ::_thesis: verum end; theorem Th43: :: UNIROOTS:43 for n being Element of NAT for z being Element of F_Complex st z is Real holds ex x being Real st ( x = z & (power F_Complex) . (z,n) = x |^ n ) proof let n be Element of NAT ; ::_thesis: for z being Element of F_Complex st z is Real holds ex x being Real st ( x = z & (power F_Complex) . (z,n) = x |^ n ) let z be Element of F_Complex; ::_thesis: ( z is Real implies ex x being Real st ( x = z & (power F_Complex) . (z,n) = x |^ n ) ) assume z is Real ; ::_thesis: ex x being Real st ( x = z & (power F_Complex) . (z,n) = x |^ n ) then reconsider x = z as Real ; percases ( x = 0 or x <> 0 ) ; supposeA1: x = 0 ; ::_thesis: ex x being Real st ( x = z & (power F_Complex) . (z,n) = x |^ n ) then A2: z = 0. F_Complex by COMPLFLD:def_1; thus ex x being Real st ( x = z & (power F_Complex) . (z,n) = x |^ n ) ::_thesis: verum proof percases ( n = 0 or n > 0 ) ; supposeA3: n = 0 ; ::_thesis: ex x being Real st ( x = z & (power F_Complex) . (z,n) = x |^ n ) then (power F_Complex) . (z,n) = 1 by COMPLFLD:8, GROUP_1:def_7 .= x |^ n by A3, NEWTON:4 ; hence ex x being Real st ( x = z & (power F_Complex) . (z,n) = x |^ n ) ; ::_thesis: verum end; supposeA4: n > 0 ; ::_thesis: ex x being Real st ( x = z & (power F_Complex) . (z,n) = x |^ n ) 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 ex x being Real st ( x = z & (power F_Complex) . (z,n) = x |^ n ) ; ::_thesis: verum end; end; end; end; supposeA6: x <> 0 ; ::_thesis: ex x being Real st ( x = z & (power F_Complex) . (z,n) = x |^ n ) defpred S1[ Element of NAT ] means (power F_Complex) . (z,$1) = x |^ $1; A7: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A8: S1[n] ; ::_thesis: S1[n + 1] (power F_Complex) . (z,(n + 1)) = ((power F_Complex) . (z,n)) * z by GROUP_1:def_7 .= (x #Z n) * x by A8, PREPOWER:36 .= (x #Z n) * (x #Z 1) by PREPOWER:35 .= x #Z (n + 1) by A6, PREPOWER:44 .= x |^ (n + 1) by PREPOWER:36 ; hence S1[n + 1] ; ::_thesis: verum 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: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A9, A7); then (power F_Complex) . (z,n) = x |^ n ; hence ex x being Real st ( x = z & (power F_Complex) . (z,n) = x |^ n ) ; ::_thesis: verum end; end; end; theorem Th44: :: UNIROOTS:44 for n being non empty Element of NAT for x being Real ex y being Element of F_Complex st ( y = x & eval ((unital_poly (F_Complex,n)),y) = (x |^ n) - 1 ) proof let n be non empty Element of NAT ; ::_thesis: for x being Real ex y being Element of F_Complex st ( y = x & eval ((unital_poly (F_Complex,n)),y) = (x |^ n) - 1 ) let x be Real; ::_thesis: ex y being Element of F_Complex st ( y = x & eval ((unital_poly (F_Complex,n)),y) = (x |^ n) - 1 ) x in COMPLEX by XCMPLX_0:def_2; then reconsider y = x as Element of F_Complex by COMPLFLD:def_1; ex x2 being Real st ( x2 = y & (power F_Complex) . (y,n) = x2 |^ n ) by Th43; then eval ((unital_poly (F_Complex,n)),y) = (x |^ n) - 1 by Th41; hence ex y being Element of F_Complex st ( y = x & eval ((unital_poly (F_Complex,n)),y) = (x |^ n) - 1 ) ; ::_thesis: verum end; theorem Th45: :: UNIROOTS:45 for n being non empty Element of NAT holds BRoots (unital_poly (F_Complex,n)) = ((n -roots_of_1),1) -bag proof let n be non empty Element of NAT ; ::_thesis: BRoots (unital_poly (F_Complex,n)) = ((n -roots_of_1),1) -bag set p = unital_poly (F_Complex,n); A1: degree (BRoots (unital_poly (F_Complex,n))) = (len (unital_poly (F_Complex,n))) -' 1 by UPROOTS:59 .= (n + 1) -' 1 by Th40 .= n by NAT_D:34 ; A2: card (n -roots_of_1) = n by Th27; ( Roots (unital_poly (F_Complex,n)) = n -roots_of_1 & support (BRoots (unital_poly (F_Complex,n))) = Roots (unital_poly (F_Complex,n)) ) by Th42, UPROOTS:def_9; hence BRoots (unital_poly (F_Complex,n)) = ((n -roots_of_1),1) -bag by A1, A2, UPROOTS:13; ::_thesis: verum end; theorem Th46: :: UNIROOTS:46 for n being non empty Element of NAT holds unital_poly (F_Complex,n) = poly_with_roots (((n -roots_of_1),1) -bag) proof let n be non empty Element of NAT ; ::_thesis: unital_poly (F_Complex,n) = poly_with_roots (((n -roots_of_1),1) -bag) set p = unital_poly (F_Complex,n); len (unital_poly (F_Complex,n)) = n + 1 by Th40; then (unital_poly (F_Complex,n)) . ((len (unital_poly (F_Complex,n))) -' 1) = (unital_poly (F_Complex,n)) . 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 ; ::_thesis: verum end; theorem Th47: :: UNIROOTS:47 for n being non empty Element of NAT for i being Element of F_Complex st i is Integer holds eval ((unital_poly (F_Complex,n)),i) is Integer proof let n be non empty Element of NAT ; ::_thesis: for i being Element of F_Complex st i is Integer holds eval ((unital_poly (F_Complex,n)),i) is Integer let i be Element of F_Complex; ::_thesis: ( i is Integer implies eval ((unital_poly (F_Complex,n)),i) is Integer ) assume A1: i is Integer ; ::_thesis: eval ((unital_poly (F_Complex,n)),i) is Integer reconsider j = i as Integer by A1; i is Real by A1, XREAL_0:def_1; then ex y being Element of F_Complex st ( y = i & eval ((unital_poly (F_Complex,n)),y) = (j |^ n) - 1 ) by Th44; hence eval ((unital_poly (F_Complex,n)),i) is Integer ; ::_thesis: verum end; begin definition let d be non empty Nat; func cyclotomic_poly d -> Polynomial of F_Complex means :Def5: :: UNIROOTS:def 5 ex s being non empty finite Subset of F_Complex st ( s = { y where y is Element of (MultGroup F_Complex) : ord y = d } & it = poly_with_roots ((s,1) -bag) ); existence ex b1 being Polynomial of F_Complex ex s being non empty finite Subset of F_Complex st ( s = { y where y is Element of (MultGroup F_Complex) : ord y = d } & b1 = poly_with_roots ((s,1) -bag) ) proof set cMGFC = the carrier of (MultGroup F_Complex); reconsider d = d as non empty Element of NAT by ORDINAL1:def_12; defpred S1[ Element of the carrier of (MultGroup F_Complex)] means ord $1 = d; set s = { y where y is Element of the carrier of (MultGroup F_Complex) : S1[y] } ; set x = [**(cos (((2 * PI) * 1) / d)),(sin (((2 * PI) * 1) / d))**]; reconsider i = d as Integer ; [**(cos (((2 * PI) * 1) / d)),(sin (((2 * PI) * 1) / d))**] <> 0. F_Complex proof assume A1: [**(cos (((2 * PI) * 1) / d)),(sin (((2 * PI) * 1) / d))**] = 0. F_Complex ; ::_thesis: contradiction 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; ::_thesis: verum end; then A2: not [**(cos (((2 * PI) * 1) / d)),(sin (((2 * PI) * 1) / d))**] in {(0. F_Complex)} by TARSKI:def_1; the carrier of (MultGroup F_Complex) = NonZero F_Complex by Def1; then reconsider x = [**(cos (((2 * PI) * 1) / d)),(sin (((2 * PI) * 1) / d))**] as Element of the carrier of (MultGroup F_Complex) by A2, XBOOLE_0:def_5; A3: d -roots_of_1 = { y where y is Element of the carrier of (MultGroup F_Complex) : ord y divides d } by Th35; A4: { y where y is Element of the carrier of (MultGroup F_Complex) : S1[y] } c= d -roots_of_1 proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { y where y is Element of the carrier of (MultGroup F_Complex) : S1[y] } or a in d -roots_of_1 ) assume a in { y where y is Element of the carrier of (MultGroup F_Complex) : S1[y] } ; ::_thesis: a in d -roots_of_1 then ex y being Element of the carrier of (MultGroup F_Complex) st ( a = y & ord y = d ) ; hence a in d -roots_of_1 by A3; ::_thesis: verum 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 { y where y is Element of the carrier of (MultGroup F_Complex) : S1[y] } ; then reconsider s = { y where y is Element of the carrier of (MultGroup F_Complex) : S1[y] } as non empty finite Subset of F_Complex by A4, XBOOLE_1:1; take poly_with_roots ((s,1) -bag) ; ::_thesis: ex s being non empty finite Subset of F_Complex st ( s = { y where y is Element of (MultGroup F_Complex) : ord y = d } & poly_with_roots ((s,1) -bag) = poly_with_roots ((s,1) -bag) ) thus ex s being non empty finite Subset of F_Complex st ( s = { y where y is Element of (MultGroup F_Complex) : ord y = d } & poly_with_roots ((s,1) -bag) = poly_with_roots ((s,1) -bag) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Polynomial of F_Complex st ex s being non empty finite Subset of F_Complex st ( s = { y where y is Element of (MultGroup F_Complex) : ord y = d } & b1 = poly_with_roots ((s,1) -bag) ) & ex s being non empty finite Subset of F_Complex st ( s = { y where y is Element of (MultGroup F_Complex) : ord y = d } & b2 = poly_with_roots ((s,1) -bag) ) holds b1 = b2 ; end; :: deftheorem Def5 defines cyclotomic_poly UNIROOTS:def_5_:_ for d being non empty Nat for b2 being Polynomial of F_Complex holds ( b2 = cyclotomic_poly d iff ex s being non empty finite Subset of F_Complex st ( s = { y where y is Element of (MultGroup F_Complex) : ord y = d } & b2 = poly_with_roots ((s,1) -bag) ) ); theorem Th48: :: UNIROOTS:48 cyclotomic_poly 1 = <%(- (1_ F_Complex)),(1_ F_Complex)%> proof set cMGFC = the carrier of (MultGroup F_Complex); consider s being non empty finite Subset of F_Complex such that A1: s = { y where y is Element of the carrier of (MultGroup F_Complex) : ord y = 1 } and A2: cyclotomic_poly 1 = poly_with_roots ((s,1) -bag) by Def5; A3: 1 -roots_of_1 = { x where x is Element of the carrier of (MultGroup F_Complex) : ord x divides 1 } by Th35; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_s_implies_x_in_1_-roots_of_1_)_&_(_x_in_1_-roots_of_1_implies_x_in_s_)_) let x be set ; ::_thesis: ( ( x in s implies x in 1 -roots_of_1 ) & ( x in 1 -roots_of_1 implies x in s ) ) hereby ::_thesis: ( x in 1 -roots_of_1 implies x in s ) assume x in s ; ::_thesis: x in 1 -roots_of_1 then ex x1 being Element of the carrier of (MultGroup F_Complex) st ( x = x1 & ord x1 = 1 ) by A1; hence x in 1 -roots_of_1 by A3; ::_thesis: verum end; assume x in 1 -roots_of_1 ; ::_thesis: x in s then consider x1 being Element of the carrier of (MultGroup F_Complex) 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; ::_thesis: verum end; then s = 1 -roots_of_1 by TARSKI:1; hence cyclotomic_poly 1 = <%(- (1_ F_Complex)),(1_ F_Complex)%> by A2, Lm4, Th46; ::_thesis: verum end; theorem Th49: :: UNIROOTS:49 for n being non empty Element of NAT for f being FinSequence of the carrier of (Polynom-Ring F_Complex) st len f = n & ( for i being non empty Element of NAT st i in dom f holds ( ( not i divides n implies f . i = <%(1_ F_Complex)%> ) & ( i divides n implies f . i = cyclotomic_poly i ) ) ) holds unital_poly (F_Complex,n) = Product f proof set cMGFC = the carrier of (MultGroup F_Complex); let n be non empty Element of NAT ; ::_thesis: for f being FinSequence of the carrier of (Polynom-Ring F_Complex) st len f = n & ( for i being non empty Element of NAT st i in dom f holds ( ( not i divides n implies f . i = <%(1_ F_Complex)%> ) & ( i divides n implies f . i = cyclotomic_poly i ) ) ) holds unital_poly (F_Complex,n) = Product f let f be FinSequence of the carrier of (Polynom-Ring F_Complex); ::_thesis: ( len f = n & ( for i being non empty Element of NAT st i in dom f holds ( ( not i divides n implies f . i = <%(1_ F_Complex)%> ) & ( i divides n implies f . i = cyclotomic_poly i ) ) ) implies unital_poly (F_Complex,n) = Product f ) assume that A1: len f = n and A2: for i being non empty Element of NAT st i in dom f holds ( ( not i divides n implies f . i = <%(1_ F_Complex)%> ) & ( i divides n implies f . i = cyclotomic_poly i ) ) ; ::_thesis: unital_poly (F_Complex,n) = Product f defpred S1[ Nat, set ] means for fi being FinSequence of the carrier of (Polynom-Ring F_Complex) st fi = f | (Seg $1) holds $2 = Product fi; set nr1 = n -roots_of_1 ; deffunc H1( Nat) -> set = { y where y is Element of (MultGroup F_Complex) : ( y in n -roots_of_1 & ord y <= $1 ) } ; A3: now__::_thesis:_for_i_being_Nat_st_i_in_Seg_(len_f)_holds_ ex_x_being_Element_of_the_carrier_of_(Polynom-Ring_F_Complex)_st_S1[i,x] let i be Nat; ::_thesis: ( i in Seg (len f) implies ex x being Element of the carrier of (Polynom-Ring F_Complex) st S1[i,x] ) assume i in Seg (len f) ; ::_thesis: ex x being Element of the carrier of (Polynom-Ring F_Complex) st S1[i,x] 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 = Product fi; ::_thesis: S1[i,x] thus S1[i,x] ; ::_thesis: verum end; consider F being FinSequence of (Polynom-Ring F_Complex) such that dom F = Seg (len f) and A4: for i being Nat st i in Seg (len f) holds S1[i,F . i] from FINSEQ_1:sch_5(A3); defpred S2[ Element of NAT ] means ex t being finite Subset of F_Complex st ( t = H1($1) & F . $1 = poly_with_roots ((t,1) -bag) ); A5: now__::_thesis:_for_i_being_Element_of_NAT_holds_H1(i)_is_finite_Subset_of_F_Complex let i be Element of NAT ; ::_thesis: H1(i) is finite Subset of F_Complex H1(i) c= n -roots_of_1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H1(i) or x in n -roots_of_1 ) assume x in H1(i) ; ::_thesis: x in n -roots_of_1 then ex y being Element of the carrier of (MultGroup F_Complex) st ( x = y & y in n -roots_of_1 & ord y <= i ) ; hence x in n -roots_of_1 ; ::_thesis: verum end; hence H1(i) is finite Subset of F_Complex by XBOOLE_1:1; ::_thesis: verum end; then reconsider sB = H1(n) as finite Subset of F_Complex ; A6: n -roots_of_1 = { x where x is Element of (MultGroup F_Complex) : ord x divides n } by Th35; A7: for i being Element of NAT st 1 <= i & i < len f & S2[i] holds S2[i + 1] proof let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f & S2[i] implies S2[i + 1] ) assume that A8: 1 <= i and A9: i < len f and A10: S2[i] ; ::_thesis: S2[i + 1] reconsider fi = f | (Seg i) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18; i in Seg (len f) by A8, A9, FINSEQ_1:1; then A11: F . i = Product fi by A4; reconsider fi1 = f | (Seg (i + 1)) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18; A12: i + 1 <= len f by A9, NAT_1:13; then i + 1 = min ((i + 1),(len f)) by XXREAL_0:def_9; then A13: len fi1 = i + 1 by FINSEQ_2:21; 1 <= i + 1 by A8, NAT_1:13; then A14: i + 1 in Seg (len f) by A12, FINSEQ_1:1; then A15: i + 1 in dom f by FINSEQ_1:def_3; reconsider sB = H1(i + 1) as finite Subset of F_Complex by A5; take sB ; ::_thesis: ( sB = H1(i + 1) & F . (i + 1) = poly_with_roots ((sB,1) -bag) ) thus sB = H1(i + 1) ; ::_thesis: F . (i + 1) = poly_with_roots ((sB,1) -bag) set B = (sB,1) -bag ; consider sb being finite Subset of F_Complex such that A16: sb = H1(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 ((sb,1) -bag)) *' fi1d1p by A17, A11, POLYNOM3:def_10 ; percases ( not i + 1 divides n or i + 1 divides n ) ; supposeA20: not i + 1 divides n ; ::_thesis: F . (i + 1) = poly_with_roots ((sB,1) -bag) set eb = EmptyBag the carrier of F_Complex; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_sB_implies_x_in_sb_)_&_(_x_in_sb_implies_x_in_sB_)_) let x be set ; ::_thesis: ( ( x in sB implies x in sb ) & ( x in sb implies x in sB ) ) hereby ::_thesis: ( x in sb implies x in sB ) assume x in sB ; ::_thesis: x in sb then consider y being Element of (MultGroup F_Complex) such that A21: x = y and A22: y in n -roots_of_1 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; ::_thesis: verum end; assume x in sb ; ::_thesis: x in sB then consider y being Element of the carrier of (MultGroup F_Complex) such that A24: ( x = y & y in n -roots_of_1 ) and A25: ord y <= i by A16; ord y <= i + 1 by A25, NAT_1:12; hence x in sB by A24; ::_thesis: verum end; then A26: sB = sb by TARSKI:1; f . (i + 1) = <%(1_ F_Complex)%> by A2, A15, A20 .= poly_with_roots (EmptyBag the carrier of F_Complex) by UPROOTS:60 ; hence F . (i + 1) = (poly_with_roots ((sb,1) -bag)) *' (poly_with_roots (EmptyBag the carrier of F_Complex)) by A4, A14, A18, A19 .= poly_with_roots (((sb,1) -bag) + (EmptyBag the carrier of F_Complex)) by UPROOTS:64 .= poly_with_roots ((sB,1) -bag) by A26, PRE_POLY:53 ; ::_thesis: verum end; supposeA27: i + 1 divides n ; ::_thesis: F . (i + 1) = poly_with_roots ((sB,1) -bag) consider scb being non empty finite Subset of F_Complex such that A28: scb = { y where y is Element of the carrier of (MultGroup F_Complex) : ord y = i + 1 } and A29: cyclotomic_poly (i + 1) = poly_with_roots ((scb,1) -bag) by Def5; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_sB_implies_x_in_sb_\/_scb_)_&_(_x_in_sb_\/_scb_implies_x_in_sB_)_) let x be set ; ::_thesis: ( ( x in sB implies x in sb \/ scb ) & ( x in sb \/ scb implies b1 in sB ) ) hereby ::_thesis: ( x in sb \/ scb implies b1 in sB ) assume x in sB ; ::_thesis: x in sb \/ scb then consider y being Element of the carrier of (MultGroup F_Complex) such that A30: x = y and A31: y in n -roots_of_1 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; ::_thesis: verum end; assume A33: x in sb \/ scb ; ::_thesis: b1 in sB percases ( x in sb or x in scb ) by A33, XBOOLE_0:def_3; suppose x in sb ; ::_thesis: b1 in sB then consider y being Element of the carrier of (MultGroup F_Complex) such that A34: ( x = y & y in n -roots_of_1 ) and A35: ord y <= i by A16; ord y <= i + 1 by A35, NAT_1:12; hence x in sB by A34; ::_thesis: verum end; suppose x in scb ; ::_thesis: b1 in sB then consider y being Element of the carrier of (MultGroup F_Complex) such that A36: x = y and A37: ord y = i + 1 by A28; y in n -roots_of_1 by A6, A27, A37; hence x in sB by A36, A37; ::_thesis: verum end; end; end; then A38: sB = sb \/ scb by TARSKI:1; set cb = (scb,1) -bag ; A39: sb misses scb proof assume sb /\ scb <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then consider x being set such that A40: x in sb /\ scb by XBOOLE_0:def_1; x in scb by A40, XBOOLE_0:def_4; then A41: ex y2 being Element of the carrier of (MultGroup F_Complex) st ( x = y2 & ord y2 = i + 1 ) by A28; x in sb by A40, XBOOLE_0:def_4; then ex y1 being Element of the carrier of (MultGroup F_Complex) st ( x = y1 & y1 in n -roots_of_1 & ord y1 <= i ) by A16; hence contradiction by A41, NAT_1:13; ::_thesis: verum end; f . (i + 1) = poly_with_roots ((scb,1) -bag) by A2, A15, A27, A29; hence F . (i + 1) = (poly_with_roots ((sb,1) -bag)) *' (poly_with_roots ((scb,1) -bag)) by A4, A14, A18, A19 .= poly_with_roots (((sb,1) -bag) + ((scb,1) -bag)) by UPROOTS:64 .= poly_with_roots ((sB,1) -bag) by A38, A39, UPROOTS:10 ; ::_thesis: verum end; end; end; A42: 0 + 1 <= n by NAT_1:13; A43: S2[1] proof reconsider t = H1(1) as finite Subset of F_Complex by A5; take t ; ::_thesis: ( t = H1(1) & F . 1 = poly_with_roots ((t,1) -bag) ) thus t = H1(1) ; ::_thesis: F . 1 = poly_with_roots ((t,1) -bag) reconsider f1 = f | (Seg 1) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18; A44: ( 1 in dom f & 1 divides n ) by A1, A42, FINSEQ_3:25, NAT_D:6; A45: 1 in Seg (len f) by A1, A42, FINSEQ_1:1; then 1 in dom f by FINSEQ_1:def_3; then reconsider fd1 = f . 1 as Element of the carrier of (Polynom-Ring F_Complex) by FINSEQ_2:11; f1 = <*(f . 1)*> by A1, A42, Th1; then F . 1 = Product <*fd1*> by A4, A45 .= fd1 by FINSOP_1:11 .= cyclotomic_poly 1 by A2, A44 ; then consider sB being non empty finite Subset of F_Complex such that A46: sB = { y where y is Element of the carrier of (MultGroup F_Complex) : ord y = 1 } and A47: F . 1 = poly_with_roots ((sB,1) -bag) by Def5; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_H1(1)_implies_x_in_sB_)_&_(_x_in_sB_implies_x_in_H1(1)_)_) let x be set ; ::_thesis: ( ( x in H1(1) implies x in sB ) & ( x in sB implies x in H1(1) ) ) hereby ::_thesis: ( x in sB implies x in H1(1) ) assume x in H1(1) ; ::_thesis: x in sB then consider y being Element of the carrier of (MultGroup F_Complex) such that A48: x = y and A49: y in n -roots_of_1 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; ::_thesis: verum end; assume x in sB ; ::_thesis: x in H1(1) then consider y being Element of the carrier of (MultGroup F_Complex) such that A51: x = y and A52: ord y = 1 by A46; ord y divides n by A52, NAT_D:6; then y in n -roots_of_1 by A6; hence x in H1(1) by A51, A52; ::_thesis: verum end; hence F . 1 = poly_with_roots ((t,1) -bag) by A47, TARSKI:1; ::_thesis: verum end; for i being Element of NAT st 1 <= i & i <= len f holds S2[i] from INT_1:sch_7(A43, A7); then A53: ex t being finite Subset of F_Complex st ( t = H1( len f) & F . (len f) = poly_with_roots ((t,1) -bag) ) by A1, A42; set b = ((n -roots_of_1),1) -bag ; A54: f = f | (Seg (len f)) by FINSEQ_3:49; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_n_-roots_of_1_implies_x_in_sB_)_&_(_x_in_sB_implies_x_in_n_-roots_of_1_)_) let x be set ; ::_thesis: ( ( x in n -roots_of_1 implies x in sB ) & ( x in sB implies x in n -roots_of_1 ) ) hereby ::_thesis: ( x in sB implies x in n -roots_of_1 ) assume A55: x in n -roots_of_1 ; ::_thesis: x in sB then consider y being Element of (MultGroup F_Complex) such that A56: x = y and A57: ord y divides n by A6; ord y <= n by A57, NAT_D:7; hence x in sB by A55, A56; ::_thesis: verum end; assume x in sB ; ::_thesis: x in n -roots_of_1 then ex y being Element of (MultGroup F_Complex) st ( y = x & y in n -roots_of_1 & ord y <= n ) ; hence x in n -roots_of_1 ; ::_thesis: verum end; then A58: n -roots_of_1 = sB by TARSKI:1; thus unital_poly (F_Complex,n) = poly_with_roots (((n -roots_of_1),1) -bag) by Th46 .= Product f by A1, A4, A58, A53, A54, FINSEQ_1:3 ; ::_thesis: verum end; theorem Th50: :: UNIROOTS:50 for n being non empty Element of NAT ex f being FinSequence of the carrier of (Polynom-Ring F_Complex) ex p being Polynomial of F_Complex st ( p = Product f & dom f = Seg n & ( for i being non empty Element of NAT st i in Seg n holds ( ( ( not i divides n or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies f . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = (cyclotomic_poly n) *' p ) proof set cPRFC = the carrier of (Polynom-Ring F_Complex); let n be non empty Element of NAT ; ::_thesis: ex f being FinSequence of the carrier of (Polynom-Ring F_Complex) ex p being Polynomial of F_Complex st ( p = Product f & dom f = Seg n & ( for i being non empty Element of NAT st i in Seg n holds ( ( ( not i divides n or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies f . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = (cyclotomic_poly n) *' p ) defpred S1[ set , set ] means ex i being non empty Element of NAT st ( i = $1 & ( not i divides n implies $2 = <%(1_ F_Complex)%> ) & ( i divides n implies $2 = cyclotomic_poly i ) ); consider m being Nat such that A1: n = m + 1 by NAT_1:6; A2: for k being Element of NAT st k in Seg n holds ex x being Element of the carrier of (Polynom-Ring F_Complex) st S1[k,x] proof let k be Element of NAT ; ::_thesis: ( k in Seg n implies ex x being Element of the carrier of (Polynom-Ring F_Complex) st S1[k,x] ) assume k in Seg n ; ::_thesis: ex x being Element of the carrier of (Polynom-Ring F_Complex) st S1[k,x] then reconsider i = k as non empty Element of NAT by FINSEQ_1:1; percases ( not i divides n or i divides n ) ; supposeA3: not i divides n ; ::_thesis: ex x being Element of the carrier of (Polynom-Ring F_Complex) st S1[k,x] reconsider FC1 = <%(1_ F_Complex)%> as Element of the carrier of (Polynom-Ring F_Complex) by POLYNOM3:def_10; take FC1 ; ::_thesis: S1[k,FC1] take i ; ::_thesis: ( i = k & ( not i divides n implies FC1 = <%(1_ F_Complex)%> ) & ( i divides n implies FC1 = cyclotomic_poly i ) ) thus i = k ; ::_thesis: ( ( not i divides n implies FC1 = <%(1_ F_Complex)%> ) & ( i divides n implies FC1 = cyclotomic_poly i ) ) thus ( ( not i divides n implies FC1 = <%(1_ F_Complex)%> ) & ( i divides n implies FC1 = cyclotomic_poly i ) ) by A3; ::_thesis: verum end; supposeA4: i divides n ; ::_thesis: ex x being Element of the carrier of (Polynom-Ring F_Complex) st S1[k,x] reconsider FC1 = cyclotomic_poly i as Element of the carrier of (Polynom-Ring F_Complex) by POLYNOM3:def_10; take FC1 ; ::_thesis: S1[k,FC1] take i ; ::_thesis: ( i = k & ( not i divides n implies FC1 = <%(1_ F_Complex)%> ) & ( i divides n implies FC1 = cyclotomic_poly i ) ) thus i = k ; ::_thesis: ( ( not i divides n implies FC1 = <%(1_ F_Complex)%> ) & ( i divides n implies FC1 = cyclotomic_poly i ) ) thus ( ( not i divides n implies FC1 = <%(1_ F_Complex)%> ) & ( i divides n implies FC1 = cyclotomic_poly i ) ) by A4; ::_thesis: verum end; end; end; consider f being FinSequence of the carrier of (Polynom-Ring F_Complex) such that A5: dom f = Seg n and A6: for k being Element of NAT st k in Seg n holds S1[k,f /. k] from RECDEF_1:sch_17(A2); reconsider fm = f | (Seg m) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18; A7: len f = n by A5, FINSEQ_1:def_3; A8: now__::_thesis:_for_i_being_non_empty_Element_of_NAT_st_i_in_dom_f_holds_ (_(_not_i_divides_n_implies_f_._i_=_<%(1__F_Complex)%>_)_&_(_i_divides_n_implies_f_._i_=_cyclotomic_poly_i_)_) let i be non empty Element of NAT ; ::_thesis: ( i in dom f implies ( ( not i divides n implies f . i = <%(1_ F_Complex)%> ) & ( i divides n implies f . i = cyclotomic_poly i ) ) ) assume A9: i in dom f ; ::_thesis: ( ( not i divides n implies f . i = <%(1_ F_Complex)%> ) & ( i divides n implies f . i = cyclotomic_poly i ) ) then A10: i <= n by A5, FINSEQ_1:1; ( ex j being non empty Element of NAT st ( j = i & ( not j divides n implies f /. i = <%(1_ F_Complex)%> ) & ( j divides n implies f /. i = cyclotomic_poly j ) ) & 1 <= i ) by A5, A6, A9, FINSEQ_1:1; hence ( ( not i divides n implies f . i = <%(1_ F_Complex)%> ) & ( i divides n implies f . i = cyclotomic_poly i ) ) by A7, A10, FINSEQ_4:15; ::_thesis: verum end; reconsider FC1 = <%(1_ F_Complex)%> as Element of the carrier of (Polynom-Ring F_Complex) by POLYNOM3:def_10; <*FC1*> is FinSequence of the carrier of (Polynom-Ring F_Complex) ; then reconsider h = fm ^ <*<%(1_ F_Complex)%>*> as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:75; reconsider p = Product h as Polynomial of F_Complex by POLYNOM3:def_10; take h ; ::_thesis: ex p being Polynomial of F_Complex st ( p = Product h & dom h = Seg n & ( for i being non empty Element of NAT st i in Seg n holds ( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = (cyclotomic_poly n) *' p ) take p ; ::_thesis: ( p = Product h & dom h = Seg n & ( for i being non empty Element of NAT st i in Seg n holds ( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = (cyclotomic_poly n) *' p ) thus p = Product h ; ::_thesis: ( dom h = Seg n & ( for i being non empty Element of NAT st i in Seg n holds ( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = (cyclotomic_poly n) *' p ) 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 the carrier of (Polynom-Ring F_Complex) by POLYNOM3:def_10; reconsider fn = f | (Seg n) as FinSequence of the carrier of (Polynom-Ring F_Complex) 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; ::_thesis: ( ( for i being non empty Element of NAT st i in Seg n holds ( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = (cyclotomic_poly n) *' p ) A15: dom fm = Seg m by A7, A11, FINSEQ_1:17; thus for i being non empty Element of NAT st i in Seg n holds ( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) ::_thesis: unital_poly (F_Complex,n) = (cyclotomic_poly n) *' p proof let i be non empty Element of NAT ; ::_thesis: ( i in Seg n implies ( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) ) assume A16: i in Seg n ; ::_thesis: ( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) percases ( i in Seg m or not i in Seg m ) ; supposeA17: i in Seg m ; ::_thesis: ( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) 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 ( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) by A5, A1, A8, A16, A18, NAT_1:13; ::_thesis: verum end; suppose not i in Seg m ; ::_thesis: ( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) then ( not 1 <= i or not 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; ::_thesis: ( i divides n & i <> n implies h . i = cyclotomic_poly i ) thus ( i divides n & i <> n implies h . i = cyclotomic_poly i ) by A19, A20, XXREAL_0:1; ::_thesis: verum end; end; end; reconsider p1 = <%(1_ F_Complex)%> as Element of the carrier of (Polynom-Ring F_Complex) 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 unital_poly (F_Complex,n) = (cyclotomic_poly n) *' p by A21, A22, POLYNOM3:def_10; ::_thesis: verum end; theorem Th51: :: UNIROOTS:51 for d being non empty Element of NAT for i being Element of NAT holds ( ( (cyclotomic_poly d) . 0 = 1 or (cyclotomic_poly d) . 0 = - 1 ) & (cyclotomic_poly d) . i is integer ) proof deffunc H1( non empty Element of NAT ) -> Polynomial of F_Complex = cyclotomic_poly $1; set cPRFC = the carrier of (Polynom-Ring F_Complex); set cFC = the carrier of F_Complex; defpred S1[ non empty Element of NAT ] means ( ( H1($1) . 0 = 1 or H1($1) . 0 = - 1 ) & ( for i being Element of NAT holds H1($1) . i is integer ) ); A1: - (1_ F_Complex) = - 1 by COMPLFLD:2, COMPLFLD:8; A2: now__::_thesis:_for_k_being_non_empty_Element_of_NAT_st_(_for_n_being_non_empty_Element_of_NAT_st_n_<_k_holds_ S1[n]_)_holds_ S1[k] let k be non empty Element of NAT ; ::_thesis: ( ( for n being non empty Element of NAT st n < k holds S1[n] ) implies S1[b1] ) assume A3: for n being non empty Element of NAT st n < k holds S1[n] ; ::_thesis: S1[b1] A4: 1 <= k by Lm1; percases ( k = 1 or k > 1 ) by A4, XXREAL_0:1; supposeA5: k = 1 ; ::_thesis: S1[b1] now__::_thesis:_for_i_being_Element_of_NAT_holds_H1(k)_._i_is_integer let i be Element of NAT ; ::_thesis: H1(k) . b1 is integer percases ( i = 0 or i = 1 or i >= 2 ) by NAT_1:23; suppose i = 0 ; ::_thesis: H1(k) . b1 is integer hence H1(k) . i is integer by A1, A5, Th48, POLYNOM5:38; ::_thesis: verum end; suppose i = 1 ; ::_thesis: H1(k) . b1 is integer hence H1(k) . i is integer by A5, Th48, COMPLFLD:8, POLYNOM5:38; ::_thesis: verum end; suppose i >= 2 ; ::_thesis: H1(k) . b1 is integer hence H1(k) . i is integer by A5, Th48, COMPLFLD:7, POLYNOM5:38; ::_thesis: verum end; end; end; hence S1[k] by A1, A5, Th48, POLYNOM5:38; ::_thesis: verum end; supposeA6: k > 1 ; ::_thesis: S1[b1] consider f being FinSequence of the carrier of (Polynom-Ring F_Complex), p being Polynomial of F_Complex such that A7: p = Product f and A8: dom f = Seg k and A9: for i being non empty Element of NAT st i in Seg k holds ( ( ( not i divides k or i = k ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides k & i <> k implies f . i = H1(i) ) ) and A10: unital_poly (F_Complex,k) = (cyclotomic_poly k) *' p by Th50; defpred S2[ Nat, set ] means ex g being FinSequence of the carrier of (Polynom-Ring F_Complex) ex p being Polynomial of F_Complex st ( g = f | (Seg $1) & p = Product g & $2 = p & ( p . 0 = 1 or p . 0 = - 1 ) & ( for j being Element of NAT holds p . j is integer ) ); defpred S3[ Element of NAT ] means ( $1 in Seg (len f) implies ex x being set st S2[$1,x] ); A11: k = len f by A8, FINSEQ_1:def_3; A12: for l being Element of NAT st S3[l] holds S3[l + 1] proof let l be Element of NAT ; ::_thesis: ( S3[l] implies S3[l + 1] ) assume A13: S3[l] ; ::_thesis: S3[l + 1] assume A14: l + 1 in Seg (len f) ; ::_thesis: ex x being set st S2[l + 1,x] percases ( l = 0 or 0 < l ) ; supposeA15: l = 0 ; ::_thesis: ex x being set st S2[l + 1,x] reconsider fl1 = f . (l + 1) as Element of the carrier of (Polynom-Ring F_Complex) by A8, A11, A14, FINSEQ_2:11; reconsider g = f | (Seg (l + 1)) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18; reconsider p = Product g as Polynomial of F_Complex by POLYNOM3:def_10; <*> the carrier of (Polynom-Ring F_Complex) = f | (Seg 0) ; then g = (<*> the carrier of (Polynom-Ring F_Complex)) ^ <*(f . (l + 1))*> by A8, A11, A14, A15, FINSEQ_5:10 .= <*(f . (l + 1))*> by FINSEQ_1:34 ; then A16: p = fl1 by FINSOP_1:11; take p ; ::_thesis: S2[l + 1,p] take g ; ::_thesis: ex p being Polynomial of F_Complex st ( g = f | (Seg (l + 1)) & p = Product g & p = p & ( p . 0 = 1 or p . 0 = - 1 ) & ( for j being Element of NAT holds p . j is integer ) ) take p ; ::_thesis: ( g = f | (Seg (l + 1)) & p = Product g & p = p & ( p . 0 = 1 or p . 0 = - 1 ) & ( for j being Element of NAT holds p . j is integer ) ) thus ( g = f | (Seg (l + 1)) & p = Product g & p = p ) ; ::_thesis: ( ( p . 0 = 1 or p . 0 = - 1 ) & ( for j being Element of NAT holds p . j is integer ) ) 1 divides k by NAT_D:6; then A17: f . 1 = H1(1) by A6, A9, A11, A14, A15; hence ( p . 0 = 1 or p . 0 = - 1 ) by A1, A15, A16, Th48, POLYNOM5:38; ::_thesis: for j being Element of NAT holds p . j is integer let j be Element of NAT ; ::_thesis: p . j is integer thus p . j is integer ::_thesis: verum proof percases ( j = 0 or j = 1 or j >= 2 ) by NAT_1:23; suppose j = 0 ; ::_thesis: p . j is integer hence p . j is integer by A1, A15, A16, A17, Th48, POLYNOM5:38; ::_thesis: verum end; suppose j = 1 ; ::_thesis: p . j is integer hence p . j is integer by A15, A16, A17, Th48, COMPLFLD:8, POLYNOM5:38; ::_thesis: verum end; suppose j >= 2 ; ::_thesis: p . j is integer hence p . j is integer by A15, A16, A17, Th48, COMPLFLD:7, POLYNOM5:38; ::_thesis: verum end; end; end; end; supposeA18: 0 < l ; ::_thesis: ex x being set st S2[l + 1,x] ( l + 1 <= len f & l <= l + 1 ) by A14, FINSEQ_1:1, NAT_1:12; then A19: l <= len f by XXREAL_0:2; 0 + 1 <= l by A18, NAT_1:13; then consider x being set such that A20: S2[l,x] by A13, A19, FINSEQ_1:1; reconsider fl1 = f . (l + 1) as Element of the carrier of (Polynom-Ring F_Complex) by A8, A11, A14, FINSEQ_2:11; reconsider g1 = f | (Seg (l + 1)) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18; reconsider p1 = Product g1 as Polynomial of F_Complex by POLYNOM3:def_10; take p1 ; ::_thesis: S2[l + 1,p1] take g1 ; ::_thesis: ex p being Polynomial of F_Complex st ( g1 = f | (Seg (l + 1)) & p = Product g1 & p1 = p & ( p . 0 = 1 or p . 0 = - 1 ) & ( for j being Element of NAT holds p . j is integer ) ) take p1 ; ::_thesis: ( g1 = f | (Seg (l + 1)) & p1 = Product g1 & p1 = p1 & ( p1 . 0 = 1 or p1 . 0 = - 1 ) & ( for j being Element of NAT holds p1 . j is integer ) ) thus ( g1 = f | (Seg (l + 1)) & p1 = Product g1 & p1 = p1 ) ; ::_thesis: ( ( p1 . 0 = 1 or p1 . 0 = - 1 ) & ( for j being Element of NAT holds p1 . j is integer ) ) reconsider fl1p = fl1 as Polynomial of F_Complex by POLYNOM3:def_10; reconsider m1 = - 1 as Element of COMPLEX by XCMPLX_0:def_2; consider g being FinSequence of the carrier of (Polynom-Ring F_Complex), p being Polynomial of F_Complex such that A21: g = f | (Seg l) and A22: p = Product g and x = p and A23: ( p . 0 = 1 or p . 0 = - 1 ) and A24: for j being Element of NAT holds p . j is integer by A20; g1 = g ^ <*fl1*> by A8, A11, A14, A21, FINSEQ_5:10; then Product g1 = (Product g) * fl1 by GROUP_4:6; then A25: p1 = p *' fl1p by A22, POLYNOM3:def_10; thus ( ( p1 . 0 = 1 or p1 . 0 = - 1 ) & ( for j being Element of NAT holds p1 . j is integer ) ) ::_thesis: verum proof percases ( not l + 1 divides k or l + 1 = k or ( l + 1 divides k & l + 1 <> k ) ) ; suppose ( not l + 1 divides k or l + 1 = k ) ; ::_thesis: ( ( p1 . 0 = 1 or p1 . 0 = - 1 ) & ( for j being Element of NAT holds p1 . j is integer ) ) then A26: fl1p = <%(1_ F_Complex)%> by A9, A11, A14; consider r being FinSequence of F_Complex such that A27: len r = 0 + 1 and A28: p1 . 0 = Sum r and A29: for m being Element of NAT st m in dom r holds r . m = (p . (m -' 1)) * (fl1p . ((0 + 1) -' m)) by A25, POLYNOM3:def_9; 1 in dom r by A27, FINSEQ_3:25; then reconsider r1 = r . 1 as Element of F_Complex by FINSEQ_2:11; r = <*r1*> by A27, FINSEQ_1:40; then A30: p1 . 0 = r1 by A28, RLVECT_1:44; 1 in dom r by A27, FINSEQ_3:25; then A31: p1 . 0 = (p . (1 -' 1)) * (fl1p . ((0 + 1) -' 1)) by A29, A30 .= (p . ((0 + 1) -' 1)) * (fl1p . 0) by NAT_D:34 .= (p . 0) * (fl1p . 0) by NAT_D:34 .= (p . 0) * (1_ F_Complex) by A26, POLYNOM5:32 ; thus ( p1 . 0 = 1 or p1 . 0 = - 1 ) ::_thesis: for j being Element of NAT holds p1 . j is integer proof percases ( p . 0 = 1 or p . 0 = - 1 ) by A23; suppose p . 0 = 1 ; ::_thesis: ( p1 . 0 = 1 or p1 . 0 = - 1 ) hence ( p1 . 0 = 1 or p1 . 0 = - 1 ) by A31, COMPLFLD:8; ::_thesis: verum end; suppose p . 0 = - 1 ; ::_thesis: ( p1 . 0 = 1 or p1 . 0 = - 1 ) hence ( p1 . 0 = 1 or p1 . 0 = - 1 ) by A31, COMPLFLD:8; ::_thesis: verum end; end; end; let j be Element of NAT ; ::_thesis: p1 . j is integer consider r being FinSequence of F_Complex such that len r = j + 1 and A32: p1 . j = Sum r and A33: for m being Element of NAT st m in dom r holds r . m = (p . (m -' 1)) * (fl1p . ((j + 1) -' m)) by A25, POLYNOM3:def_9; for i being Element of NAT st i in dom r holds r . i is integer proof let i be Element of NAT ; ::_thesis: ( i in dom r implies r . i is integer ) reconsider pi1 = p . (i -' 1) as Integer by A24; set j1i = (j + 1) -' i; now__::_thesis:_(_(_(j_+_1)_-'_i_=_0_&_fl1p_._((j_+_1)_-'_i)_=_1_)_or_(_(j_+_1)_-'_i_>=_1_&_fl1p_._((j_+_1)_-'_i)_=_0_)_) A34: ( (j + 1) -' i = 0 or (j + 1) -' i >= 0 + 1 ) by NAT_1:13; percases ( (j + 1) -' i = 0 or (j + 1) -' i >= 1 ) by A34; case (j + 1) -' i = 0 ; ::_thesis: fl1p . ((j + 1) -' i) = 1 hence fl1p . ((j + 1) -' i) = 1 by A26, COMPLFLD:8, POLYNOM5:32; ::_thesis: verum end; case (j + 1) -' i >= 1 ; ::_thesis: fl1p . ((j + 1) -' i) = 0 hence fl1p . ((j + 1) -' i) = 0 by A26, COMPLFLD:7, POLYNOM5:32; ::_thesis: verum end; end; end; then reconsider fl1pj1i = fl1p . ((j + 1) -' i) as Integer ; assume i in dom r ; ::_thesis: r . i is integer then r . i = (p . (i -' 1)) * (fl1p . ((j + 1) -' i)) by A33 .= pi1 * fl1pj1i ; hence r . i is integer ; ::_thesis: verum end; hence p1 . j is integer by A32, Th4; ::_thesis: verum end; supposeA35: ( l + 1 divides k & l + 1 <> k ) ; ::_thesis: ( ( p1 . 0 = 1 or p1 . 0 = - 1 ) & ( for j being Element of NAT holds p1 . j is integer ) ) consider r being FinSequence of F_Complex such that A36: len r = 0 + 1 and A37: p1 . 0 = Sum r and A38: for m being Element of NAT st m in dom r holds r . m = (p . (m -' 1)) * (fl1p . ((0 + 1) -' m)) by A25, POLYNOM3:def_9; 1 in dom r by A36, FINSEQ_3:25; then reconsider r1 = r . 1 as Element of F_Complex by FINSEQ_2:11; r = <*r1*> by A36, FINSEQ_1:40; then A39: p1 . 0 = r1 by A37, RLVECT_1:44; 1 in dom r by A36, FINSEQ_3:25; then A40: p1 . 0 = (p . (1 -' 1)) * (fl1p . ((0 + 1) -' 1)) by A38, A39 .= (p . ((0 + 1) -' 1)) * (fl1p . 0) by NAT_D:34 .= (p . 0) * (fl1p . 0) by NAT_D:34 ; l + 1 <= k by A35, NAT_D:7; then A41: l + 1 < k by A35, XXREAL_0:1; A42: fl1p = H1(l + 1) by A9, A11, A14, A35; then reconsider fl1p0 = fl1p . 0 as Integer by A3, A41; A43: ( fl1p0 = 1 or fl1p0 = m1 ) by A3, A42, A41; thus ( p1 . 0 = 1 or p1 . 0 = - 1 ) ::_thesis: for j being Element of NAT holds p1 . j is integer proof percases ( p . 0 = 1 or p . 0 = - 1 ) by A23; suppose p . 0 = 1 ; ::_thesis: ( p1 . 0 = 1 or p1 . 0 = - 1 ) hence ( p1 . 0 = 1 or p1 . 0 = - 1 ) by A3, A42, A41, A40; ::_thesis: verum end; suppose p . 0 = - 1 ; ::_thesis: ( p1 . 0 = 1 or p1 . 0 = - 1 ) hence ( p1 . 0 = 1 or p1 . 0 = - 1 ) by A40, A43; ::_thesis: verum end; end; end; let j be Element of NAT ; ::_thesis: p1 . j is integer consider r being FinSequence of F_Complex such that len r = j + 1 and A44: p1 . j = Sum r and A45: for m being Element of NAT st m in dom r holds r . m = (p . (m -' 1)) * (fl1p . ((j + 1) -' m)) by A25, POLYNOM3:def_9; for i being Element of NAT st i in dom r holds r . i is integer proof let i be Element of NAT ; ::_thesis: ( i in dom r implies r . i is integer ) reconsider fl1pj1i = fl1p . ((j + 1) -' i) as Integer by A3, A42, A41; reconsider pi1 = p . (i -' 1) as Integer by A24; assume i in dom r ; ::_thesis: r . i is integer then r . i = (p . (i -' 1)) * (fl1p . ((j + 1) -' i)) by A45 .= pi1 * fl1pj1i ; hence r . i is integer ; ::_thesis: verum end; hence p1 . j is integer by A44, Th4; ::_thesis: verum end; end; end; end; end; end; defpred S4[ Nat] means H1(k) . $1 is integer ; A46: (0 + 1) -' 1 = 0 by NAT_D:34; A47: S3[ 0 ] by FINSEQ_1:1; for l being Element of NAT holds S3[l] from NAT_1:sch_1(A47, A12); then A48: for l being Nat st l in Seg (len f) holds ex x being set st S2[l,x] ; consider F being FinSequence such that dom F = Seg (len f) and A49: for i being Nat st i in Seg (len f) holds S2[i,F . i] from FINSEQ_1:sch_1(A48); consider g being FinSequence of the carrier of (Polynom-Ring F_Complex), p1 being Polynomial of F_Complex such that A50: ( g = f | (Seg k) & p1 = Product g ) and F . k = p1 and A51: ( p1 . 0 = 1 or p1 . 0 = - 1 ) and A52: for j being Element of NAT holds p1 . j is integer by A11, A49, FINSEQ_1:3; A53: p = p1 by A7, A11, A50, FINSEQ_3:49; A54: now__::_thesis:_for_m_being_Nat_st_(_for_n_being_Nat_st_n_<_m_holds_ S4[n]_)_holds_ S4[m] let m be Nat; ::_thesis: ( ( for n being Nat st n < m holds S4[n] ) implies S4[b1] ) reconsider m1 = m as Element of NAT by ORDINAL1:def_12; consider r being FinSequence of the carrier of F_Complex such that A55: len r = m + 1 and A56: (unital_poly (F_Complex,k)) . m = Sum r and A57: for l being Element of NAT st l in dom r holds r . l = (p . (l -' 1)) * (H1(k) . ((m1 + 1) -' l)) by A10, POLYNOM3:def_9; reconsider Src = Sum r as Element of COMPLEX by COMPLFLD:def_1; now__::_thesis:_Src_is_integer percases ( m1 = 0 or m1 = k or ( m1 <> 0 & m1 <> k ) ) ; suppose m1 = 0 ; ::_thesis: Src is integer hence Src is integer by A1, A56, Th38; ::_thesis: verum end; suppose m1 = k ; ::_thesis: Src is integer hence Src is integer by A56, Th38, COMPLFLD:8; ::_thesis: verum end; suppose ( m1 <> 0 & m1 <> k ) ; ::_thesis: Src is integer hence Src is integer by A56, Th39, COMPLFLD:7; ::_thesis: verum end; end; end; then reconsider Sr = Src as Integer ; A58: ((1,1) -cut r) ^ (((1 + 1),(len r)) -cut r) = r by A55, GRAPH_2:9, NAT_1:11; set s = ((1 + 1),(len r)) -cut r; reconsider Ssc = Sum (((1 + 1),(len r)) -cut r) as Element of COMPLEX by COMPLFLD:def_1; assume A59: for n being Nat st n < m holds S4[n] ; ::_thesis: S4[b1] now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(((1_+_1),(len_r))_-cut_r)_holds_ (((1_+_1),(len_r))_-cut_r)_._i_is_integer let i be Element of NAT ; ::_thesis: ( i in dom (((1 + 1),(len r)) -cut r) implies (((1 + 1),(len r)) -cut r) . b1 is integer ) assume A60: i in dom (((1 + 1),(len r)) -cut r) ; ::_thesis: (((1 + 1),(len r)) -cut r) . b1 is integer percases ( len r < 2 or 1 + 1 <= len r ) ; suppose len r < 2 ; ::_thesis: (((1 + 1),(len r)) -cut r) . b1 is integer then ((1 + 1),(len r)) -cut r = {} by GRAPH_2:def_1; hence (((1 + 1),(len r)) -cut r) . i is integer ; ::_thesis: verum end; supposeA61: 1 + 1 <= len r ; ::_thesis: (((1 + 1),(len r)) -cut r) . b1 is integer then A62: (len (((1 + 1),(len r)) -cut r)) + (1 + 1) = (len r) + 1 by GRAPH_2:def_1; percases ( m = 0 or m > 0 ) ; suppose m = 0 ; ::_thesis: (((1 + 1),(len r)) -cut r) . b1 is integer hence (((1 + 1),(len r)) -cut r) . i is integer by A55, A61; ::_thesis: verum end; supposeA63: m > 0 ; ::_thesis: (((1 + 1),(len r)) -cut r) . b1 is integer i <> 0 by A60, FINSEQ_3:25; then reconsider cpkmi = H1(k) . (m -' i) as Integer by A59, A63, NAT_2:9; reconsider ppi = p . i as Integer by A52, A53; i <> 0 by A60, FINSEQ_3:25; then consider i1 being Nat such that A64: i = i1 + 1 by NAT_1:6; A65: i <= len (((1 + 1),(len r)) -cut r) by A60, FINSEQ_3:25; then ( 1 <= i + 1 & i + 1 <= (len (((1 + 1),(len r)) -cut r)) + 1 ) by NAT_1:11, XREAL_1:6; then 1 + i in dom r by A62, FINSEQ_3:25; then A66: r . (1 + i) = (p . ((1 + i) -' 1)) * (H1(k) . ((m + 1) -' (1 + i))) by A57 .= (p . ((i + 1) -' 1)) * (H1(k) . (((m + 1) -' 1) -' i)) by NAT_2:30 .= (p . i) * (H1(k) . (((m + 1) -' 1) -' i)) by NAT_D:34 .= ppi * cpkmi by NAT_D:34 ; i1 < len (((1 + 1),(len r)) -cut r) by A65, A64, NAT_1:13; then (((1 + 1),(len r)) -cut r) . i = r . ((1 + 1) + i1) by A61, A64, GRAPH_2:def_1 .= r . (1 + i) by A64 ; hence (((1 + 1),(len r)) -cut r) . i is integer by A66; ::_thesis: verum end; end; end; end; end; then reconsider Ss = Ssc as Integer by Th4; A67: 1 <= len r by A55, NAT_1:11; then A68: 1 in dom r by FINSEQ_3:25; then reconsider r1 = r . 1 as Element of the carrier of F_Complex by FINSEQ_2:11; reconsider r1c = r1 as Element of COMPLEX by COMPLFLD:def_1; (1,1) -cut r = <*r1*> by A67, GRAPH_2:6; then Sum r = r1 + (Sum (((1 + 1),(len r)) -cut r)) by A58, FVSUM_1:72; then r1c = Sr - Ss ; then reconsider r1i = r1 as Integer ; A69: r1i = (p . (1 -' 1)) * (H1(k) . ((m + 1) -' 1)) by A57, A68 .= (p . 0) * (H1(k) . m1) by A46, NAT_D:34 ; percases ( p . 0 = 1 or p . 0 = - 1 ) by A7, A11, A50, A51, FINSEQ_3:49; suppose p . 0 = 1 ; ::_thesis: S4[b1] hence S4[m] by A69; ::_thesis: verum end; suppose p . 0 = - 1 ; ::_thesis: S4[b1] then r1 = (- (1_ F_Complex)) * (H1(k) . m1) by A69, COMPLFLD:2, COMPLFLD:8 .= - ((1_ F_Complex) * (H1(k) . m1)) by VECTSP_1:9 .= - (H1(k) . m1) by VECTSP_1:def_8 ; then 0. F_Complex = (- (H1(k) . m1)) + (- r1) by RLVECT_1:def_10 .= (- r1) - (H1(k) . m1) ; then - r1 = H1(k) . m by VECTSP_1:19; then - r1i = H1(k) . m by COMPLFLD:2; hence S4[m] ; ::_thesis: verum end; end; end; A70: for i being Nat holds S4[i] from NAT_1:sch_4(A54); consider r being FinSequence of the carrier of F_Complex such that A71: len r = 0 + 1 and A72: (unital_poly (F_Complex,k)) . 0 = Sum r and A73: for l being Element of NAT st l in dom r holds r . l = (p . (l -' 1)) * (H1(k) . ((0 + 1) -' l)) by A10, POLYNOM3:def_9; A74: 1 in dom r by A71, FINSEQ_3:25; then reconsider r1 = r . 1 as Element of the carrier of F_Complex by FINSEQ_2:11; r = <*r1*> by A71, FINSEQ_1:40; then A75: Sum r = r . 1 by RLVECT_1:44 .= (p . 0) * (H1(k) . 0) by A73, A46, A74 ; ( H1(k) . 0 = 1 or H1(k) . 0 = - 1 ) proof percases ( p . 0 = 1 or p . 0 = - 1 ) by A7, A11, A50, A51, FINSEQ_3:49; suppose p . 0 = 1 ; ::_thesis: ( H1(k) . 0 = 1 or H1(k) . 0 = - 1 ) hence ( H1(k) . 0 = 1 or H1(k) . 0 = - 1 ) by A1, A72, A75, Th38; ::_thesis: verum end; suppose p . 0 = - 1 ; ::_thesis: ( H1(k) . 0 = 1 or H1(k) . 0 = - 1 ) then - (1_ F_Complex) = (- (1_ F_Complex)) * (H1(k) . 0) by A1, A72, A75, Th38 .= - ((1_ F_Complex) * (H1(k) . 0)) by VECTSP_1:9 .= - (H1(k) . 0) by VECTSP_1:def_8 ; hence ( H1(k) . 0 = 1 or H1(k) . 0 = - 1 ) by COMPLFLD:8, RLVECT_1:18; ::_thesis: verum end; end; end; hence S1[k] by A70; ::_thesis: verum end; end; end; for d being non empty Element of NAT holds S1[d] from UNIROOTS:sch_1(A2); hence for d being non empty Element of NAT for i being Element of NAT holds ( ( (cyclotomic_poly d) . 0 = 1 or (cyclotomic_poly d) . 0 = - 1 ) & (cyclotomic_poly d) . i is integer ) ; ::_thesis: verum end; theorem Th52: :: UNIROOTS:52 for d being non empty Element of NAT for z being Element of F_Complex st z is Integer holds eval ((cyclotomic_poly d),z) is Integer proof let d be non empty Element of NAT ; ::_thesis: for z being Element of F_Complex st z is Integer holds eval ((cyclotomic_poly d),z) is Integer let z be Element of F_Complex; ::_thesis: ( z is Integer implies eval ((cyclotomic_poly d),z) is Integer ) assume A1: z is Integer ; ::_thesis: eval ((cyclotomic_poly d),z) is Integer set phi = cyclotomic_poly d; consider F being FinSequence of F_Complex such that A2: eval ((cyclotomic_poly d),z) = Sum F and len F = len (cyclotomic_poly d) and A3: for i being Element of NAT st i in dom F holds F . i = ((cyclotomic_poly d) . (i -' 1)) * ((power F_Complex) . (z,(i -' 1))) by POLYNOM4:def_2; for i being Element of NAT st i in dom F holds F . i is Integer proof let i be Element of NAT ; ::_thesis: ( i in dom F implies F . i is Integer ) assume i in dom F ; ::_thesis: F . i is Integer then A4: F . i = ((cyclotomic_poly d) . (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 = (cyclotomic_poly d) . (i -' 1) as Integer by Th51; F . i = i1 * i2 by A4; hence F . i is Integer ; ::_thesis: verum end; hence eval ((cyclotomic_poly d),z) is Integer by A2, Th14; ::_thesis: verum end; theorem Th53: :: UNIROOTS:53 for n, ni being non empty Element of NAT for f being FinSequence of the carrier of (Polynom-Ring F_Complex) for s being finite Subset of F_Complex st s = { y where y is Element of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } & dom f = Seg n & ( for i being non empty Element of NAT st i in dom f holds ( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) holds Product f = poly_with_roots ((s,1) -bag) proof set cMGFC = the carrier of (MultGroup F_Complex); set cPRFC = the carrier of (Polynom-Ring F_Complex); let n, ni be non empty Element of NAT ; ::_thesis: for f being FinSequence of the carrier of (Polynom-Ring F_Complex) for s being finite Subset of F_Complex st s = { y where y is Element of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } & dom f = Seg n & ( for i being non empty Element of NAT st i in dom f holds ( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) holds Product f = poly_with_roots ((s,1) -bag) let f be FinSequence of the carrier of (Polynom-Ring F_Complex); ::_thesis: for s being finite Subset of F_Complex st s = { y where y is Element of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } & dom f = Seg n & ( for i being non empty Element of NAT st i in dom f holds ( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) holds Product f = poly_with_roots ((s,1) -bag) let s be finite Subset of F_Complex; ::_thesis: ( s = { y where y is Element of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } & dom f = Seg n & ( for i being non empty Element of NAT st i in dom f holds ( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) implies Product f = poly_with_roots ((s,1) -bag) ) assume that A1: s = { y where y is Element of the carrier of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } and A2: dom f = Seg n and A3: for i being non empty Element of NAT st i in dom f holds ( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ; ::_thesis: Product f = poly_with_roots ((s,1) -bag) deffunc H1( Nat) -> set = { y where y is Element of the carrier of (MultGroup F_Complex) : ( y in s & ord y <= $1 ) } ; A4: now__::_thesis:_for_i_being_Element_of_NAT_holds_H1(i)_is_finite_Subset_of_F_Complex let i be Element of NAT ; ::_thesis: H1(i) is finite Subset of F_Complex H1(i) c= s proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H1(i) or x in s ) assume x in H1(i) ; ::_thesis: x in s then ex y being Element of the carrier of (MultGroup F_Complex) st ( x = y & y in s & ord y <= i ) ; hence x in s ; ::_thesis: verum end; hence H1(i) is finite Subset of F_Complex by XBOOLE_1:1; ::_thesis: verum end; then reconsider sB = H1(n) as finite Subset of F_Complex ; A5: len f = n by A2, FINSEQ_1:def_3; defpred S1[ Nat, set ] means for fi being FinSequence of the carrier of (Polynom-Ring F_Complex) st fi = f | (Seg $1) holds $2 = Product fi; A6: now__::_thesis:_for_i_being_Nat_st_i_in_Seg_(len_f)_holds_ ex_x_being_Element_of_the_carrier_of_(Polynom-Ring_F_Complex)_st_S1[i,x] let i be Nat; ::_thesis: ( i in Seg (len f) implies ex x being Element of the carrier of (Polynom-Ring F_Complex) st S1[i,x] ) assume i in Seg (len f) ; ::_thesis: ex x being Element of the carrier of (Polynom-Ring F_Complex) st S1[i,x] 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 = Product fi; ::_thesis: S1[i,x] thus S1[i,x] ; ::_thesis: verum end; consider F being FinSequence of the carrier of (Polynom-Ring F_Complex) such that dom F = Seg (len f) and A7: for i being Nat st i in Seg (len f) holds S1[i,F . i] from FINSEQ_1:sch_5(A6); defpred S2[ Element of NAT ] means ex t being finite Subset of F_Complex st ( t = H1($1) & F . $1 = poly_with_roots ((t,1) -bag) ); A8: for i being Element of NAT st 1 <= i & i < len f & S2[i] holds S2[i + 1] proof let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f & S2[i] implies S2[i + 1] ) assume that A9: 1 <= i and A10: i < len f and A11: S2[i] ; ::_thesis: S2[i + 1] reconsider fi = f | (Seg i) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18; i in Seg (len f) by A9, A10, FINSEQ_1:1; then A12: F . i = Product fi by A7; reconsider fi1 = f | (Seg (i + 1)) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18; A13: i + 1 <= len f by A10, NAT_1:13; then i + 1 = min ((i + 1),(len f)) by XXREAL_0:def_9; then A14: len fi1 = i + 1 by FINSEQ_2:21; reconsider sB = H1(i + 1) as finite Subset of F_Complex by A4; take sB ; ::_thesis: ( sB = H1(i + 1) & F . (i + 1) = poly_with_roots ((sB,1) -bag) ) thus sB = H1(i + 1) ; ::_thesis: F . (i + 1) = poly_with_roots ((sB,1) -bag) set B = (sB,1) -bag ; consider sb being finite Subset of F_Complex such that A15: sb = H1(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 ((sb,1) -bag)) *' fi1d1p by A12, A16, POLYNOM3:def_10; percases ( not i + 1 divides n or i + 1 divides ni or i + 1 = n or ( i + 1 divides n & not i + 1 divides ni & i + 1 <> n ) ) ; supposeA22: ( not i + 1 divides n or i + 1 divides ni or i + 1 = n ) ; ::_thesis: F . (i + 1) = poly_with_roots ((sB,1) -bag) A23: now__::_thesis:_for_x_being_set_holds_ (_(_x_in_sB_implies_x_in_sb_)_&_(_x_in_sb_implies_x_in_sB_)_) let x be set ; ::_thesis: ( ( x in sB implies x in sb ) & ( x in sb implies x in sB ) ) hereby ::_thesis: ( x in sb implies x in sB ) assume x in sB ; ::_thesis: x in sb then consider y being Element of (MultGroup F_Complex) such that A24: x = y and A25: y in s and A26: ord y <= i + 1 ; ex y1 being Element of the carrier of (MultGroup F_Complex) 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; ::_thesis: verum end; assume x in sb ; ::_thesis: x in sB then consider y being Element of (MultGroup F_Complex) such that A27: ( x = y & y in s ) and A28: ord y <= i by A15; ord y <= i + 1 by A28, NAT_1:12; hence x in sB by A27; ::_thesis: verum end; f . (i + 1) = <%(1_ F_Complex)%> by A3, A18, A22; then F . (i + 1) = poly_with_roots ((sb,1) -bag) by A20, A19, A21, UPROOTS:32 .= poly_with_roots ((sB,1) -bag) by A23, TARSKI:1 ; hence F . (i + 1) = poly_with_roots ((sB,1) -bag) ; ::_thesis: verum end; supposeA29: ( i + 1 divides n & not i + 1 divides ni & i + 1 <> n ) ; ::_thesis: F . (i + 1) = poly_with_roots ((sB,1) -bag) consider scb being non empty finite Subset of F_Complex such that A30: scb = { y where y is Element of the carrier of (MultGroup F_Complex) : ord y = i + 1 } and A31: cyclotomic_poly (i + 1) = poly_with_roots ((scb,1) -bag) by Def5; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_sB_implies_x_in_sb_\/_scb_)_&_(_x_in_sb_\/_scb_implies_x_in_sB_)_) let x be set ; ::_thesis: ( ( x in sB implies x in sb \/ scb ) & ( x in sb \/ scb implies b1 in sB ) ) hereby ::_thesis: ( x in sb \/ scb implies b1 in sB ) assume x in sB ; ::_thesis: x in sb \/ scb then consider y being Element of the carrier of (MultGroup F_Complex) 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; ::_thesis: verum end; assume A35: x in sb \/ scb ; ::_thesis: b1 in sB percases ( x in sb or x in scb ) by A35, XBOOLE_0:def_3; suppose x in sb ; ::_thesis: b1 in sB then consider y being Element of the carrier of (MultGroup F_Complex) 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; ::_thesis: verum end; suppose x in scb ; ::_thesis: b1 in sB then consider y being Element of the carrier of (MultGroup F_Complex) 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; ::_thesis: verum end; end; end; then A40: sB = sb \/ scb by TARSKI:1; set cb = (scb,1) -bag ; A41: sb misses scb proof assume sb /\ scb <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then consider x being set such that A42: x in sb /\ scb by XBOOLE_0:def_1; x in scb by A42, XBOOLE_0:def_4; then A43: ex y2 being Element of the carrier of (MultGroup F_Complex) st ( x = y2 & ord y2 = i + 1 ) by A30; x in sb by A42, XBOOLE_0:def_4; then ex y1 being Element of the carrier of (MultGroup F_Complex) st ( x = y1 & y1 in s & ord y1 <= i ) by A15; hence contradiction by A43, NAT_1:13; ::_thesis: verum end; f . (i + 1) = poly_with_roots ((scb,1) -bag) by A3, A18, A29, A31; then F . (i + 1) = (poly_with_roots ((sb,1) -bag)) *' (poly_with_roots ((scb,1) -bag)) by A7, A17, A19, A21 .= poly_with_roots (((sb,1) -bag) + ((scb,1) -bag)) by UPROOTS:64 .= poly_with_roots ((sB,1) -bag) by A40, A41, UPROOTS:10 ; hence F . (i + 1) = poly_with_roots ((sB,1) -bag) ; ::_thesis: verum end; end; end; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_s_implies_x_in_sB_)_&_(_x_in_sB_implies_x_in_s_)_) let x be set ; ::_thesis: ( ( x in s implies x in sB ) & ( x in sB implies x in s ) ) hereby ::_thesis: ( x in sB implies x in s ) assume A44: x in s ; ::_thesis: x in sB then consider y being Element of (MultGroup F_Complex) such that A45: x = y and A46: ord y divides n and not ord y divides ni and ord y <> n by A1; ord y <= n by A46, NAT_D:7; hence x in sB by A44, A45; ::_thesis: verum end; assume x in sB ; ::_thesis: x in s then ex y being Element of (MultGroup F_Complex) st ( y = x & y in s & ord y <= n ) ; hence x in s ; ::_thesis: verum end; then A47: s = sB by TARSKI:1; A48: 0 + 1 <= n by NAT_1:13; A49: S2[1] proof reconsider t = H1(1) as finite Subset of F_Complex by A4; take t ; ::_thesis: ( t = H1(1) & F . 1 = poly_with_roots ((t,1) -bag) ) thus t = H1(1) ; ::_thesis: F . 1 = poly_with_roots ((t,1) -bag) reconsider f1 = f | (Seg 1) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18; A50: 1 in dom f by A5, A48, FINSEQ_3:25; A51: 1 divides ni by NAT_D:6; now__::_thesis:_t_is_empty assume not t is empty ; ::_thesis: contradiction then consider x being set such that A52: x in t by XBOOLE_0:def_1; consider y being Element of the carrier of (MultGroup F_Complex) such that x = y and A53: y in s and A54: ord y <= 1 by A52; consider y1 being Element of the carrier of (MultGroup F_Complex) 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__::_thesis:_not_ord_y1_=_0 assume ord y1 = 0 ; ::_thesis: contradiction then ex u being Nat st n = 0 * u by A56, NAT_D:def_3; hence contradiction ; ::_thesis: verum end; then 0 + 1 <= ord y1 by NAT_1:13; hence contradiction by A51, A54, A55, A57, XXREAL_0:1; ::_thesis: verum 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 the carrier of (Polynom-Ring F_Complex) 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 F . 1 = poly_with_roots ((t,1) -bag) by A58, UPROOTS:60; ::_thesis: verum end; for i being Element of NAT st 1 <= i & i <= len f holds S2[i] from INT_1:sch_7(A49, A8); then ( f = f | (Seg (len f)) & ex S being finite Subset of F_Complex st ( S = H1( len f) & F . (len f) = poly_with_roots ((S,1) -bag) ) ) by A5, A48, FINSEQ_3:49; hence Product f = poly_with_roots ((s,1) -bag) by A5, A7, A47, FINSEQ_1:3; ::_thesis: verum end; theorem Th54: :: UNIROOTS:54 for n, ni being non empty Element of NAT st ni < n & ni divides n holds ex f being FinSequence of the carrier of (Polynom-Ring F_Complex) ex p being Polynomial of F_Complex st ( p = Product f & dom f = Seg n & ( for i being non empty Element of NAT st i in Seg n holds ( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)) *' p ) proof set cMGFC = the carrier of (MultGroup F_Complex); set cPRFC = the carrier of (Polynom-Ring F_Complex); let n, ni be non empty Element of NAT ; ::_thesis: ( ni < n & ni divides n implies ex f being FinSequence of the carrier of (Polynom-Ring F_Complex) ex p being Polynomial of F_Complex st ( p = Product f & dom f = Seg n & ( for i being non empty Element of NAT st i in Seg n holds ( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)) *' p ) ) assume that A1: ni < n and A2: ni divides n ; ::_thesis: ex f being FinSequence of the carrier of (Polynom-Ring F_Complex) ex p being Polynomial of F_Complex st ( p = Product f & dom f = Seg n & ( for i being non empty Element of NAT st i in Seg n holds ( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)) *' p ) set rbp = { y where y is Element of the carrier of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } ; { y where y is Element of the carrier of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } c= n -roots_of_1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { y where y is Element of the carrier of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } or x in n -roots_of_1 ) assume x in { y where y is Element of the carrier of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } ; ::_thesis: x in n -roots_of_1 then ex y being Element of the carrier of (MultGroup F_Complex) st ( x = y & ord y divides n & not ord y divides ni & ord y <> n ) ; hence x in n -roots_of_1 by Th34; ::_thesis: verum end; then reconsider rbp = { y where y is Element of the carrier of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } as finite Subset of F_Complex by XBOOLE_1:1; A3: n -roots_of_1 c= the carrier of (MultGroup F_Complex) by Th32; set bp = (rbp,1) -bag ; defpred S1[ set , set ] means ex d being non empty Nat st ( $1 = d & ( ( not d divides n or d divides ni or d = n ) implies $2 = <%(1_ F_Complex)%> ) & ( d divides n & not d divides ni & d <> n implies $2 = cyclotomic_poly d ) ); A4: now__::_thesis:_for_i_being_Nat_st_i_in_Seg_n_holds_ ex_x_being_Element_of_the_carrier_of_(Polynom-Ring_F_Complex)_st_S1[i,x] let i be Nat; ::_thesis: ( i in Seg n implies ex x being Element of the carrier of (Polynom-Ring F_Complex) st S1[x,b2] ) assume A5: i in Seg n ; ::_thesis: ex x being Element of the carrier of (Polynom-Ring F_Complex) st S1[x,b2] then A6: not i is empty by FINSEQ_1:1; percases ( not i divides n or i divides ni or i = n or ( i divides n & not i divides ni & i <> n ) ) ; supposeA7: ( not i divides n or i divides ni or i = n ) ; ::_thesis: ex x being Element of the carrier of (Polynom-Ring F_Complex) st S1[x,b2] <%(1_ F_Complex)%> is Element of the carrier of (Polynom-Ring F_Complex) by POLYNOM3:def_10; hence ex x being Element of the carrier of (Polynom-Ring F_Complex) st S1[i,x] by A6, A7; ::_thesis: verum end; supposeA8: ( i divides n & not i divides ni & i <> n ) ; ::_thesis: ex x being Element of the carrier of (Polynom-Ring F_Complex) st S1[x,b2] reconsider i9 = i as non empty Element of NAT by A5, FINSEQ_1:1; cyclotomic_poly i9 is Element of the carrier of (Polynom-Ring F_Complex) by POLYNOM3:def_10; hence ex x being Element of the carrier of (Polynom-Ring F_Complex) st S1[i,x] by A8; ::_thesis: verum end; end; end; consider f being FinSequence of the carrier of (Polynom-Ring F_Complex) such that A9: dom f = Seg n and A10: for i being Nat st i in Seg n holds S1[i,f . i] from FINSEQ_1:sch_5(A4); A11: now__::_thesis:_for_i_being_non_empty_Element_of_NAT_st_i_in_Seg_n_holds_ (_(_(_not_i_divides_n_or_i_divides_ni_or_i_=_n_)_implies_f_._i_=_<%(1__F_Complex)%>_)_&_(_i_divides_n_&_not_i_divides_ni_&_i_<>_n_implies_f_._i_=_cyclotomic_poly_i_)_) let i be non empty Element of NAT ; ::_thesis: ( i in Seg n implies ( ( ( 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 ) ) ) assume i in Seg n ; ::_thesis: ( ( ( 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 ) ) then ex d being non empty Nat st ( i = d & ( ( not d divides n or d divides ni or d = n ) implies f . i = <%(1_ F_Complex)%> ) & ( d divides n & not d divides ni & d <> n implies f . i = cyclotomic_poly d ) ) by A10; hence ( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ; ::_thesis: verum end; then Product f = poly_with_roots ((rbp,1) -bag) by A9, Th53; then reconsider p = Product f as Polynomial of F_Complex ; take f ; ::_thesis: ex p being Polynomial of F_Complex st ( p = Product f & dom f = Seg n & ( for i being non empty Element of NAT st i in Seg n holds ( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)) *' p ) take p ; ::_thesis: ( p = Product f & dom f = Seg n & ( for i being non empty Element of NAT st i in Seg n holds ( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)) *' p ) thus p = Product f ; ::_thesis: ( dom f = Seg n & ( for i being non empty Element of NAT st i in Seg n holds ( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)) *' p ) thus dom f = Seg n by A9; ::_thesis: ( ( for i being non empty Element of NAT st i in Seg n holds ( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)) *' p ) thus for i being non empty Element of NAT st i in Seg n holds ( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) by A11; ::_thesis: unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)) *' p set b = ((n -roots_of_1),1) -bag ; set bi = ((ni -roots_of_1),1) -bag ; consider rbn being non empty finite Subset of F_Complex such that A12: rbn = { y where y is Element of the carrier of (MultGroup F_Complex) : 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 <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then consider x being set such that A14: x in (ni -roots_of_1) /\ rbn by XBOOLE_0:def_1; x in rbn by A14, XBOOLE_0:def_4; then A15: ex y1 being Element of the carrier of (MultGroup F_Complex) st ( x = y1 & ord y1 = n ) by A12; x in ni -roots_of_1 by A14, XBOOLE_0:def_4; then ex y being Element of the carrier of (MultGroup F_Complex) st ( x = y & ord y divides ni ) by Th36; hence contradiction by A1, A15, NAT_D:7; ::_thesis: verum end; then A16: (((ni -roots_of_1),1) -bag) + ((rbn,1) -bag) = (((ni -roots_of_1) \/ rbn),1) -bag by UPROOTS:10; set rbibn = (ni -roots_of_1) \/ rbn; reconsider rbibn = (ni -roots_of_1) \/ rbn as finite Subset of F_Complex ; A17: ni -roots_of_1 c= n -roots_of_1 by A2, Th28; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_n_-roots_of_1_implies_x_in_rbibn_\/_rbp_)_&_(_x_in_rbibn_\/_rbp_implies_x_in_n_-roots_of_1_)_) let x be set ; ::_thesis: ( ( x in n -roots_of_1 implies x in rbibn \/ rbp ) & ( x in rbibn \/ rbp implies b1 in n -roots_of_1 ) ) hereby ::_thesis: ( x in rbibn \/ rbp implies b1 in n -roots_of_1 ) assume A18: x in n -roots_of_1 ; ::_thesis: x in rbibn \/ rbp then reconsider y = x as Element of the carrier of (MultGroup F_Complex) by A3; A19: ord y divides n by A18, Th34; percases ( ord y = n or ( ord y <> n & not ord y divides ni ) or ( ord y <> n & ord y divides ni ) ) ; suppose ord y = n ; ::_thesis: x in rbibn \/ rbp 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; ::_thesis: verum end; suppose ( ord y <> n & not ord y divides ni ) ; ::_thesis: x in rbibn \/ rbp then y in rbp by A19; hence x in rbibn \/ rbp by XBOOLE_0:def_3; ::_thesis: verum end; suppose ( ord y <> n & ord y divides ni ) ; ::_thesis: x in rbibn \/ rbp 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; ::_thesis: verum end; end; end; assume x in rbibn \/ rbp ; ::_thesis: b1 in n -roots_of_1 then A20: ( x in rbibn or x in rbp ) by XBOOLE_0:def_3; percases ( x in ni -roots_of_1 or x in rbn or x in rbp ) by A20, XBOOLE_0:def_3; suppose x in ni -roots_of_1 ; ::_thesis: b1 in n -roots_of_1 hence x in n -roots_of_1 by A17; ::_thesis: verum end; suppose x in rbn ; ::_thesis: b1 in n -roots_of_1 then ex y being Element of the carrier of (MultGroup F_Complex) st ( x = y & ord y = n ) by A12; hence x in n -roots_of_1 by Th34; ::_thesis: verum end; suppose x in rbp ; ::_thesis: b1 in n -roots_of_1 then ex y being Element of the carrier of (MultGroup F_Complex) st ( x = y & ord y divides n & not ord y divides ni & ord y <> n ) ; hence x in n -roots_of_1 by Th34; ::_thesis: verum end; end; end; then A21: n -roots_of_1 = rbibn \/ rbp by TARSKI:1; set bibn = (rbibn,1) -bag ; A22: unital_poly (F_Complex,ni) = poly_with_roots (((ni -roots_of_1),1) -bag) by Th46; rbibn misses rbp proof assume rbibn /\ rbp <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then consider x being set such that A23: x in rbibn /\ rbp by XBOOLE_0:def_1; x in rbp by A23, XBOOLE_0:def_4; then A24: ex y being Element of the carrier of (MultGroup F_Complex) 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; percases ( x in ni -roots_of_1 or x in rbn ) by A25, XBOOLE_0:def_3; suppose x in ni -roots_of_1 ; ::_thesis: contradiction then ex y being Element of the carrier of (MultGroup F_Complex) st ( x = y & ord y divides ni ) by Th36; hence contradiction by A24; ::_thesis: verum end; suppose x in rbn ; ::_thesis: contradiction then ex y being Element of the carrier of (MultGroup F_Complex) st ( x = y & ord y = n ) by A12; hence contradiction by A24; ::_thesis: verum end; end; end; then A26: ((n -roots_of_1),1) -bag = ((rbibn,1) -bag) + ((rbp,1) -bag) by A21, UPROOTS:10; unital_poly (F_Complex,n) = poly_with_roots (((n -roots_of_1),1) -bag) by Th46 .= (poly_with_roots ((rbibn,1) -bag)) *' (poly_with_roots ((rbp,1) -bag)) by A26, UPROOTS:64 .= ((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)) *' (poly_with_roots ((rbp,1) -bag)) by A13, A16, A22, UPROOTS:64 ; hence unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)) *' p by A9, A11, Th53; ::_thesis: verum end; theorem Th55: :: UNIROOTS:55 for i being Integer for c being Element of F_Complex for f being FinSequence of the carrier of (Polynom-Ring F_Complex) for p being Polynomial of F_Complex st p = Product f & c = i & ( for i being non empty Element of NAT holds ( not i in dom f or 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; ::_thesis: for c being Element of F_Complex for f being FinSequence of the carrier of (Polynom-Ring F_Complex) for p being Polynomial of F_Complex st p = Product f & c = i & ( for i being non empty Element of NAT holds ( not i in dom f or f . i = <%(1_ F_Complex)%> or f . i = cyclotomic_poly i ) ) holds eval (p,c) is integer let c be Element of F_Complex; ::_thesis: for f being FinSequence of the carrier of (Polynom-Ring F_Complex) for p being Polynomial of F_Complex st p = Product f & c = i & ( for i being non empty Element of NAT holds ( not i in dom f or f . i = <%(1_ F_Complex)%> or f . i = cyclotomic_poly i ) ) holds eval (p,c) is integer let f be FinSequence of the carrier of (Polynom-Ring F_Complex); ::_thesis: for p being Polynomial of F_Complex st p = Product f & c = i & ( for i being non empty Element of NAT holds ( not i in dom f or f . i = <%(1_ F_Complex)%> or f . i = cyclotomic_poly i ) ) holds eval (p,c) is integer let p be Polynomial of F_Complex; ::_thesis: ( p = Product f & c = i & ( for i being non empty Element of NAT holds ( not i in dom f or f . i = <%(1_ F_Complex)%> or f . i = cyclotomic_poly i ) ) implies eval (p,c) is integer ) assume that A2: p = Product f and A3: c = i and A4: for i being non empty Element of NAT holds ( not i in dom f or f . i = <%(1_ F_Complex)%> or f . i = cyclotomic_poly i ) ; ::_thesis: eval (p,c) is integer A5: eval ((1_. F_Complex),c) = 1 by COMPLFLD:8, POLYNOM4:18; percases ( len f = 0 or 0 < len f ) ; suppose len f = 0 ; ::_thesis: eval (p,c) is integer 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 eval (p,c) is integer by A5, POLYNOM3:def_10; ::_thesis: verum end; supposeA6: 0 < len f ; ::_thesis: eval (p,c) is integer defpred S1[ Nat, set ] means for fi being FinSequence of the carrier of (Polynom-Ring F_Complex) st fi = f | (Seg $1) holds $2 = Product fi; A7: f = f | (Seg (len f)) by FINSEQ_3:49; A8: now__::_thesis:_for_i_being_Nat_st_i_in_Seg_(len_f)_holds_ ex_x_being_Element_of_the_carrier_of_(Polynom-Ring_F_Complex)_st_S1[i,x] let i be Nat; ::_thesis: ( i in Seg (len f) implies ex x being Element of the carrier of (Polynom-Ring F_Complex) st S1[i,x] ) assume i in Seg (len f) ; ::_thesis: ex x being Element of the carrier of (Polynom-Ring F_Complex) st S1[i,x] 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 = Product fi; ::_thesis: S1[i,x] thus S1[i,x] ; ::_thesis: verum end; consider F being FinSequence of the carrier of (Polynom-Ring F_Complex) such that dom F = Seg (len f) and A9: for i being Nat st i in Seg (len f) holds S1[i,F . i] from FINSEQ_1:sch_5(A8); defpred S2[ Element of NAT ] means ex r being Polynomial of F_Complex st ( r = F . $1 & eval (r,c) is integer ); A10: now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<_len_f_&_S2[i]_holds_ S2[i_+_1] let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f & S2[i] implies S2[i + 1] ) assume that A11: 1 <= i and A12: i < len f ; ::_thesis: ( S2[i] implies S2[i + 1] ) 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: S2[i] ; ::_thesis: S2[i + 1] 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 S2[i + 1] ::_thesis: verum proof reconsider epfi = eval (pfi,c), efi1d1p = eval (fi1d1p,c) as Element of COMPLEX by COMPLFLD:def_1; now__::_thesis:_eval_(fi1d1p,c)_is_integer reconsider i1 = i + 1 as non empty Element of NAT ; percases ( f . i1 = <%(1_ F_Complex)%> or f . i1 = cyclotomic_poly i1 ) by A4, A17; suppose f . i1 = <%(1_ F_Complex)%> ; ::_thesis: eval (fi1d1p,c) is integer hence eval (fi1d1p,c) is integer by A5, A1, FINSEQ_1:4, FUNCT_1:49; ::_thesis: verum end; suppose f . i1 = cyclotomic_poly i1 ; ::_thesis: eval (fi1d1p,c) is integer hence eval (fi1d1p,c) is integer by A3, A19, Th52; ::_thesis: verum end; end; end; then reconsider iefi1d1p = efi1d1p as Integer ; reconsider iepfi = epfi as Integer by A9, A18, A13; take pfi1 ; ::_thesis: ( pfi1 = F . (i + 1) & eval (pfi1,c) is integer ) thus pfi1 = F . (i + 1) by A9, A16; ::_thesis: eval (pfi1,c) is integer pfi1 = pfi *' fi1d1p by A20, POLYNOM3:def_10; then eval (pfi1,c) = (eval (pfi,c)) * (eval (fi1d1p,c)) by POLYNOM4:24 .= iepfi * iefi1d1p ; hence eval (pfi1,c) is integer ; ::_thesis: verum end; end; A21: 0 + 1 <= len f by A6, NAT_1:13; then A22: 1 in Seg (len f) by FINSEQ_1:1; A23: S2[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 = fd1 as Polynomial of F_Complex by POLYNOM3:def_10; take fd1 ; ::_thesis: ( fd1 = F . 1 & eval (fd1,c) is integer ) f1 = <*(f . 1)*> by A21, Th1; hence fd1 = Product f1 by FINSOP_1:11 .= F . 1 by A9, A22 ; ::_thesis: eval (fd1,c) is integer percases ( f . 1 = <%(1_ F_Complex)%> or f . 1 = cyclotomic_poly 1 ) by A4, A24; suppose f . 1 = <%(1_ F_Complex)%> ; ::_thesis: eval (fd1,c) is integer hence eval (fd1,c) is integer by A1, COMPLFLD:8, POLYNOM4:18; ::_thesis: verum end; suppose f . 1 = cyclotomic_poly 1 ; ::_thesis: eval (fd1,c) is integer hence eval (fd1,c) is integer by A3, Th52; ::_thesis: verum end; end; end; for i being Element of NAT st 1 <= i & i <= len f holds S2[i] from INT_1:sch_7(A23, A10); then ex r being Polynomial of F_Complex st ( r = F . (len f) & eval (r,c) is integer ) by A21; hence eval (p,c) is integer by A2, A6, A9, A7, FINSEQ_1:3; ::_thesis: verum end; end; end; theorem Th56: :: UNIROOTS:56 for n being non empty Element of NAT for j, k, q being Integer for qc being Element of F_Complex st qc = q & j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) holds j divides k proof let n be non empty Element of NAT ; ::_thesis: for j, k, q being Integer for qc being Element of F_Complex st qc = q & j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) holds j divides k let j, k, q be Integer; ::_thesis: for qc being Element of F_Complex st qc = q & j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) holds j divides k let qc be Element of F_Complex; ::_thesis: ( qc = q & j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) implies j divides k ) assume that A1: qc = q and A2: j = eval ((cyclotomic_poly n),qc) and A3: k = eval ((unital_poly (F_Complex,n)),qc) ; ::_thesis: j divides k set jfc = eval ((cyclotomic_poly n),qc); percases ( n = 1 or n > 1 ) by NAT_1:53; suppose n = 1 ; ::_thesis: j divides k hence j divides k by A2, A3, Th48, POLYNOM5:def_4; ::_thesis: verum end; supposeA4: n > 1 ; ::_thesis: j divides k set eup1fc = eval ((unital_poly (F_Complex,1)),qc); reconsider eup1 = eval ((unital_poly (F_Complex,1)),qc) as Integer by A1, Th47; consider f being FinSequence of the carrier of (Polynom-Ring F_Complex), p being Polynomial of F_Complex such that A5: p = Product f and A6: ( dom f = Seg n & ( for i being non empty Element of NAT st i in Seg n holds ( ( ( not i divides n or i divides 1 or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides 1 & i <> n implies f . i = cyclotomic_poly i ) ) ) ) and A7: unital_poly (F_Complex,n) = ((unital_poly (F_Complex,1)) *' (cyclotomic_poly n)) *' p by A4, Th54, NAT_D:6; set epfc = eval (p,qc); now__::_thesis:_for_i_being_non_empty_Element_of_NAT_holds_ (_not_i_in_dom_f_or_f_._i_=_<%(1__F_Complex)%>_or_f_._i_=_cyclotomic_poly_i_) let i be non empty Element of NAT ; ::_thesis: ( not i in dom f or f . b1 = <%(1_ F_Complex)%> or f . b1 = cyclotomic_poly b1 ) assume A8: i in dom f ; ::_thesis: ( f . b1 = <%(1_ F_Complex)%> or f . b1 = cyclotomic_poly b1 ) percases ( not i divides n or i divides 1 or i = n or ( i divides n & not i divides 1 & i <> n ) ) ; suppose ( not i divides n or i divides 1 or i = n ) ; ::_thesis: ( f . b1 = <%(1_ F_Complex)%> or f . b1 = cyclotomic_poly b1 ) hence ( f . i = <%(1_ F_Complex)%> or f . i = cyclotomic_poly i ) by A6, A8; ::_thesis: verum end; suppose ( i divides n & not i divides 1 & i <> n ) ; ::_thesis: ( f . b1 = <%(1_ F_Complex)%> or f . b1 = cyclotomic_poly b1 ) hence ( f . i = <%(1_ F_Complex)%> or f . i = cyclotomic_poly i ) by A6, A8; ::_thesis: verum end; end; end; then reconsider ep = eval (p,qc) as Integer by A1, A5, Th55; k = (eval (((unital_poly (F_Complex,1)) *' (cyclotomic_poly n)),qc)) * (eval (p,qc)) by A3, A7, POLYNOM4:24; then k = ((eval ((unital_poly (F_Complex,1)),qc)) * (eval ((cyclotomic_poly n),qc))) * (eval (p,qc)) by POLYNOM4:24; then k = (eup1 * ep) * j by A2; hence j divides k by INT_1:def_3; ::_thesis: verum end; end; end; theorem Th57: :: UNIROOTS:57 for n, ni being non empty Element of NAT for q being Integer st ni < n & ni divides n holds for qc being Element of F_Complex st qc = q holds for j, k, l being Integer st j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) holds j divides k div l proof let n, ni be non empty Element of NAT ; ::_thesis: for q being Integer st ni < n & ni divides n holds for qc being Element of F_Complex st qc = q holds for j, k, l being Integer st j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) holds j divides k div l let q be Integer; ::_thesis: ( ni < n & ni divides n implies for qc being Element of F_Complex st qc = q holds for j, k, l being Integer st j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) holds j divides k div l ) assume A1: ( ni < n & ni divides n ) ; ::_thesis: for qc being Element of F_Complex st qc = q holds for j, k, l being Integer st j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) holds j divides k div l set ttt = (unital_poly (F_Complex,ni)) *' (cyclotomic_poly n); consider f being FinSequence of the carrier of (Polynom-Ring F_Complex), p being Polynomial of F_Complex such that A2: p = Product f and A3: ( dom f = Seg n & ( for i being non empty Element of NAT st i in Seg n holds ( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) ) and A4: unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)) *' p by A1, Th54; A5: now__::_thesis:_for_i_being_non_empty_Element_of_NAT_holds_ (_not_i_in_dom_f_or_f_._i_=_<%(1__F_Complex)%>_or_f_._i_=_cyclotomic_poly_i_) let i be non empty Element of NAT ; ::_thesis: ( not i in dom f or f . b1 = <%(1_ F_Complex)%> or f . b1 = cyclotomic_poly b1 ) assume A6: i in dom f ; ::_thesis: ( f . b1 = <%(1_ F_Complex)%> or f . b1 = cyclotomic_poly b1 ) percases ( not i divides n or i divides ni or i = n or ( i divides n & not i divides ni & i <> n ) ) ; suppose ( not i divides n or i divides ni or i = n ) ; ::_thesis: ( f . b1 = <%(1_ F_Complex)%> or f . b1 = cyclotomic_poly b1 ) hence ( f . i = <%(1_ F_Complex)%> or f . i = cyclotomic_poly i ) by A3, A6; ::_thesis: verum end; suppose ( i divides n & not i divides ni & i <> n ) ; ::_thesis: ( f . b1 = <%(1_ F_Complex)%> or f . b1 = cyclotomic_poly b1 ) hence ( f . i = <%(1_ F_Complex)%> or f . i = cyclotomic_poly i ) by A3, A6; ::_thesis: verum end; end; end; let qc be Element of F_Complex; ::_thesis: ( qc = q implies for j, k, l being Integer st j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) holds j divides k div l ) assume qc = q ; ::_thesis: for j, k, l being Integer st j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) holds j divides k div l then eval (p,qc) is integer by A2, A5, Th55; then consider m being Integer such that A7: m = eval (p,qc) ; let j, k, l be Integer; ::_thesis: ( j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) implies j divides k div l ) assume A8: ( j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) ) ; ::_thesis: j divides k div l 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 (((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)),qc)) * (eval (p,qc)) by A4, POLYNOM4:24; then A9: k = (lcf * jcf) * mcf by A8, A7, POLYNOM4:24 .= (l * j) * m ; now__::_thesis:_j_divides_k_div_l percases ( l <> 0 or l = 0 ) ; supposeA10: l <> 0 ; ::_thesis: j divides k div l 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 j divides k div l by INT_1:def_3; ::_thesis: verum end; suppose l = 0 ; ::_thesis: j divides k div l then k div l = 0 by INT_1:48; hence j divides k div l by INT_2:12; ::_thesis: verum end; end; end; hence j divides k div l ; ::_thesis: verum end; theorem :: UNIROOTS:58 for n, q being non empty Element of NAT for qc being Element of F_Complex st qc = q holds for j being Integer st j = eval ((cyclotomic_poly n),qc) holds j divides (q |^ n) - 1 proof let n, q be non empty Element of NAT ; ::_thesis: for qc being Element of F_Complex st qc = q holds for j being Integer st j = eval ((cyclotomic_poly n),qc) holds j divides (q |^ n) - 1 let qc be Element of F_Complex; ::_thesis: ( qc = q implies for j being Integer st j = eval ((cyclotomic_poly n),qc) holds j divides (q |^ n) - 1 ) assume A1: qc = q ; ::_thesis: for j being Integer st j = eval ((cyclotomic_poly n),qc) holds j divides (q |^ n) - 1 A2: ex y1 being Element of F_Complex st ( y1 = q & eval ((unital_poly (F_Complex,n)),y1) = (q |^ n) - 1 ) by Th44; let j be Integer; ::_thesis: ( j = eval ((cyclotomic_poly n),qc) implies j divides (q |^ n) - 1 ) assume j = eval ((cyclotomic_poly n),qc) ; ::_thesis: j divides (q |^ n) - 1 hence j divides (q |^ n) - 1 by A1, A2, Th56; ::_thesis: verum end; theorem :: UNIROOTS:59 for n, ni, q being non empty Element of NAT st ni < n & ni divides n holds for qc being Element of F_Complex st qc = q holds for j being Integer st j = eval ((cyclotomic_poly n),qc) holds j divides ((q |^ n) - 1) div ((q |^ ni) - 1) proof let n, ni, q be non empty Element of NAT ; ::_thesis: ( ni < n & ni divides n implies for qc being Element of F_Complex st qc = q holds for j being Integer st j = eval ((cyclotomic_poly n),qc) holds j divides ((q |^ n) - 1) div ((q |^ ni) - 1) ) assume A1: ( ni < n & ni divides n ) ; ::_thesis: for qc being Element of F_Complex st qc = q holds for j being Integer st j = eval ((cyclotomic_poly n),qc) holds j divides ((q |^ n) - 1) div ((q |^ ni) - 1) let qc be Element of F_Complex; ::_thesis: ( qc = q implies for j being Integer st j = eval ((cyclotomic_poly n),qc) holds j divides ((q |^ n) - 1) div ((q |^ ni) - 1) ) assume A2: qc = q ; ::_thesis: for j being Integer st j = eval ((cyclotomic_poly n),qc) holds j divides ((q |^ n) - 1) div ((q |^ ni) - 1) A3: ( ex y1 being Element of F_Complex st ( y1 = q & eval ((unital_poly (F_Complex,n)),y1) = (q |^ n) - 1 ) & ex y2 being Element of F_Complex st ( y2 = q & eval ((unital_poly (F_Complex,ni)),y2) = (q |^ ni) - 1 ) ) by Th44; let j be Integer; ::_thesis: ( j = eval ((cyclotomic_poly n),qc) implies j divides ((q |^ n) - 1) div ((q |^ ni) - 1) ) assume j = eval ((cyclotomic_poly n),qc) ; ::_thesis: j divides ((q |^ n) - 1) div ((q |^ ni) - 1) hence j divides ((q |^ n) - 1) div ((q |^ ni) - 1) by A1, A2, A3, Th57; ::_thesis: verum end; theorem :: UNIROOTS:60 for n being non empty Element of NAT st 1 < n holds for q being Element of NAT st 1 < q holds for qc being Element of F_Complex st qc = q holds for i being Integer st i = eval ((cyclotomic_poly n),qc) holds abs i > q - 1 proof set MGFC = MultGroup F_Complex; set cMGFC = the carrier of (MultGroup F_Complex); let n be non empty Element of NAT ; ::_thesis: ( 1 < n implies for q being Element of NAT st 1 < q holds for qc being Element of F_Complex st qc = q holds for i being Integer st i = eval ((cyclotomic_poly n),qc) holds abs i > q - 1 ) assume A1: 1 < n ; ::_thesis: for q being Element of NAT st 1 < q holds for qc being Element of F_Complex st qc = q holds for i being Integer st i = eval ((cyclotomic_poly n),qc) holds abs i > q - 1 consider S being non empty finite Subset of F_Complex such that A2: S = { y where y is Element of the carrier of (MultGroup F_Complex) : 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 ; ::_thesis: ( 1 < q implies for qc being Element of F_Complex st qc = q holds for i being Integer st i = eval ((cyclotomic_poly n),qc) holds abs i > q - 1 ) assume A4: 1 < q ; ::_thesis: for qc being Element of F_Complex st qc = q holds for i being Integer st i = eval ((cyclotomic_poly n),qc) holds abs i > q - 1 let qc be Element of F_Complex; ::_thesis: ( qc = q implies for i being Integer st i = eval ((cyclotomic_poly n),qc) holds abs i > q - 1 ) assume A5: qc = q ; ::_thesis: for i being Integer st i = eval ((cyclotomic_poly n),qc) holds abs i > q - 1 deffunc H1( set ) -> Element of REAL = |.(qc - (fs /. $1)).|; consider p1 being FinSequence such that A6: ( len p1 = len fs & ( for i being Nat st i in dom p1 holds p1 . i = H1(i) ) ) from FINSEQ_1:sch_2(); A7: for i being Element of NAT for c being Element of F_Complex st i in dom p1 & c = (canFS S) . i holds p1 . i = |.(qc - c).| proof let i be Element of NAT ; ::_thesis: for c being Element of F_Complex st i in dom p1 & c = (canFS S) . i holds p1 . i = |.(qc - c).| let c be Element of F_Complex; ::_thesis: ( i in dom p1 & c = (canFS S) . i implies p1 . i = |.(qc - c).| ) assume that A8: i in dom p1 and A9: c = (canFS S) . i ; ::_thesis: p1 . i = |.(qc - c).| i in dom fs by A6, A8, FINSEQ_3:29; then fs /. i = (canFS S) . i by PARTFUN1:def_6; hence p1 . i = |.(qc - c).| by A6, A8, A9; ::_thesis: verum end; for x being set st x in rng p1 holds x in REAL proof let x be set ; ::_thesis: ( x in rng p1 implies x in REAL ) assume x in rng p1 ; ::_thesis: x in REAL then consider i being Nat such that A10: i in dom p1 and A11: p1 . i = x by FINSEQ_2:10; i in dom fs by A6, A10, FINSEQ_3:29; then fs /. i = (canFS S) . i by PARTFUN1:def_6; then x = |.(qc - (fs /. i)).| by A7, A10, A11; hence x in REAL ; ::_thesis: verum end; then rng p1 c= REAL by TARSKI:def_3; then reconsider ps = p1 as non empty FinSequence of REAL by A6, FINSEQ_1:def_4; len fs = card S by UPROOTS:3; then A12: |.(eval ((cyclotomic_poly n),qc)).| = Product ps by A3, A6, A7, Th3; A13: rng fs = S by FUNCT_2:def_3; A14: for i being Element of NAT st i in dom ps holds ps . i > q - 1 proof let i be Element of NAT ; ::_thesis: ( i in dom ps implies ps . i > q - 1 ) assume A15: i in dom ps ; ::_thesis: ps . i > q - 1 i in dom fs by A6, A15, FINSEQ_3:29; then fs /. i = (canFS S) . i by PARTFUN1:def_6; then A16: ps . i = |.([**q,0**] - (fs /. i)).| by A5, A7, A15; A17: i in dom fs by A6, A15, FINSEQ_3:29; then fs . i in rng fs by FUNCT_1:3; then fs /. i in rng fs by A17, PARTFUN1:def_6; then A18: ex y being Element of (MultGroup F_Complex) st ( fs /. i = y & ord y = n ) by A2, A13; A19: now__::_thesis:_not_fs_/._i_=_[**1,0**] assume A20: fs /. i = [**1,0**] ; ::_thesis: contradiction 1_ (MultGroup F_Complex) = [**1,0**] by Th17, COMPLFLD:8; hence contradiction by A1, A18, A20, GROUP_1:42; ::_thesis: verum end; fs /. i in n -roots_of_1 by A18, Th34; then |.(fs /. i).| = 1 by Th23; hence ps . i > q - 1 by A4, A16, A19, Th6; ::_thesis: verum 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; ::_thesis: ( i = eval ((cyclotomic_poly n),qc) implies abs i > q - 1 ) reconsider x = q - 1 as Real by XREAL_0:def_1; assume i = eval ((cyclotomic_poly n),qc) ; ::_thesis: abs i > q - 1 then abs i > x by A21, A12, A14, Th7; hence abs i > q - 1 ; ::_thesis: verum end;