:: INT_3 semantic presentation

definition

redefine func multint -> M6(K17(INT ,INT ), INT ) means :Def1: :: INT_3:def 1
for b₁, b₂ being Element of INT holds a₁ . b₁,b₂ = multreal . b₁,b₂;
compatibility

proof end;

end;

:: deftheorem Def1 defines multint INT_3:def 1 :

definition

redefine func compint -> M6( INT , INT ) means :: INT_3:def 2
for b₁ being Element of INT holds a₁ . b₁ = compreal . b₁;
compatibility

proof end;

end;

:: deftheorem Def2 defines compint INT_3:def 2 :

definition

func INT.Ring -> doubleLoopStr equals :: INT_3:def 3
doubleLoopStr(# INT ,addint ,multint ,(In 1,INT ),(In 0,INT ) #);
coherence ;

end;

:: deftheorem Def3 defines INT.Ring INT_3:def 3 :

Lemma2: for b₁ being Element of INT.Ring holds b₁ in REAL

proof end;

registration

cluster INT.Ring -> non empty strict ;
coherence

proof end;

end;

set c₁ = INT.Ring ;

Lemma3: 0 = 0. INT.Ring

proof end;

Lemma4: for b₁, b₂ being Element of INT.Ring
for b₃, b₄ being Integer st b₃ = b₁ & b₄ = b₂ holds
b₁ * b₂ = b₃ * b₄

proof end;

Lemma5: for b₁, b₂ being Element of INT.Ring st b₁ = 1 holds
( b₂ * b₁ = b₂ & b₁ * b₂ = b₂ )

proof end;

registration

cluster INT.Ring -> non empty unital strict ;
coherence

proof end;

end;

Lemma6: 1. INT.Ring = 1

proof end;

registration

cluster INT.Ring -> non empty unital associative commutative Abelian add-associative right_zeroed right_complementable strict distributive non degenerated domRing-like ;
coherence

proof end;

end;

Lemma7: for b₁ being Element of INT.Ring
for b₂ being Integer st b₂ = b₁ holds
- b₂ = - b₁

proof end;

definition

let c₂, c₃ be Element of INT.Ring ;
pred c₁ <= c₂ means :Def4: :: INT_3:def 4
ex b₁, b₂ being Integer st
( b₁ = a₁ & b₂ = a₂ & b₁ <= b₂ );
reflexivity

proof end;

connectedness

proof end;

end;

:: deftheorem Def4 defines <= INT_3:def 4 :

notation

let c₂, c₃ be Element of INT.Ring ;
synonym c₂ >= c₁ for c₁ <= c₂;
antonym c₂ < c₁ for c₁ <= c₂;
antonym c₁ > c₂ for c₁ <= c₂;

end;

Lemma9: for b₁, b₂ being Element of INT.Ring holds
( b₁ < b₂ iff ( b₁ <= b₂ & b₁ <> b₂ ) )

proof end;

definition

let c₂ be Element of INT.Ring ;
func abs c₁ -> Element of INT.Ring equals :Def5: :: INT_3:def 5
a₁ if a₁ >= 0. INT.Ring
otherwise - a₁;
correctness ;

end;

:: deftheorem Def5 defines abs INT_3:def 5 :

definition

func absint -> Function of the carrier of INT.Ring , NAT means :Def6: :: INT_3:def 6
for b₁ being Element of INT.Ring holds a₁ . b₁ = absreal . b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines absint INT_3:def 6 :

theorem Th1: :: INT_3:1

for b₁ being Element of INT.Ring holds absint . b₁ = abs b₁

proof end;

Lemma13: for b₁ being Integer holds
( b₁ = 0 or absreal . b₁ >= 1 )

proof end;

Lemma14: for b₁, b₂ being Element of INT.Ring
for b₃, b₄ being Integer st b₃ = b₁ & b₄ = b₂ holds
b₁ + b₂ = b₃ + b₄

proof end;

Lemma15: for b₁, b₂ being Element of INT.Ring st b₂ <> 0. INT.Ring holds
for b₃ being Integer st b₃ = b₂ & 0 <= b₃ holds
ex b₄, b₅ being Element of INT.Ring st
( b₁ = (b₄ * b₂) + b₅ & ( b₅ = 0. INT.Ring or absint . b₅ < absint . b₂ ) )

proof end;

Lemma16: for b₁, b₂ being Element of INT.Ring st b₂ <> 0. INT.Ring holds
for b₃ being Integer st b₃ = b₂ & 0 <= b₃ holds
ex b₄, b₅ being Element of INT.Ring st
( b₁ = (b₄ * b₂) + b₅ & 0. INT.Ring <= b₅ & b₅ < abs b₂ )

proof end;

theorem Th2: :: INT_3:2

for b₁, b₂, b₃, b₄, b₅, b₆ being Element of INT.Ring st b₂ <> 0. INT.Ring & b₁ = (b₃ * b₂) + b₅ & 0. INT.Ring <= b₅ & b₅ < abs b₂ & b₁ = (b₄ * b₂) + b₆ & 0. INT.Ring <= b₆ & b₆ < abs b₂ holds
( b₃ = b₄ & b₅ = b₆ )

proof end;

definition

let c₂, c₃ be Element of INT.Ring ;
assume E18: c₃ <> 0. INT.Ring ;
func c₁ div c₂ -> Element of INT.Ring means :Def7: :: INT_3:def 7
ex b₁ being Element of INT.Ring st
( a₁ = (a₃ * a₂) + b₁ & 0. INT.Ring <= b₁ & b₁ < abs a₂ );
existence

proof end;

uniqueness by E18, Th2;

end;

:: deftheorem Def7 defines div INT_3:def 7 :

definition

let c₂, c₃ be Element of INT.Ring ;
assume E19: c₃ <> 0. INT.Ring ;
func c₁ mod c₂ -> Element of INT.Ring means :Def8: :: INT_3:def 8
ex b₁ being Element of INT.Ring st
( a₁ = (b₁ * a₂) + a₃ & 0. INT.Ring <= a₃ & a₃ < abs a₂ );
existence

proof end;

uniqueness by E19, Th2;

end;

:: deftheorem Def8 defines mod INT_3:def 8 :

theorem Th3: :: INT_3:3

for b₁, b₂ being Element of INT.Ring st b₂ <> 0. INT.Ring holds
b₁ = ((b₁ div b₂) * b₂) + (b₁ mod b₂)

proof end;

definition

let c₂ be non empty doubleLoopStr ;
attr a₁ is Euclidian means :Def9: :: INT_3:def 9
ex b₁ being Function of the carrier of a₁, NAT st
for b₂, b₃ being Element of a₁ st b₃ <> 0. a₁ holds
ex b₄, b₅ being Element of a₁ st
( b₂ = (b₄ * b₃) + b₅ & ( b₅ = 0. a₁ or b₁ . b₅ < b₁ . b₃ ) );

end;

:: deftheorem Def9 defines Euclidian INT_3:def 9 :

registration end;

Lemma21: for b₁ being non empty associative commutative right_zeroed left_unital Field-like doubleLoopStr
for b₂ being Function of the carrier of b₁, NAT
for b₃, b₄ being Element of b₁ st b₄ <> 0. b₁ holds
ex b₅, b₆ being Element of b₁ st
( b₃ = (b₅ * b₄) + b₆ & ( b₆ = 0. b₁ or b₂ . b₆ < b₂ . b₄ ) )

proof end;

registration

cluster commutative strict non degenerated domRing-like Euclidian doubleLoopStr ;
existence

proof end;

end;

definition

mode EuclidianRing is commutative distributive non degenerated domRing-like Euclidian Ring;

end;

registration

cluster strict doubleLoopStr ;
existence

proof end;

end;

definition

let c₂ be non empty Euclidian doubleLoopStr ;
mode DegreeFunction of c₁ -> Function of the carrier of a₁, NAT means :Def10: :: INT_3:def 10
for b₁, b₂ being Element of a₁ st b₂ <> 0. a₁ holds
ex b₃, b₄ being Element of a₁ st
( b₁ = (b₃ * b₂) + b₄ & ( b₄ = 0. a₁ or a₂ . b₄ < a₂ . b₂ ) );
existence by Def9;

end;

:: deftheorem Def10 defines DegreeFunction INT_3:def 10 :

theorem Th4: :: INT_3:4

for b₁ being EuclidianRing holds b₁ is gcdDomain

proof end;

registration end;

definition

redefine func absint as absint -> DegreeFunction of INT.Ring ;
coherence

proof end;

end;

theorem Th5: :: INT_3:5

for b₁ being non empty associative commutative right_zeroed left_unital Field-like doubleLoopStr holds b₁ is Euclidian

proof end;

registration

cluster non empty associative commutative right_zeroed left_unital Field-like -> non empty Euclidian doubleLoopStr ;
coherence by Th5;

end;

theorem Th6: :: INT_3:6

for b₁ being non empty associative commutative right_zeroed left_unital Field-like doubleLoopStr
for b₂ being Function of the carrier of b₁, NAT holds b₂ is DegreeFunction of b₁

proof end;

theorem Th7: :: INT_3:7

canceled;

theorem Th8: :: INT_3:8

for b₁, b₂, b₃ being Integer holds
( ( b₁ <> 0 implies (b₂ + (b₁ * b₃)) div b₁ = (b₂ div b₁) + b₃ ) & (b₂ + (b₁ * b₃)) mod b₁ = b₂ mod b₁ )

proof end;

theorem Th9: :: INT_3:9

for b₁ being natural number st b₁ > 0 holds
for b₂ being Integer holds
( b₂ mod b₁ >= 0 & b₂ mod b₁ < b₁ )

proof end;

theorem Th10: :: INT_3:10

for b₁, b₂ being Integer holds
( ( 0 <= b₂ & b₂ < b₁ implies b₂ mod b₁ = b₂ ) & ( 0 > b₂ & b₂ >= - b₁ implies b₂ mod b₁ = b₁ + b₂ ) )

proof end;

theorem Th11: :: INT_3:11

for b₁ being natural number st b₁ > 0 holds
for b₂ being Integer holds
( b₂ mod b₁ = 0 iff b₁ divides b₂ )

proof end;

theorem Th12: :: INT_3:12

for b₁, b₂, b₃ being Integer holds
( ( b₁ <> 0 & b₂ mod b₁ = b₃ mod b₁ implies b₂,b₃ are_congruent_mod b₁ ) & ( b₂,b₃ are_congruent_mod b₁ implies b₂ mod b₁ = b₃ mod b₁ ) )

proof end;

theorem Th13: :: INT_3:13

for b₁ being natural number
for b₂ being Integer holds (b₂ mod b₁) mod b₁ = b₂ mod b₁

proof end;

theorem Th14: :: INT_3:14

for b₁, b₂, b₃ being Integer holds (b₂ + b₃) mod b₁ = ((b₂ mod b₁) + (b₃ mod b₁)) mod b₁

proof end;

theorem Th15: :: INT_3:15

for b₁, b₂, b₃ being Integer holds (b₂ * b₃) mod b₁ = ((b₂ mod b₁) * (b₃ mod b₁)) mod b₁

proof end;

theorem Th16: :: INT_3:16

for b₁, b₂ being Integer ex b₃, b₄ being Integer st b₁ gcd b₂ = (b₃ * b₁) + (b₄ * b₂)

proof end;

definition

let c₂ be natural number ;
assume E34: c₂ > 0 ;
func multint c₁ -> BinOp of Segm a₁ means :Def11: :: INT_3:def 11
for b₁, b₂ being Element of Segm a₁ holds a₂ . b₁,b₂ = (b₁ * b₂) mod a₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines multint INT_3:def 11 :

definition

let c₂ be natural number ;
assume E35: c₂ > 0 ;
func compint c₁ -> UnOp of Segm a₁ means :Def12: :: INT_3:def 12
for b₁ being Element of Segm a₁ holds a₂ . b₁ = (a₁ - b₁) mod a₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines compint INT_3:def 12 :

Lemma36: for b₁ being natural number st b₁ > 0 holds
for b₂ being natural number st b₂ < b₁ holds
for b₃ being natural number st b₃ = b₁ - b₂ holds
(b₁ - b₂) mod b₁ = b₃ mod b₁

proof end;

theorem Th17: :: INT_3:17

for b₁ being natural number st b₁ > 0 holds
for b₂, b₃ being Element of Segm b₁ holds
( ( b₂ + b₃ < b₁ implies (addint b₁) . b₂,b₃ = b₂ + b₃ ) & ( (addint b₁) . b₂,b₃ = b₂ + b₃ implies b₂ + b₃ < b₁ ) & ( b₂ + b₃ >= b₁ implies (addint b₁) . b₂,b₃ = (b₂ + b₃) - b₁ ) & ( (addint b₁) . b₂,b₃ = (b₂ + b₃) - b₁ implies b₂ + b₃ >= b₁ ) )

proof end;

Lemma38: for b₁, b₂ being natural number st b₂ <> 0 holds
ex b₃ being Nat st
( b₃ * b₂ <= b₁ & b₁ < (b₃ + 1) * b₂ )

proof end;

theorem Th18: :: INT_3:18

for b₁ being natural number st b₁ > 0 holds
for b₂, b₃ being Element of Segm b₁
for b₄ being natural number holds
( ( b₄ * b₁ <= b₂ * b₃ & b₂ * b₃ < (b₄ + 1) * b₁ ) iff (multint b₁) . b₂,b₃ = (b₂ * b₃) - (b₄ * b₁) )

proof end;

theorem Th19: :: INT_3:19

for b₁ being natural number st b₁ > 0 holds
for b₂ being Element of Segm b₁ holds
( ( b₂ = 0 implies (compint b₁) . b₂ = 0 ) & ( (compint b₁) . b₂ = 0 implies b₂ = 0 ) & ( b₂ <> 0 implies (compint b₁) . b₂ = b₁ - b₂ ) & ( (compint b₁) . b₂ = b₁ - b₂ implies b₂ <> 0 ) )

proof end;

definition

let c₂ be natural number ;
func INT.Ring c₁ -> doubleLoopStr equals :: INT_3:def 13
doubleLoopStr(# (Segm a₁),(addint a₁),(multint a₁),(In 1,(Segm a₁)),(In 0,(Segm a₁)) #);
coherence ;

end;

:: deftheorem Def13 defines INT.Ring INT_3:def 13 :

registration

let c₂ be natural number ;
cluster INT.Ring a₁ -> non empty strict ;
coherence

proof end;

end;

theorem Th20: :: INT_3:20

( INT.Ring 1 is degenerated & INT.Ring 1 is Ring & INT.Ring 1 is Field-like & INT.Ring 1 is unital & INT.Ring 1 is distributive & INT.Ring 1 is commutative )

proof end;

registration

cluster unital commutative strict Field-like degenerated Euclidian doubleLoopStr ;
existence by Th20;

end;

E41: now

let c₂, c₃ be natural number ;
assume E42: c₃ > 0 ;
assume c₂ in Segm c₃ ;
then c₂ < c₃ by E42, GR_CY_1:10;
then E43: c₃ - c₂ is Nat by INT_1:18;
assume c₂ > 0 ;
then c₃ - c₂ < c₃ - 0 by REAL_1:92;
hence c₃ - c₂ in Segm c₃ by E43, GR_CY_1:10;

end;

Lemma42: for b₁ being natural number st 0 < b₁ holds
for b₂, b₃ being Element of (INT.Ring b₁) st b₂ = 1 holds
( b₃ * b₂ = b₃ & b₂ * b₃ = b₃ )

proof end;

E43: now

let c₂ be natural number ;
assume E44: 1 < c₂ ;
thus INT.Ring c₂ is unital

proof

set c₃ = INT.Ring c₂;
reconsider c₄ = 1 as Element of (INT.Ring c₂) by E44, GR_CY_1:10;
take c₄ ; :: according to GROUP_1:def 2
thus for b₁ being Element of the carrier of (INT.Ring c₂) holds
( b₁ * c₄ = b₁ & c₄ * b₁ = b₁ ) by E44, Lemma42;

end;

Lemma44: for b₁ being natural number st 1 < b₁ holds
1. (INT.Ring b₁) = 1

proof end;

theorem Th21: :: INT_3:21

for b₁ being natural number st b₁ > 1 holds
( not INT.Ring b₁ is degenerated & INT.Ring b₁ is unital commutative distributive Ring )

proof end;

Lemma46: for b₁ being natural number st b₁ > 0 holds
0. (INT.Ring b₁) = 0

proof end;

theorem Th22: :: INT_3:22

for b₁ being natural number st b₁ > 1 holds
( INT.Ring b₁ is non empty associative commutative Abelian add-associative right_zeroed right_complementable distributive left_unital Field-like non degenerated doubleLoopStr iff b₁ is Prime )

proof end;

registration

let c₂ be Prime;
cluster INT.Ring a₁ -> non empty associative commutative Abelian add-associative right_zeroed right_complementable strict distributive left_unital Field-like non degenerated Euclidian ;
coherence

proof end;

end;

theorem Th23: :: INT_3:23

1. INT.Ring = 1 by Lemma6;

theorem Th24: :: INT_3:24

for b₁ being natural number st 1 < b₁ holds
1. (INT.Ring b₁) = 1 by Lemma44;