:: UNIROOTS semantic presentation

theorem Th1: :: UNIROOTS:1

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

proof end;

Lemma2: for b₁ being Nat holds
( not b₁ is empty iff 1 <= b₁ )

proof end;

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

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

provided

E3: for b₁ being non empty Nat st ( for b₂ being non empty Nat st b₂ < b₁ holds
P₁[b₂] ) holds
P₁[b₁]

proof end;

theorem Th2: :: UNIROOTS:2

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

proof end;

Lemma4: for b₁ being FinSequence
for b₂, b₃ being Nat st b₃ <= b₂ holds
(b₁ | (Seg b₂)) | (Seg b₃) = b₁ | (Seg b₃)

proof end;

theorem Th3: :: UNIROOTS:3

for b₁ being FinSequence of F_Complex
for b₂ being FinSequence of REAL st len b₁ = len b₂ & ( for b₃ being Nat st b₃ in dom b₁ holds
|.(b₁ /. b₃).| = b₂ . b₃ ) holds
|.(Product b₁).| = Product b₂

proof end;

theorem Th4: :: UNIROOTS:4

for b₁ being non empty finite Subset of F_Complex
for b₂ being Element of F_Complex
for b₃ being FinSequence of REAL st len b₃ = card b₁ & ( for b₄ being Nat
for b₅ being Element of F_Complex st b₄ in dom b₃ & b₅ = (canFS b₁) . b₄ holds
b₃ . b₄ = |.(b₂ - b₅).| ) holds
|.(eval (poly_with_roots (b₁,1 -bag )),b₂).| = Product b₃

proof end;

theorem Th5: :: UNIROOTS:5

for b₁ being FinSequence of F_Complex st ( for b₂ being Nat st b₂ in dom b₁ holds
b₁ . b₂ is integer ) holds
Sum b₁ is integer

proof end;

theorem Th6: :: UNIROOTS:6

canceled;

theorem Th7: :: UNIROOTS:7

for b₁, b₂ being Element of F_Complex
for b₃, b₄ being Real st b₃ = b₁ & b₄ = b₂ holds
( b₃ * b₄ = b₁ * b₂ & b₃ + b₄ = b₁ + b₂ ) by COMPLFLD:3, COMPLFLD:6;

theorem Th8: :: UNIROOTS:8

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

proof end;

theorem Th9: :: UNIROOTS:9

for b₁ being non empty FinSequence of REAL
for b₂ being Real st b₂ >= 1 & ( for b₃ being Nat st b₃ in dom b₁ holds
b₁ . b₃ > b₂ ) holds
Product b₁ > b₂

proof end;

theorem Th10: :: UNIROOTS:10

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

proof end;

theorem Th11: :: UNIROOTS:11

for b₁, b₂ being Nat holds
( cos (((2 * PI ) * b₂) / b₁) = cos (((2 * PI ) * (b₂ mod b₁)) / b₁) & sin (((2 * PI ) * b₂) / b₁) = sin (((2 * PI ) * (b₂ mod b₁)) / b₁) )

proof end;

theorem Th12: :: UNIROOTS:12

for b₁, b₂ being Nat holds [**(cos (((2 * PI ) * b₂) / b₁)),(sin (((2 * PI ) * b₂) / b₁))**] = [**(cos (((2 * PI ) * (b₂ mod b₁)) / b₁)),(sin (((2 * PI ) * (b₂ mod b₁)) / b₁))**]

proof end;

theorem Th13: :: UNIROOTS:13

for b₁, b₂, b₃ being Nat holds [**(cos (((2 * PI ) * b₂) / b₁)),(sin (((2 * PI ) * b₂) / b₁))**] * [**(cos (((2 * PI ) * b₃) / b₁)),(sin (((2 * PI ) * b₃) / b₁))**] = [**(cos (((2 * PI ) * ((b₂ + b₃) mod b₁)) / b₁)),(sin (((2 * PI ) * ((b₂ + b₃) mod b₁)) / b₁))**]

