:: UNIROOTS semantic presentation

theorem Th1: :: UNIROOTS:1

for n being Nat holds
( n = 0 or n = 1 or n >= 2 )

proof end;

Lm1: for k being Nat holds
( not k is empty iff 1 <= k )

proof end;

scheme :: UNIROOTS:sch 1
CompIndNE{ P₁[ non empty Nat] } :

for k being non empty Nat holds P₁[k]

provided

A1: for k being non empty Nat st ( for n being non empty Nat st n < k holds
P₁[n] ) holds
P₁[k]

proof end;

theorem Th2: :: UNIROOTS:2

for f being FinSequence st 1 <= len f holds
f | (Seg 1) = <*(f . 1)*>

proof end;

Lm2: for f being FinSequence
for n, i being Nat st i <= n holds
(f | (Seg n)) | (Seg i) = f | (Seg i)

proof end;

theorem Th3: :: UNIROOTS:3

for f being FinSequence of F_Complex
for g being FinSequence of REAL st len f = len g & ( for i being Nat st i in dom f holds
|.(f /. i).| = g . i ) holds
|.(Product f).| = Product g

proof end;

theorem Th4: :: UNIROOTS:4

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 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 end;

theorem Th5: :: UNIROOTS:5

for f being FinSequence of F_Complex st ( for i being Nat st i in dom f holds
f . i is integer ) holds
Sum f is integer

proof end;

theorem :: UNIROOTS:6

canceled;

theorem Th7: :: UNIROOTS:7

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 ) by COMPLFLD:3, COMPLFLD:6;

theorem Th8: :: UNIROOTS:8

for q being Real st q is Integer & q > 0 holds
for r being Element of F_Complex st |.r.| = 1 & r <> [**1,0**] holds
|.([**q,0**] - r).| > q - 1

proof end;

theorem Th9: :: UNIROOTS:9

for ps being non empty FinSequence of REAL
for x being Real st x >= 1 & ( for i being Nat st i in dom ps holds
ps . i > x ) holds
Product ps > x

proof end;

theorem Th10: :: UNIROOTS:10

for n being Nat holds 1. F_Complex = (power F_Complex ) . (1. F_Complex ),n

proof end;

theorem Th11: :: UNIROOTS:11

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

proof end;

theorem Th12: :: UNIROOTS:12

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

proof end;

theorem Th13: :: UNIROOTS:13

for n, i, j being 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 end;

theorem Th14: :: UNIROOTS:14

for L being non empty unital associative HGrStr
for x being Element of L
for n, m being Nat holds (power L) . x,(n * m) = (power L) . ((power L) . x,n),m

proof end;

theorem Th15: :: UNIROOTS:15

for n being Nat
for x being Element of F_Complex st x is Integer holds
(power F_Complex ) . x,n is Integer

proof end;

theorem Th16: :: UNIROOTS:16

for F being FinSequence of F_Complex st ( for i being Nat st i in dom F holds
F . i is Integer ) holds
Sum F is Integer

proof end;

theorem Th17: :: UNIROOTS:17

for a being real number st 0 <= a & a < 2 * PI & cos a = 1 holds
a = 0

proof end;

Lm3: Z3 is finite
by GROUP_1:def 14, MOD_2:def 23;

registration

cluster finite doubleLoopStr ;
existence by Lm3, MOD_2:37;
cluster finite doubleLoopStr ;
existence by Lm3, MOD_2:37;

end;

definition

let R be Skew-Field;
func MultGroup R -> strict Group means :Def1: :: UNIROOTS:def 1
( the carrier of it = the carrier of R \ {(0. R)} & the mult of it = the mult of R || the carrier of it );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def1 defines MultGroup UNIROOTS:def 1 :

theorem :: UNIROOTS:18

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

proof end;

theorem Th19: :: UNIROOTS:19

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 end;

theorem Th20: :: UNIROOTS:20

for R being Skew-Field holds 1. R = 1. (MultGroup R)

proof end;

registration

let R be finite Skew-Field;
cluster MultGroup R -> strict finite ;
correctness

proof end;

end;

theorem :: UNIROOTS:21

for R being finite Skew-Field holds ord (MultGroup R) = (card the carrier of R) - 1

proof end;

theorem Th22: :: UNIROOTS:22

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 end;

theorem :: UNIROOTS:23

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

proof end;

definition

let n be non empty Nat;
func n -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

proof end;

end;

:: deftheorem defines -roots_of_1 UNIROOTS:def 2 :

theorem Th24: :: UNIROOTS:24

for n being non empty 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 end;

theorem Th25: :: UNIROOTS:25

for n being non empty Nat holds 1. F_Complex in n -roots_of_1

proof end;

theorem Th26: :: UNIROOTS:26

for n being non empty Nat
for x being Element of F_Complex st x in n -roots_of_1 holds
|.x.| = 1

proof end;

theorem Th27: :: UNIROOTS:27

for n being non empty Nat
for x being Element of F_Complex holds
( x in n -roots_of_1 iff ex k being Nat st x = [**(cos (((2 * PI ) * k) / n)),(sin (((2 * PI ) * k) / n))**] )

proof end;

theorem Th28: :: UNIROOTS:28

for n being non empty 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 end;

theorem Th29: :: UNIROOTS:29

for n being non empty Nat holds n -roots_of_1 = { [**(cos (((2 * PI ) * k) / n)),(sin (((2 * PI ) * k) / n))**] where k is Nat : k < n }

proof end;

theorem Th30: :: UNIROOTS:30

for n being non empty Nat holds Card (n -roots_of_1 ) = n

proof end;

registration

let n be non empty Nat;
cluster n -roots_of_1 -> non empty ;
correctness by Th25;
cluster n -roots_of_1 -> finite ;
correctness

