:: The Ring of Integers, Euclidean Rings and Modulo Integers
:: by Christoph Schwarzweller
::
:: Received February 4, 1999
:: Copyright (c) 1999-2021 Association of Mizar Users

definition

redefine func multint means :Def1: :: INT_3:def 1
for a, b being Element of INT holds it . (a,b) = multreal . (a,b);

compatibility
for b₁ being Element of K16(K17(K17(INT,INT),INT)) holds
( b₁ = multint iff for a, b being Element of INT holds b₁ . (a,b) = multreal . (a,b) )

proof end;

end;

:: deftheorem Def1 defines multint INT_3:def 1 :
for b₁ being Element of K16(K17(K17(INT,INT),INT)) holds
( b₁ = multint iff for a, b being Element of INT holds b₁ . (a,b) = multreal . (a,b) );

definition

redefine func compint means :: INT_3:def 2
for a being Element of INT holds it . a = compreal . a;

compatibility
for b₁ being Element of K16(K17(INT,INT)) holds
( b₁ = compint iff for a being Element of INT holds b₁ . a = compreal . a )

proof end;

end;

:: deftheorem defines compint INT_3:def 2 :
for b₁ being Element of K16(K17(INT,INT)) holds
( b₁ = compint iff for a being Element of INT holds b₁ . a = compreal . a );

definition

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

