:: 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;
*