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


begin

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 b1 being Element of K6(K7(K7(INT,INT),INT)) holds
( b1 = multint iff for a, b being Element of INT holds b1 . (a,b) = multreal . (a,b) )
proof end;
end;

:: deftheorem Def1 defines multint INT_3:def 1 :
for b1 being Element of K6(K7(K7(INT,INT),INT)) holds
( b1 = multint iff for a, b being Element of INT holds b1 . (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 b1 being Element of K6(K7(INT,INT)) holds
( b1 = compint iff for a being Element of INT holds b1 . a = compreal . a )
proof end;
end;

:: deftheorem defines compint INT_3:def 2 :
for b1 being Element of K6(K7(INT,INT)) holds
( b1 = compint iff for a being Element of INT holds b1 . 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)) #);

Lm1: for x being Element of INT.Ring holds x in REAL
proof end;

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 ;

Lm2: 0 in INT
by INT_1:def 2;

then Lm3: 0 = 0. INT.Ring
by FUNCT_7:def 1;

registration
cluster INT.Ring -> well-unital ;
coherence
INT.Ring is well-unital
proof end;
end;

Lm4: 1_ INT.Ring = 1
proof 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 abs a -> Element of INT.Ring equals :: INT_3:def 4
a if a >= 0. INT.Ring
otherwise - a;
coherence
|.a.| is Element of INT.Ring
proof end;
compatibility
for b1 being Element of INT.Ring holds
( ( a >= 0. INT.Ring implies ( b1 = |.a.| iff b1 = a ) ) & ( not a >= 0. INT.Ring implies ( b1 = |.a.| iff b1 = - a ) ) ) by Lm3, ABSVALUE:def 1;
consistency
for b1 being Element of INT.Ring holds verum ;
end;

:: deftheorem defines abs INT_3:def 4 :
for a being Element of INT.Ring holds
( ( a >= 0. INT.Ring implies abs a = a ) & ( not a >= 0. INT.Ring implies abs a = - a ) );

definition
func absint -> Function of the carrier of INT.Ring,NAT means :Def5: :: INT_3:def 5
 for a being Element of INT.Ring holds it . a = absreal . a;
existence
ex b1 being Function of the carrier of INT.Ring,NAT st
for a being Element of INT.Ring holds b1 . a = absreal . a
proof end;
uniqueness
for b1, b2 being Function of the carrier of INT.Ring,NAT st ( for a being Element of INT.Ring holds b1 . a = absreal . a ) & ( for a being Element of INT.Ring holds b2 . a = absreal . a ) holds
b1 = b2
proof end;
end;

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

theorem Th1: :: INT_3:1
for a being Element of INT.Ring holds absint . a = abs a
proof end;

Lm5: for a being Integer holds
( a = 0 or absreal . a >= 1 )
proof end;

Lm6: 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;

Lm7: 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 & 0. INT.Ring <= r & r < abs b )
proof end;

theorem Th2: :: 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 < abs b & a = (q2 * b) + r2 & 0. INT.Ring <= r2 & r2 < abs b holds
( q1 = q2 & r1 = r2 )
proof end;

definition
let a, b be Element of INT.Ring;
assume A1: b <> 0. INT.Ring ;
func a div b -> Element of INT.Ring means :Def6: :: INT_3:def 6
 ex r being Element of INT.Ring st
( a = (it * b) + r & 0. INT.Ring <= r & r < abs b );
existence
ex b1, r being Element of INT.Ring st
( a = (b1 * b) + r & 0. INT.Ring <= r & r < abs b )
proof end;
uniqueness
for b1, b2 being Element of INT.Ring st ex r being Element of INT.Ring st
( a = (b1 * b) + r & 0. INT.Ring <= r & r < abs b ) & ex r being Element of INT.Ring st
( a = (b2 * b) + r & 0. INT.Ring <= r & r < abs b ) holds
b1 = b2 by A1, Th2;
end;

:: deftheorem Def6 defines div INT_3:def 6 :
for a, b being Element of INT.Ring st b <> 0. INT.Ring holds
for b3 being Element of INT.Ring holds
( b3 = a div b iff ex r being Element of INT.Ring st
( a = (b3 * b) + r & 0. INT.Ring <= r & r < abs b ) );

definition
let a, b be Element of INT.Ring;
assume A1: b <> 0. INT.Ring ;
func a mod b -> Element of INT.Ring means :Def7: :: INT_3:def 7
 ex q being Element of INT.Ring st
