:: GR_CY_1 semantic presentation

definition

let c₁ be natural number ;
assume E1: c₁ > 0 ;
func Segm c₁ -> non empty Subset of NAT equals :Def1: :: GR_CY_1:def 1
{ b₁ where B is Nat : b₁ < a₁ } ;
coherence

proof end;

end;

:: deftheorem Def1 defines Segm GR_CY_1:def 1 :

Lemma2: for b₁ being set
for b₂ being Nat st b₂ > 0 & b₁ in Segm b₂ holds
b₁ is Nat
;

theorem Th1: :: GR_CY_1:1

canceled;

theorem Th2: :: GR_CY_1:2

canceled;

theorem Th3: :: GR_CY_1:3

canceled;

theorem Th4: :: GR_CY_1:4

canceled;

theorem Th5: :: GR_CY_1:5

canceled;

theorem Th6: :: GR_CY_1:6

canceled;

theorem Th7: :: GR_CY_1:7

canceled;

theorem Th8: :: GR_CY_1:8

canceled;

theorem Th9: :: GR_CY_1:9

canceled;

theorem Th10: :: GR_CY_1:10

for b₁, b₂ being natural number st b₁ > 0 holds
( b₂ in Segm b₁ iff b₂ < b₁ )

proof end;

theorem Th11: :: GR_CY_1:11

canceled;

theorem Th12: :: GR_CY_1:12

for b₁ being natural number st b₁ > 0 holds
0 in Segm b₁ by Th10;

theorem Th13: :: GR_CY_1:13

Segm 1 = {0}

proof end;

definition

redefine func addint -> M6([:INT ,INT :], INT ) means :: GR_CY_1:def 2
for b₁, b₂ being Element of INT holds a₁ . b₁,b₂ = addreal . b₁,b₂;
compatibility

proof end;

end;

:: deftheorem Def2 defines addint GR_CY_1:def 2 :

theorem Th14: :: GR_CY_1:14

for b₁, b₂ being Integer holds addint . b₁,b₂ = b₁ + b₂

proof end;

theorem Th15: :: GR_CY_1:15

for b₁ being Element of INT st b₁ = 0 holds
b₁ is_a_unity_wrt addint by BINOP_2:4, SETWISEO:22;

definition

let c₁ be FinSequence of INT ;
func Sum c₁ -> Integer equals :: GR_CY_1:def 3
addint $$ a₁;
coherence ;

end;

:: deftheorem Def3 defines Sum GR_CY_1:def 3 :

theorem Th16: :: GR_CY_1:16

canceled;

theorem Th17: :: GR_CY_1:17

canceled;

theorem Th18: :: GR_CY_1:18

canceled;

theorem Th19: :: GR_CY_1:19

canceled;

theorem Th20: :: GR_CY_1:20

for b₁ being Element of INT
for b₂ being FinSequence of INT holds Sum (b₂ ^ <*b₁*>) = (Sum b₂) + (@ b₁)

proof end;

theorem Th21: :: GR_CY_1:21

for b₁ being Element of INT holds Sum <*b₁*> = b₁ by FINSOP_1:12;

theorem Th22: :: GR_CY_1:22

Sum (<*> INT ) = 0 by BINOP_2:4, FINSOP_1:11;

Lemma8: for b₁ being Group
for b₂ being Element of b₁ holds Product (((len (<*> INT )) |-> b₂) |^ (<*> INT )) = b₂ |^ (Sum (<*> INT ))

proof end;

Lemma9: for b₁ being Group
for b₂ being Element of b₁
for b₃ being FinSequence of INT
for b₄ being Element of INT st Product (((len b₃) |-> b₂) |^ b₃) = b₂ |^ (Sum b₃) holds
Product (((len (b₃ ^ <*b₄*>)) |-> b₂) |^ (b₃ ^ <*b₄*>)) = b₂ |^ (Sum (b₃ ^ <*b₄*>))