proof end;

theorem Th14: :: UNIROOTS:14

for b₁ being non empty unital associative HGrStr
for b₂ being Element of b₁
for b₃, b₄ being Nat holds (power b₁) . b₂,(b₃ * b₄) = (power b₁) . ((power b₁) . b₂,b₃),b₄

proof end;

theorem Th15: :: UNIROOTS:15

for b₁ being Nat
for b₂ being Element of F_Complex st b₂ is Integer holds
(power F_Complex ) . b₂,b₁ is Integer

proof end;

theorem Th16: :: UNIROOTS:16

for b₁ being FinSequence of F_Complex st ( for b₂ being Nat st b₂ in dom b₁ holds
b₁ . b₂ is Integer ) holds
Sum b₁ is Integer

proof end;

theorem Th17: :: UNIROOTS:17

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

proof end;

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

registration

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

end;

definition

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

proof end;

uniqueness ;

end;

:: deftheorem Def1 defines MultGroup UNIROOTS:def 1 :

theorem Th18: :: UNIROOTS:18

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

proof end;

theorem Th19: :: UNIROOTS:19

for b₁ being Skew-Field
for b₂, b₃ being Element of b₁
for b₄, b₅ being Element of (MultGroup b₁) st b₂ = b₄ & b₃ = b₅ holds
b₄ * b₅ = b₂ * b₃

proof end;

theorem Th20: :: UNIROOTS:20

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

proof end;

registration

let c₁ be finite Skew-Field;
cluster MultGroup a₁ -> strict finite ;
correctness

proof end;

end;

theorem Th21: :: UNIROOTS:21

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

proof end;

theorem Th22: :: UNIROOTS:22

for b₁ being Skew-Field
for b₂ being set st b₂ in the carrier of (MultGroup b₁) holds
b₂ in the carrier of b₁

proof end;

theorem Th23: :: UNIROOTS:23

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

proof end;

definition

let c₁ be non empty Nat;
func c₁ -roots_of_1 -> Subset of F_Complex equals :: UNIROOTS:def 2
{ b₁ where B is Element of F_Complex : b₁ is CRoot of a₁, 1. F_Complex } ;
coherence

proof end;

end;

:: deftheorem Def2 defines -roots_of_1 UNIROOTS:def 2 :

theorem Th24: :: UNIROOTS:24

for b₁ being non empty Nat
for b₂ being Element of F_Complex holds
( b₂ in b₁ -roots_of_1 iff b₂ is CRoot of b₁, 1. F_Complex )

proof end;

theorem Th25: :: UNIROOTS:25

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

proof end;

theorem Th26: :: UNIROOTS:26

for b₁ being non empty Nat
for b₂ being Element of F_Complex st b₂ in b₁ -roots_of_1 holds
|.b₂.| = 1

proof end;

theorem Th27: :: UNIROOTS:27

for b₁ being non empty Nat
for b₂ being Element of F_Complex holds
( b₂ in b₁ -roots_of_1 iff ex b₃ being Nat st b₂ = [**(cos (((2 * PI ) * b₃) / b₁)),(sin (((2 * PI ) * b₃) / b₁))**] )

proof end;

theorem Th28: :: UNIROOTS:28

for b₁ being non empty Nat
for b₂, b₃ being Element of COMPLEX st b₂ in b₁ -roots_of_1 & b₃ in b₁ -roots_of_1 holds
b₂ * b₃ in b₁ -roots_of_1

proof end;

theorem Th29: :: UNIROOTS:29

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

proof end;

theorem Th30: :: UNIROOTS:30

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

proof end;

registration

let c₁ be non empty Nat;
cluster a₁ -roots_of_1 -> non empty ;
correctness by Th25;
cluster a₁ -roots_of_1 -> finite ;
correctness

proof end;

end;

theorem Th31: :: UNIROOTS:31