coherence
doubleLoopStr(# INT,addint,multint,(In (1,INT)),(In (0,INT)) #) is doubleLoopStr ;

end;

:: deftheorem defines INT.Ring INT_3:def 3 :
INT.Ring = doubleLoopStr(# INT,addint,multint,(In (1,INT)),(In (0,INT)) #);

registration

cluster INT.Ring -> non empty strict ;

coherence
( INT.Ring is strict & not INT.Ring is empty ) ;

end;

registration

cluster the carrier of INT.Ring -> integer-membered ;

coherence
the carrier of INT.Ring is integer-membered ;

end;

registration

let a, b be Element of INT.Ring;
let c, d be Integer;

identify a * b with c * d when a = c, b = d;

compatibility
( a = c & b = d implies a * b = c * d )

proof end;

identify a + b with c + d when a = c, b = d;

compatibility
( a = c & b = d implies a + b = c + d )

proof end;

end;

set M = INT.Ring ;

registration

cluster INT.Ring -> well-unital ;

coherence
INT.Ring is well-unital ;

end;

registration

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

coherence
( INT.Ring is Abelian & INT.Ring is add-associative & INT.Ring is right_zeroed & INT.Ring is right_complementable & INT.Ring is distributive & INT.Ring is commutative & INT.Ring is associative & INT.Ring is domRing-like & not INT.Ring is degenerated )

proof end;

end;

registration

let a be Element of INT.Ring;
let b be Integer;

identify - a with - b when a = b;

compatibility
( a = b implies - a = - b )

proof end;

end;

definition

let a be Element of INT.Ring;
:: original: |.
redefine func |.a.| -> Element of INT.Ring;
coherence
|.a.| is Element of INT.Ring

proof end;

end;

:: deftheorem INT_3:def 4 :
canceled;

definition

func absint -> Function of INT.Ring,NAT means :Def5: :: INT_3:def 5
for a being Element of INT.Ring holds it . a = absreal . a;

existence
ex b₁ being Function of INT.Ring,NAT st
for a being Element of INT.Ring holds b₁ . a = absreal . a

proof end;

uniqueness
for b₁, b₂ being Function of INT.Ring,NAT st ( for a being Element of INT.Ring holds b₁ . a = absreal . a ) & ( for a being Element of INT.Ring holds b₂ . a = absreal . a ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines absint INT_3:def 5 :
for b₁ being Function of INT.Ring,NAT holds
( b₁ = absint iff for a being Element of INT.Ring holds b₁ . a = absreal . a );

theorem Th1: :: INT_3:1

for a being Element of INT.Ring holds absint . a = |.a.|

proof end;

Lm1: for a being Integer holds
( a = 0 or absreal . a >= 1 )

proof end;

Lm2: for a, b being Element of INT.Ring st b <> 0. INT.Ring holds
for b9 being Integer st b9 = b & 0 <= b9 holds
ex q, r being Element of INT.Ring st
( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) )

proof end;

theorem :: INT_3:2

for a, b, q1, q2, r1, r2 being Element of INT.Ring st b <> 0. INT.Ring & a = (q1 * b) + r1 & 0. INT.Ring <= r1 & r1 < |.b.| & a = (q2 * b) + r2 & 0. INT.Ring <= r2 & r2 < |.b.| holds
( q1 = q2 & r1 = r2 )

proof end;

definition

let a, b be Element of INT.Ring;
:: original: div
redefine func a div b -> Element of INT.Ring;
coherence
a div b is Element of INT.Ring by INT_1:def 2;
:: original: mod
redefine func a mod b -> Element of INT.Ring;
coherence
a mod b is Element of INT.Ring by INT_1:def 2;

end;

:: deftheorem INT_3:def 6 :
canceled;

:: deftheorem INT_3:def 7 :
canceled;

theorem :: INT_3:3

for a, b being Element of INT.Ring st b <> 0. INT.Ring holds
a = ((a div b) * b) + (a mod b) by INT_1:59;

definition

let I be non empty doubleLoopStr ;

attr I is Euclidian means :Def8: :: INT_3:def 8
ex f being Function of I,NAT st
for a, b being Element of I st b <> 0. I holds
ex q, r being Element of I st
( a = (q * b) + r & ( r = 0. I or f . r < f . b ) );

end;

:: deftheorem Def8 defines Euclidian INT_3:def 8 :
for I being non empty doubleLoopStr holds
( I is Euclidian iff ex f being Function of I,NAT st
for a, b being Element of I st b <> 0. I holds
ex q, r being Element of I st
( a = (q * b) + r & ( r = 0. I or f . r < f . b ) ) );

registration

cluster INT.Ring -> Euclidian ;

coherence
INT.Ring is Euclidian

proof end;

end;

Lm4: for F being non empty almost_left_invertible associative commutative right_zeroed well-unital doubleLoopStr
for f being Function of F,NAT
for a, b being Element of F st b <> 0. F holds
ex q, r being Element of F st
( a = (q * b) + r & ( r = 0. F or f . r < f . b ) )

proof end;

registration

cluster non empty non degenerated right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like Euclidian for doubleLoopStr ;

existence
ex b₁ being Ring st
( b₁ is strict & b₁ is Euclidian & b₁ is domRing-like & not b₁ is degenerated & b₁ is distributive & b₁ is commutative )

proof end;

end;

definition

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

end;

definition

let E be non empty Euclidian doubleLoopStr ;

mode DegreeFunction of E -> Function of E,NAT means :Def9: :: INT_3:def 9
for a, b being Element of E st b <> 0. E holds
ex q, r being Element of E st
( a = (q * b) + r & ( r = 0. E or it . r < it . b ) );

existence
ex b₁ being Function of E,NAT st
for a, b being Element of E st b <> 0. E holds
ex q, r being Element of E st
( a = (q * b) + r & ( r = 0. E or b₁ . r < b₁ . b ) ) by Def8;

end;

:: deftheorem Def9 defines DegreeFunction INT_3:def 9 :
for E being non empty Euclidian doubleLoopStr
for b₂ being Function of E,NAT holds
( b₂ is DegreeFunction of E iff for a, b being Element of E st b <> 0. E holds
ex q, r being Element of E st
( a = (q * b) + r & ( r = 0. E or b₂ . r < b₂ . b ) ) );

theorem Th4: :: INT_3:4

for E being EuclidianRing holds E is gcdDomain

proof end;

registration

cluster non degenerated right_complementable associative commutative Abelian add-associative right_zeroed right-distributive well-unital domRing-like Euclidian -> non degenerated right_complementable associative commutative Abelian add-associative right_zeroed right-distributive well-unital domRing-like gcd-like for doubleLoopStr ;

coherence
for b₁ being non degenerated right_complementable associative commutative Abelian add-associative right_zeroed right-distributive well-unital domRing-like doubleLoopStr st b₁ is Euclidian holds
b₁ is gcd-like by Th4;

end;

definition

:: original: absint
redefine func absint -> DegreeFunction of INT.Ring ;
coherence
absint is DegreeFunction of INT.Ring

proof end;

end;

theorem Th5: :: INT_3:5

for F being non empty almost_left_invertible associative commutative right_zeroed well-unital doubleLoopStr holds F is Euclidian

proof end;

registration

cluster non empty almost_left_invertible associative commutative right_zeroed well-unital -> non empty Euclidian for doubleLoopStr ;

coherence
for b₁ being non empty doubleLoopStr st b₁ is commutative & b₁ is associative & b₁ is well-unital & b₁ is almost_left_invertible & b₁ is right_zeroed holds
b₁ is Euclidian by Th5;

end;

theorem :: INT_3:6

for F being non empty almost_left_invertible associative commutative right_zeroed well-unital doubleLoopStr
for f being Function of F,NAT holds f is DegreeFunction of F

proof end;

definition

let n be natural Number ;
assume A1: n > 0 ;

func multint n -> BinOp of (Segm n) means :Def10: :: INT_3:def 10
for k, l being Element of Segm n holds it . (k,l) = (k * l) mod n;

existence
ex b₁ being BinOp of (Segm n) st
for k, l being Element of Segm n holds b₁ . (k,l) = (k * l) mod n

proof end;

uniqueness
for b₁, b₂ being BinOp of (Segm n) st ( for k, l being Element of Segm n holds b₁ . (k,l) = (k * l) mod n ) & ( for k, l being Element of Segm n holds b₂ . (k,l) = (k * l) mod n ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines multint INT_3:def 10 :
for n being natural Number st n > 0 holds
for b₂ being BinOp of (Segm n) holds
( b₂ = multint n iff for k, l being Element of Segm n holds b₂ . (k,l) = (k * l) mod n );

definition

let n be natural Number ;
assume A1: n > 0 ;

func compint n -> UnOp of (Segm n) means :Def11: :: INT_3:def 11
for k being Element of Segm n holds it . k = (n - k) mod n;

existence
ex b₁ being UnOp of (Segm n) st
for k being Element of Segm n holds b₁ . k = (n - k) mod n

proof end;

uniqueness
for b₁, b₂ being UnOp of (Segm n) st ( for k being Element of Segm n holds b₁ . k = (n - k) mod n ) & ( for k being Element of Segm n holds b₂ . k = (n - k) mod n ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines compint INT_3:def 11 :
for n being natural Number st n > 0 holds
for b₂ being UnOp of (Segm n) holds
( b₂ = compint n iff for k being Element of Segm n holds b₂ . k = (n - k) mod n );

theorem Th7: :: INT_3:7

for n being Nat st n > 0 holds
for a, b being Element of Segm n holds
( ( a + b < n implies (addint n) . (a,b) = a + b ) & ( (addint n) . (a,b) = a + b implies a + b < n ) & ( a + b >= n implies (addint n) . (a,b) = (a + b) - n ) & ( (addint n) . (a,b) = (a + b) - n implies a + b >= n ) )

proof end;

Lm5: for a, b being Nat st b <> 0 holds
ex k being Element of NAT st
( k * b <= a & a < (k + 1) * b )

proof end;

theorem Th8: :: INT_3:8

for n being Nat st n > 0 holds
for a, b being Element of Segm n
for k being Nat holds
( ( k * n <= a * b & a * b < (k + 1) * n ) iff (multint n) . (a,b) = (a * b) - (k * n) )

proof end;

theorem :: INT_3:9

for n being Nat st n > 0 holds
for a being Element of Segm n holds
( ( a = 0 implies (compint n) . a = 0 ) & ( (compint n) . a = 0 implies a = 0 ) & ( a <> 0 implies (compint n) . a = n - a ) & ( (compint n) . a = n - a implies a <> 0 ) )

proof end;

definition

let n be natural Number ;

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

coherence
doubleLoopStr(# (Segm n),(addint n),(multint n),(In (1,(Segm n))),(In (0,(Segm n))) #) is doubleLoopStr ;

end;

:: deftheorem defines INT.Ring INT_3:def 12 :
for n being natural Number holds INT.Ring n = doubleLoopStr(# (Segm n),(addint n),(multint n),(In (1,(Segm n))),(In (0,(Segm n))) #);

registration

let n be non zero Nat;

cluster INT.Ring n -> non empty strict ;

coherence
( INT.Ring n is strict & not INT.Ring n is empty ) ;

end;

theorem Th10: :: INT_3:10

( INT.Ring 1 is degenerated & INT.Ring 1 is Ring & INT.Ring 1 is almost_left_invertible & INT.Ring 1 is unital & INT.Ring 1 is distributive & INT.Ring 1 is commutative )

proof end;

registration

cluster non empty degenerated right_complementable almost_left_invertible strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital for doubleLoopStr ;

existence
ex b₁ being Ring st
( b₁ is strict & b₁ is degenerated & b₁ is unital & b₁ is distributive & b₁ is almost_left_invertible & b₁ is commutative ) by Th10;

end;

Lm6: now :: thesis: for a, n being Nat st a in Segm n & a > 0 holds
n - a in Segm n

let a, n be Nat; :: thesis: ( a in Segm n & a > 0 implies n - a in Segm n )
assume a in Segm n ; :: thesis: ( a > 0 implies n - a in Segm n )
then a < n by NAT_1:44;
then A1: n - a is Element of NAT by INT_1:5;
assume a > 0 ; :: thesis: n - a in Segm n
then n - a < n - 0 by XREAL_1:15;
hence n - a in Segm n by A1, NAT_1:44; :: thesis: verum

end;

Lm7: for n being Nat st 1 < n holds
1. (INT.Ring n) = 1
by NAT_1:44, SUBSET_1:def 8;

theorem Th11: :: INT_3:11

for n being Nat st n > 1 holds
( not INT.Ring n is degenerated & INT.Ring n is commutative Ring )

proof end;

theorem Th12: :: INT_3:12

for p being Nat st p > 1 holds
( INT.Ring p is non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr iff p is Prime )

proof end;

registration

cluster natural prime -> non zero for set ;

coherence
for b₁ being Prime holds not b₁ is zero

proof end;

end;

registration

let p be Prime;

cluster INT.Ring p -> non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive ;

coherence
( INT.Ring p is add-associative & INT.Ring p is right_zeroed & INT.Ring p is right_complementable & INT.Ring p is Abelian & INT.Ring p is commutative & INT.Ring p is associative & INT.Ring p is well-unital & INT.Ring p is distributive & INT.Ring p is almost_left_invertible & not INT.Ring p is degenerated )

proof end;

end;

theorem :: INT_3:13

1. INT.Ring = 1 ;

theorem :: INT_3:14

for n being Nat st 1 < n holds
1. (INT.Ring n) = 1 by Lm7;

:: from SCMRING3, 2011.08.19, A.T.

registration

cluster INT.Ring -> infinite ;

coherence
not INT.Ring is finite ;

end;

registration

cluster non empty infinite right_complementable strict unital associative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital for doubleLoopStr ;

existence
ex b₁ being Ring st
( b₁ is strict & b₁ is infinite )

proof end;

end;