proof end;

end;

theorem Th31: :: UNIROOTS:31

for n, ni being non empty Nat st ni divides n holds
ni -roots_of_1 c= n -roots_of_1

proof end;

theorem Th32: :: UNIROOTS:32

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 Nat holds (power (MultGroup R)) . x,k = (power R) . y,k

proof end;

theorem Th33: :: UNIROOTS:33

for n being non empty Nat
for x being Element of (MultGroup F_Complex ) st x in n -roots_of_1 holds
x is_not_of_order_0

proof end;

theorem Th34: :: UNIROOTS:34

for n being non empty Nat
for k being 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 end;

theorem Th35: :: UNIROOTS:35

for n being non empty Nat holds n -roots_of_1 c= the carrier of (MultGroup F_Complex )

proof end;

theorem :: UNIROOTS:36

for n being non empty Nat ex x being Element of (MultGroup F_Complex ) st ord x = n

proof end;

theorem Th37: :: UNIROOTS:37

for n being non empty Nat
for x being Element of (MultGroup F_Complex ) holds
( ord x divides n iff x in n -roots_of_1 )

proof end;

theorem Th38: :: UNIROOTS:38

for n being non empty Nat holds n -roots_of_1 = { x where x is Element of (MultGroup F_Complex ) : ord x divides n }

proof end;

theorem Th39: :: UNIROOTS:39

for n being non empty 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 end;

definition

let n be non empty Nat;
func n -th_roots_of_1 -> strict Group means :Def3: :: UNIROOTS:def 3
( the carrier of it = n -roots_of_1 & the mult of it = the mult of F_Complex || (n -roots_of_1 ) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def3 defines -th_roots_of_1 UNIROOTS:def 3 :

theorem :: UNIROOTS:40

for n being non empty Nat holds n -th_roots_of_1 is Subgroup of MultGroup F_Complex

proof end;

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

proof end;

end;

:: deftheorem defines unital_poly UNIROOTS:def 4 :

theorem Th41: :: UNIROOTS:41

unital_poly F_Complex ,1 = <%(- (1. F_Complex )),(1. F_Complex )%> by POLYNOM5:def 4;

theorem Th42: :: UNIROOTS:42

for L being non empty left_unital doubleLoopStr
for n being non empty Nat holds
( (unital_poly L,n) . 0 = - (1. L) & (unital_poly L,n) . n = 1. L )

proof end;

theorem Th43: :: UNIROOTS:43

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 end;

theorem Th44: :: UNIROOTS:44

for L being non empty left_unital non degenerated doubleLoopStr
for n being non empty Nat holds len (unital_poly L,n) = n + 1

proof end;

registration

let L be non empty left_unital non degenerated doubleLoopStr ;
let n be non empty Nat;
cluster unital_poly L,n -> non-zero ;
correctness

proof end;

end;

theorem Th45: :: UNIROOTS:45

for n being non empty Nat
for x being Element of F_Complex holds eval (unital_poly F_Complex ,n),x = ((power F_Complex ) . x,n) - 1

proof end;

theorem Th46: :: UNIROOTS:46

for n being non empty Nat holds Roots (unital_poly F_Complex ,n) = n -roots_of_1

proof end;

theorem Th47: :: UNIROOTS:47

for n being 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 end;

theorem Th48: :: UNIROOTS:48

for n being non empty 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 end;

theorem Th49: :: UNIROOTS:49

for n being non empty Nat holds BRoots (unital_poly F_Complex ,n) = (n -roots_of_1 ),1 -bag

proof end;

theorem Th50: :: UNIROOTS:50

for n being non empty Nat holds unital_poly F_Complex ,n = poly_with_roots ((n -roots_of_1 ),1 -bag )

proof end;

definition

let i be Integer;
let n be Nat;
:: original: |^
redefine func i |^ n -> Integer;
coherence ;

end;

theorem Th51: :: UNIROOTS:51

for n being non empty Nat
for i being Element of F_Complex st i is Integer holds
eval (unital_poly F_Complex ,n),i is Integer

proof end;

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

proof end;

uniqueness ;

end;

:: deftheorem Def5 defines cyclotomic_poly UNIROOTS:def 5 :

theorem Th52: :: UNIROOTS:52

cyclotomic_poly 1 = <%(- (1. F_Complex )),(1. F_Complex )%>

proof end;

theorem Th53: :: UNIROOTS:53

for n being non empty Nat
for f being FinSequence of the carrier of (Polynom-Ring F_Complex ) st len f = n & ( for i being non empty 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 end;

theorem Th54: :: UNIROOTS:54

for n being non empty 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 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 end;

theorem Th55: :: UNIROOTS:55

for d being non empty Nat
for i being Nat holds
( ( (cyclotomic_poly d) . 0 = 1 or (cyclotomic_poly d) . 0 = - 1 ) & (cyclotomic_poly d) . i is integer )

proof end;

theorem Th56: :: UNIROOTS:56

for d being non empty Nat
for z being Element of F_Complex st z is Integer holds
eval (cyclotomic_poly d),z is Integer

proof end;

theorem Th57: :: UNIROOTS:57

for n, ni being non empty 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 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 end;

theorem Th58: :: UNIROOTS:58

for n, ni being non empty 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 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 end;

theorem Th59: :: UNIROOTS:59

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 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 end;

theorem Th60: :: UNIROOTS:60

for n being non empty 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 end;

theorem Th61: :: UNIROOTS:61

for n, ni being non empty 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 end;

theorem :: UNIROOTS:62

for n, q being non empty 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 end;

theorem :: UNIROOTS:63

for n, ni, q being non empty 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 end;

theorem :: UNIROOTS:64

for n being non empty Nat st 1 < n holds
for q being 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 end;