proof end;

theorem Th23: :: GR_CY_1:23

canceled;

theorem Th24: :: GR_CY_1:24

for b₁ being Group
for b₂ being Element of b₁
for b₃ being FinSequence of INT holds Product (((len b₃) |-> b₂) |^ b₃) = b₂ |^ (Sum b₃)

proof end;

theorem Th25: :: GR_CY_1:25

for b₁ being Group
for b₂, b₃ being Element of b₁ holds
( b₂ in gr {b₃} iff ex b₄ being Integer st b₂ = b₃ |^ b₄ )

proof end;

theorem Th26: :: GR_CY_1:26

for b₁ being Group
for b₂ being Element of b₁ st b₁ is finite holds
b₂ is_not_of_order_0

proof end;

theorem Th27: :: GR_CY_1:27

for b₁ being Group
for b₂ being Element of b₁ st b₁ is finite holds
ord b₂ = ord (gr {b₂})

proof end;

theorem Th28: :: GR_CY_1:28

for b₁ being Group
for b₂ being Element of b₁ st b₁ is finite holds
ord b₂ divides ord b₁

proof end;

theorem Th29: :: GR_CY_1:29

for b₁ being Group
for b₂ being Element of b₁ st b₁ is finite holds
b₂ |^ (ord b₁) = 1. b₁

proof end;

theorem Th30: :: GR_CY_1:30

for b₁ being Nat
for b₂ being Group
for b₃ being Element of b₂ st b₂ is finite holds
(b₃ |^ b₁) " = b₃ |^ ((ord b₂) - (b₁ mod (ord b₂)))

proof end;

theorem Th31: :: GR_CY_1:31

for b₁ being strict Group st ord b₁ > 1 holds
ex b₂ being Element of b₁ st b₂ <> 1. b₁

proof end;

theorem Th32: :: GR_CY_1:32

for b₁ being Nat
for b₂ being strict Group st b₂ is finite & ord b₂ = b₁ & b₁ is prime holds
for b₃ being strict Subgroup of b₂ holds
( b₃ = (1). b₂ or b₃ = b₂ )

proof end;

theorem Th33: :: GR_CY_1:33