( a = (q * b) + it & 0. INT.Ring <= it & it < abs b );
existence
ex b1, q being Element of INT.Ring st
( a = (q * b) + b1 & 0. INT.Ring <= b1 & b1 < abs b )
proof end;
uniqueness
for b1, b2 being Element of INT.Ring st ex q being Element of INT.Ring st
( a = (q * b) + b1 & 0. INT.Ring <= b1 & b1 < abs b ) & ex q being Element of INT.Ring st
( a = (q * b) + b2 & 0. INT.Ring <= b2 & b2 < abs b ) holds
b1 = b2 by A1, Th2;
end;

:: deftheorem Def7 defines mod INT_3:def 7 :
for a, b being Element of INT.Ring st b <> 0. INT.Ring holds
for b3 being Element of INT.Ring holds
( b3 = a mod b iff ex q being Element of INT.Ring st
( a = (q * b) + b3 & 0. INT.Ring <= b3 & b3 < abs b ) );

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

begin

definition
let I be non empty doubleLoopStr ;
attr I is Euclidian means :Def8: :: INT_3:def 8
 ex f being Function of the carrier 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 the carrier 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;

Lm8: for F being non empty almost_left_invertible associative commutative right_zeroed well-unital doubleLoopStr
for f being Function of the carrier 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 b1 being Ring st
( b1 is strict & b1 is Euclidian & b1 is domRing-like & not b1 is degenerated & b1 is distributive & b1 is commutative )
proof end;
end;

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

registration
cluster non empty non degenerated V77() 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 b1 being EuclidianRing st b1 is strict
proof end;
end;

definition
let E be non empty Euclidian doubleLoopStr ;
mode DegreeFunction of E -> Function of the carrier 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 b1 being Function of the carrier 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 b1 . r < b1 . b ) ) by Def8;
end;

:: deftheorem Def9 defines DegreeFunction INT_3:def 9 :
for E being non empty Euclidian doubleLoopStr
for b2 being Function of the carrier of E,NAT holds
( b2 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 b2 . r < b2 . b ) ) );

theorem Th4: :: INT_3:4
for E being EuclidianRing holds E is gcdDomain
proof end;

registration
cluster non empty non degenerated right_complementable associative commutative Abelian add-associative right_zeroed right-distributive well-unital domRing-like Euclidian -> non empty non degenerated right_complementable associative commutative Abelian add-associative right_zeroed right-distributive well-unital domRing-like gcd-like for doubleLoopStr ;
coherence
for b1 being non empty non degenerated right_complementable associative commutative Abelian add-associative right_zeroed right-distributive well-unital domRing-like doubleLoopStr st b1 is Euclidian holds
b1 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 b1 being non empty doubleLoopStr st b1 is commutative & b1 is associative & b1 is well-unital & b1 is almost_left_invertible & b1 is right_zeroed & b1 is almost_left_invertible holds
b1 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 the carrier of F,NAT holds f is DegreeFunction of F
proof end;

begin

definition
let n be Nat;
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 b1 being BinOp of (Segm n) st
for k, l being Element of Segm n holds b1 . (k,l) = (k * l) mod n
proof end;
uniqueness
for b1, b2 being BinOp of (Segm n) st ( for k, l being Element of Segm n holds b1 . (k,l) = (k * l) mod n ) & ( for k, l being Element of Segm n holds b2 . (k,l) = (k * l) mod n ) holds
b1 = b2
proof end;
end;

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

definition
let n be Nat;
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 b1 being UnOp of (Segm n) st
for k being Element of Segm n holds b1 . k = (n - k) mod n
proof end;
uniqueness
for b1, b2 being UnOp of (Segm n) st ( for k being Element of Segm n holds b1 . k = (n - k) mod n ) & ( for k being Element of Segm n holds b2 . k = (n - k) mod n ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines compint INT_3:def 11 :
for n being Nat st n > 0 holds
for b2 being UnOp of (Segm n) holds
( b2 = compint n iff for k being Element of Segm n holds b2 . 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;

Lm9: 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 Nat;
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 Nat 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 b1 being Ring st
( b1 is strict & b1 is degenerated & b1 is unital & b1 is distributive & b1 is almost_left_invertible & b1 is commutative ) by Th10;
end;

Lm10: 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;

Lm11: for n being Nat st 1 < n holds
1. (INT.Ring n) = 1
proof end;

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 V10() prime -> non zero for set ;
coherence
for b1 being Prime holds not b1 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 by Lm4;

theorem :: INT_3:14
for n being Nat st 1 < n holds
1. (INT.Ring n) = 1 by Lm11;

begin

:: 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 b1 being Ring st
( b1 is strict & b1 is infinite )
proof end;
end;