for b₁, b₂ being non empty Nat st b₂ divides b₁ holds
b₂ -roots_of_1 c= b₁ -roots_of_1

proof end;

theorem Th32: :: UNIROOTS:32

for b₁ being Skew-Field
for b₂ being Element of (MultGroup b₁)
for b₃ being Element of b₁ st b₃ = b₂ holds
for b₄ being Nat holds (power (MultGroup b₁)) . b₂,b₄ = (power b₁) . b₃,b₄

proof end;

theorem Th33: :: UNIROOTS:33

for b₁ being non empty Nat
for b₂ being Element of (MultGroup F_Complex ) st b₂ in b₁ -roots_of_1 holds
b₂ is_not_of_order_0

proof end;

theorem Th34: :: UNIROOTS:34

for b₁ being non empty Nat
for b₂ being Nat
for b₃ being Element of (MultGroup F_Complex ) st b₃ = [**(cos (((2 * PI ) * b₂) / b₁)),(sin (((2 * PI ) * b₂) / b₁))**] holds
ord b₃ = b₁ div (b₂ gcd b₁)

proof end;

theorem Th35: :: UNIROOTS:35

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

proof end;

theorem Th36: :: UNIROOTS:36

for b₁ being non empty Nat ex b₂ being Element of (MultGroup F_Complex ) st ord b₂ = b₁

proof end;

theorem Th37: :: UNIROOTS:37

for b₁ being non empty Nat
for b₂ being Element of (MultGroup F_Complex ) holds
( ord b₂ divides b₁ iff b₂ in b₁ -roots_of_1 )

proof end;

theorem Th38: :: UNIROOTS:38

for b₁ being non empty Nat holds b₁ -roots_of_1 = { b₂ where B is Element of (MultGroup F_Complex ) : ord b₂ divides b₁ }

proof end;

theorem Th39: :: UNIROOTS:39

for b₁ being non empty Nat
for b₂ being set holds
( b₂ in b₁ -roots_of_1 iff ex b₃ being Element of (MultGroup F_Complex ) st
( b₂ = b₃ & ord b₃ divides b₁ ) )

proof end;

definition

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

proof end;

uniqueness ;

end;

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

theorem Th40: :: UNIROOTS:40

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

proof end;

definition

let c₁ be non empty Nat;
let c₂ be non empty left_unital doubleLoopStr ;
func unital_poly c₂,c₁ -> Polynomial of a₂ equals :: UNIROOTS:def 4
((0_. a₂) +* 0,(- (1. a₂))) +* a₁,(1. a₂);
coherence

proof end;

end;

:: deftheorem Def4 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 b₁ being non empty left_unital doubleLoopStr
for b₂ being non empty Nat holds
( (unital_poly b₁,b₂) . 0 = - (1. b₁) & (unital_poly b₁,b₂) . b₂ = 1. b₁ )

proof end;

theorem Th43: :: UNIROOTS:43

for b₁ being non empty left_unital doubleLoopStr
for b₂ being non empty Nat
for b₃ being Nat st b₃ <> 0 & b₃ <> b₂ holds
(unital_poly b₁,b₂) . b₃ = 0. b₁

proof end;

theorem Th44: :: UNIROOTS:44

for b₁ being non empty left_unital non degenerated doubleLoopStr
for b₂ being non empty Nat holds len (unital_poly b₁,b₂) = b₂ + 1

proof end;

registration

let c₁ be non empty left_unital non degenerated doubleLoopStr ;
let c₂ be non empty Nat;
cluster unital_poly a₁,a₂ -> non-zero ;
correctness

proof end;

end;

theorem Th45: :: UNIROOTS:45

for b₁ being non empty Nat
for b₂ being Element of F_Complex holds eval (unital_poly F_Complex ,b₁),b₂ = ((power F_Complex ) . b₂,b₁) - 1

proof end;

theorem Th46: :: UNIROOTS:46

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