( HGrStr(# INT ,addint #) is associative & HGrStr(# INT ,addint #) is Group-like )

proof end;

definition

func INT.Group -> strict Group equals :: GR_CY_1:def 4
HGrStr(# INT ,addint #);
coherence by Th33;

end;

:: deftheorem Def4 defines INT.Group GR_CY_1:def 4 :

definition

let c₁ be natural number ;
assume E19: c₁ > 0 ;
func addint c₁ -> BinOp of Segm a₁ means :Def5: :: GR_CY_1:def 5
for b₁, b₂ being Element of Segm a₁ holds a₂ . b₁,b₂ = (b₁ + b₂) mod a₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines addint GR_CY_1:def 5 :

theorem Th34: :: GR_CY_1:34

for b₁ being natural number st b₁ > 0 holds
( HGrStr(# (Segm b₁),(addint b₁) #) is associative & HGrStr(# (Segm b₁),(addint b₁) #) is Group-like )

proof end;

definition

let c₁ be natural number ;
assume E21: c₁ > 0 ;
func INT.Group c₁ -> strict Group equals :Def6: :: GR_CY_1:def 6
HGrStr(# (Segm a₁),(addint a₁) #);
coherence by E21, Th34;

end;

:: deftheorem Def6 defines INT.Group GR_CY_1:def 6 :

theorem Th35: :: GR_CY_1:35

1. INT.Group = 0

proof end;

theorem Th36: :: GR_CY_1:36

for b₁ being natural number st b₁ > 0 holds
1. (INT.Group b₁) = 0

proof end;

definition

let c₁ be Element of INT.Group ;
func @' c₁ -> Integer equals :: GR_CY_1:def 7
a₁;
coherence by INT_1:def 2;

end;

:: deftheorem Def7 defines @' GR_CY_1:def 7 :

definition

let c₁ be Integer;
func @' c₁ -> Element of INT.Group equals :: GR_CY_1:def 8
a₁;
coherence by INT_1:def 2;

end;

:: deftheorem Def8 defines @' GR_CY_1:def 8 :

theorem Th37: :: GR_CY_1:37

for b₁ being Element of INT.Group holds b₁ " = - (@' b₁)

proof end;

Lemma25: for b₁, b₂ being Element of INT.Group
for b₃, b₄ being Integer st b₁ = b₃ & b₂ = b₄ holds
b₁ * b₂ = b₃ + b₄
by Th14;

theorem Th38: :: GR_CY_1:38

for b₁ being Element of INT.Group st b₁ = 1 holds
for b₂ being Nat holds b₁ |^ b₂ = b₂

proof end;

theorem Th39: :: GR_CY_1:39

for b₁ being Element of INT.Group
for b₂ being Integer st b₁ = 1 holds
b₂ = b₁ |^ b₂

proof end;

Lemma28: ex b₁ being Element of INT.Group st HGrStr(# the carrier of INT.Group ,the mult of INT.Group #) = gr {b₁}

proof end;

definition

let c₁ be Group;
attr a₁ is cyclic means :Def9: :: GR_CY_1:def 9
ex b₁ being Element of a₁ st HGrStr(# the carrier of a₁,the mult of a₁ #) = gr {b₁};

end;

:: deftheorem Def9 defines cyclic GR_CY_1:def 9 :

registration

cluster strict cyclic HGrStr ;
existence

proof end;

end;

theorem Th40: :: GR_CY_1:40

for b₁ being Group holds (1). b₁ is cyclic

proof end;

theorem Th41: :: GR_CY_1:41

for b₁ being Group holds
( b₁ is cyclic Group iff ex b₂ being Element of b₁ st
for b₃ being Element of b₁ ex b₄ being Integer st b₃ = b₂ |^ b₄ )

proof end;

theorem Th42: :: GR_CY_1:42

for b₁ being Group st b₁ is finite holds
( b₁ is cyclic Group iff ex b₂ being Element of b₁ st
for b₃ being Element of b₁ ex b₄ being Nat st b₃ = b₂ |^ b₄ )

proof end;

theorem Th43: :: GR_CY_1:43

for b₁ being strict Group st b₁ is finite holds
( b₁ is cyclic Group iff ex b₂ being Element of b₁ st ord b₂ = ord b₁ )

proof end;

theorem Th44: :: GR_CY_1:44

for b₁ being Group
for b₂ being strict Subgroup of b₁ st b₁ is finite & b₁ is cyclic Group holds
b₂ is cyclic Group

proof end;

theorem Th45: :: GR_CY_1:45

for b₁ being Nat
for b₂ being strict Group st b₂ is finite & ord b₂ = b₁ & b₁ is prime holds
b₂ is cyclic Group

proof end;

theorem Th46: :: GR_CY_1:46

for b₁ being Nat st b₁ > 0 holds
ex b₂ being Element of (INT.Group b₁) st
for b₃ being Element of (INT.Group b₁) ex b₄ being Integer st b₃ = b₂ |^ b₄

proof end;

registration

cluster cyclic -> commutative HGrStr ;
coherence

proof end;

end;

theorem Th47: :: GR_CY_1:47

canceled;

theorem Th48: :: GR_CY_1:48

INT.Group is cyclic

proof end;

theorem Th49: :: GR_CY_1:49

for b₁ being Nat st b₁ > 0 holds
INT.Group b₁ is cyclic Group

proof end;

theorem Th50: :: GR_CY_1:50

INT.Group is commutative Group

proof end;

theorem Th51: :: GR_CY_1:51

for b₁, b₂ being Nat st 0 < b₁ & b₁ <= b₂ holds
Segm b₁ c= Segm b₂

proof end;