proof end;

theorem Th47: :: UNIROOTS:47

for b₁ being Nat
for b₂ being Element of F_Complex st b₂ is Real holds
ex b₃ being Real st
( b₃ = b₂ & (power F_Complex ) . b₂,b₁ = b₃ |^ b₁ )

proof end;

theorem Th48: :: UNIROOTS:48

for b₁ being non empty Nat
for b₂ being Real ex b₃ being Element of F_Complex st
( b₃ = b₂ & eval (unital_poly F_Complex ,b₁),b₃ = (b₂ |^ b₁) - 1 )

proof end;

theorem Th49: :: UNIROOTS:49

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

proof end;

theorem Th50: :: UNIROOTS:50

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

proof end;

definition

let c₁ be Integer;
let c₂ be Nat;
redefine func |^ as c₁ |^ c₂ -> Integer;
coherence ;

end;

theorem Th51: :: UNIROOTS:51

for b₁ being non empty Nat
for b₂ being Element of F_Complex st b₂ is Integer holds
eval (unital_poly F_Complex ,b₁),b₂ is Integer

proof end;

definition

let c₁ be non empty Nat;
func cyclotomic_poly c₁ -> Polynomial of F_Complex means :Def5: :: UNIROOTS:def 5
ex b₁ being non empty finite Subset of F_Complex st
( b₁ = { b₂ where B is Element of (MultGroup F_Complex ) : ord b₂ = a₁ } & a₂ = poly_with_roots (b₁,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 b₁ being non empty Nat
for b₂ being FinSequence of the carrier of (Polynom-Ring F_Complex ) st len b₂ = b₁ & ( for b₃ being non empty Nat st b₃ in dom b₂ holds
( ( not b₃ divides b₁ implies b₂ . b₃ = <%(1. F_Complex )%> ) & ( b₃ divides b₁ implies b₂ . b₃ = cyclotomic_poly b₃ ) ) ) holds
unital_poly F_Complex ,b₁ = Product b₂

proof end;

theorem Th54: :: UNIROOTS:54

for b₁ being non empty Nat ex b₂ being FinSequence of the carrier of (Polynom-Ring F_Complex )ex b₃ being Polynomial of F_Complex st
( b₃ = Product b₂ & dom b₂ = Seg b₁ & ( for b₄ being non empty Nat st b₄ in Seg b₁ holds
( ( ( not b₄ divides b₁ or b₄ = b₁ ) implies b₂ . b₄ = <%(1. F_Complex )%> ) & ( b₄ divides b₁ & b₄ <> b₁ implies b₂ . b₄ = cyclotomic_poly b₄ ) ) ) & unital_poly F_Complex ,b₁ = (cyclotomic_poly b₁) *' b₃ )

proof end;

theorem Th55: :: UNIROOTS:55

for b₁ being non empty Nat
for b₂ being Nat holds
( ( (cyclotomic_poly b₁) . 0 = 1 or (cyclotomic_poly b₁) . 0 = - 1 ) & (cyclotomic_poly b₁) . b₂ is integer )

proof end;

theorem Th56: :: UNIROOTS:56

for b₁ being non empty Nat
for b₂ being Element of F_Complex st b₂ is Integer holds
eval (cyclotomic_poly b₁),b₂ is Integer

proof end;

theorem Th57: :: UNIROOTS:57

for b₁, b₂ being non empty Nat
for b₃ being FinSequence of the carrier of (Polynom-Ring F_Complex )
for b₄ being finite Subset of F_Complex st b₄ = { b₅ where B is Element of (MultGroup F_Complex ) : ( ord b₅ divides b₁ & not ord b₅ divides b₂ & ord b₅ <> b₁ ) } & dom b₃ = Seg b₁ & ( for b₅ being non empty Nat st b₅ in dom b₃ holds
( ( ( not b₅ divides b₁ or b₅ divides b₂ or b₅ = b₁ ) implies b₃ . b₅ = <%(1. F_Complex )%> ) & ( b₅ divides b₁ & not b₅ divides b₂ & b₅ <> b₁ implies b₃ . b₅ = cyclotomic_poly b₅ ) ) ) holds
Product b₃ = poly_with_roots (b₄,1 -bag )

proof end;

theorem Th58: :: UNIROOTS:58

for b₁, b₂ being non empty Nat st b₂ < b₁ & b₂ divides b₁ holds
ex b₃ being FinSequence of the carrier of (Polynom-Ring F_Complex )ex b₄ being Polynomial of F_Complex st
( b₄ = Product b₃ & dom b₃ = Seg b₁ & ( for b₅ being non empty Nat st b₅ in Seg b₁ holds
( ( ( not b₅ divides b₁ or b₅ divides b₂ or b₅ = b₁ ) implies b₃ . b₅ = <%(1. F_Complex )%> ) & ( b₅ divides b₁ & not b₅ divides b₂ & b₅ <> b₁ implies b₃ . b₅ = cyclotomic_poly b₅ ) ) ) & unital_poly F_Complex ,b₁ = ((unital_poly F_Complex ,b₂) *' (cyclotomic_poly b₁)) *' b₄ )

proof end;

theorem Th59: :: UNIROOTS:59

for b₁ being Integer
for b₂ being Element of F_Complex
for b₃ being FinSequence of the carrier of (Polynom-Ring F_Complex )
for b₄ being Polynomial of F_Complex st b₄ = Product b₃ & b₂ = b₁ & ( for b₅ being non empty Nat holds
( not b₅ in dom b₃ or b₃ . b₅ = <%(1. F_Complex )%> or b₃ . b₅ = cyclotomic_poly b₅ ) ) holds
eval b₄,b₂ is integer

proof end;

theorem Th60: :: UNIROOTS:60

for b₁ being non empty Nat
for b₂, b₃, b₄ being Integer
for b₅ being Element of F_Complex st b₅ = b₄ & b₂ = eval (cyclotomic_poly b₁),b₅ & b₃ = eval (unital_poly F_Complex ,b₁),b₅ holds
b₂ divides b₃

proof end;

theorem Th61: :: UNIROOTS:61

for b₁, b₂ being non empty Nat
for b₃ being Integer st b₂ < b₁ & b₂ divides b₁ holds
for b₄ being Element of F_Complex st b₄ = b₃ holds
for b₅, b₆, b₇ being Integer st b₅ = eval (cyclotomic_poly b₁),b₄ & b₆ = eval (unital_poly F_Complex ,b₁),b₄ & b₇ = eval (unital_poly F_Complex ,b₂),b₄ holds
b₅ divides b₆ div b₇

proof end;

theorem Th62: :: UNIROOTS:62

for b₁, b₂ being non empty Nat
for b₃ being Element of F_Complex st b₃ = b₂ holds
for b₄ being Integer st b₄ = eval (cyclotomic_poly b₁),b₃ holds
b₄ divides (b₂ |^ b₁) - 1

proof end;

theorem Th63: :: UNIROOTS:63

for b₁, b₂, b₃ being non empty Nat st b₂ < b₁ & b₂ divides b₁ holds
for b₄ being Element of F_Complex st b₄ = b₃ holds
for b₅ being Integer st b₅ = eval (cyclotomic_poly b₁),b₄ holds
b₅ divides ((b₃ |^ b₁) - 1) div ((b₃ |^ b₂) - 1)

proof end;

theorem Th64: :: UNIROOTS:64

for b₁ being non empty Nat st 1 < b₁ holds
for b₂ being Nat st 1 < b₂ holds
for b₃ being Element of F_Complex st b₃ = b₂ holds
for b₄ being Integer st b₄ = eval (cyclotomic_poly b₁),b₃ holds
abs b₄ > b₂ - 1

proof end;