:: The Ring of Integers, Euclidean Rings and Modulo Integers
:: by Christoph Schwarzweller
::
:: Received February 4, 1999
:: Copyright (c) 1999-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, BINOP_2, SUBSET_1, FUNCT_1, BINOP_1, RELAT_1, ARYTM_1,
ALGSTR_0, FUNCT_7, CARD_1, STRUCT_0, XBOOLE_0, INT_1, ARYTM_3, SUPINF_2,
VECTSP_1, MESFUNC1, GROUP_1, RLVECT_1, LATTICES, VECTSP_2, COMPLEX1,
XXREAL_0, EUCLID, TARSKI, NAT_1, FUNCSDOM, GCD_1, INT_2, XCMPLX_0,
NEWTON, INT_3, MEMBERED, FINSET_1, ORDINAL1;
notations TARSKI, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, COMPLEX1, XTUPLE_0,
RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, EUCLID, XCMPLX_0, XXREAL_0, BINOP_2,
GR_CY_1, INT_1, FUNCT_7, NEWTON, INT_2, NAT_D, MEMBERED, STRUCT_0,
ALGSTR_0, RLVECT_1, GCD_1, GROUP_1, VECTSP_1, VECTSP_2;
constructors REAL_1, NAT_D, BINOP_2, NEWTON, FUNCT_7, GR_CY_1, EUCLID, GCD_1,
RELSET_1, XTUPLE_0, BINOP_1;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0,
XREAL_0, NAT_1, INT_1, NEWTON, STRUCT_0, VECTSP_1, GCD_1, VALUED_0,
MEMBERED, CARD_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin
definition
redefine func multint means
:: INT_3:def 1
for a,b being Element of INT holds it.(a, b) = multreal.(a,b);
end;
definition
redefine func compint means
:: INT_3:def 2
for a being Element of INT holds it.(a) = compreal.(a);
end;
definition
func INT.Ring -> doubleLoopStr equals
:: INT_3:def 3
doubleLoopStr(#INT,addint,multint,In(1,INT),In(0,INT)#);
end;
registration
cluster INT.Ring -> strict non empty;
end;
registration
cluster the carrier of INT.Ring -> integer-membered;
end;
registration
let a,b be Element of INT.Ring, c,d be Integer;
identify a * b with c * d when a = c, b = d;
identify a + b with c + d when a = c, b = d;
end;
registration
cluster INT.Ring -> well-unital;
end;
registration
cluster INT.Ring -> Abelian add-associative right_zeroed
right_complementable distributive commutative associative domRing-like non
degenerated;
end;
registration
let a be Element of INT.Ring, b be Integer;
identify -a with -b when a = b;
end;
definition
::$CD
let a be Element of INT.Ring;
redefine func |.a.| -> Element of INT.Ring;
end;
definition
func absint -> Function of INT.Ring,NAT means
:: INT_3:def 5
for a being Element of INT.Ring holds it.a = absreal.(a);
end;
theorem :: INT_3:1
for a being Element of INT.Ring holds absint.a = |.a.|;
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;
definition
::$CD 2
let a,b be Element of INT.Ring;
redefine func a div b -> Element of INT.Ring;
redefine func a mod b -> Element of INT.Ring;
end;
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);
begin :: Euclidian Domains
definition
let I be non empty doubleLoopStr;
attr I is Euclidian means
:: INT_3:def 8
ex f being Function of I,NAT st
for a,b being Element of I st b <> 0.I
ex q,r being Element of I st a = q * b + r & (r = 0.I or f.r < f.b);
end;
registration
cluster INT.Ring -> Euclidian;
end;
registration
cluster strict Euclidian domRing-like non degenerated distributive
commutative for Ring;
end;
definition
mode EuclidianRing is Euclidian domRing-like non degenerated distributive
commutative Ring;
end;
definition
let E be Euclidian non empty doubleLoopStr;
mode DegreeFunction of E -> Function of E,NAT means
:: INT_3:def 9
for a,b being Element of E st b <> 0.E
ex q,r being Element of E st a = q * b + r & (r = 0.E or it.r < it.b);
end;
theorem :: INT_3:4
for E being EuclidianRing holds E is gcdDomain;
registration
cluster Euclidian -> gcd-like for domRing-like Abelian
add-associative right_zeroed right_complementable associative commutative
well-unital right-distributive non degenerated doubleLoopStr;
end;
definition
redefine func absint -> DegreeFunction of INT.Ring;
end;
theorem :: INT_3:5
for F being commutative associative well-unital
almost_left_invertible right_zeroed non empty doubleLoopStr holds
F is Euclidian;
registration
cluster commutative associative well-unital almost_left_invertible
right_zeroed -> Euclidian for non empty doubleLoopStr;
end;
theorem :: INT_3:6
for F being commutative associative well-unital almost_left_invertible
right_zeroed non empty doubleLoopStr for f being Function of F,NAT
holds f is DegreeFunction of F;
begin :: Modulo Integers
definition
let n be natural Number such that
n > 0;
func multint(n) -> BinOp of Segm(n) means
:: INT_3:def 10
for k,l being Element of Segm(n) holds it.(k,l) = (k * l) mod n;
end;
definition
let n be natural Number such that
n > 0;
func compint(n) -> UnOp of Segm(n) means
:: INT_3:def 11
for k being Element of Segm (n) holds it.k = (n - k) mod n;
end;
theorem :: INT_3:7
for n being Nat st n > 0 for a,b being Element of
Segm(n) holds (a + b < n iff (addint(n)).(a,b) = a + b) & (a + b >= n iff (
addint(n)).(a,b) = (a + b) - n);
theorem :: INT_3:8
for n being Nat st n > 0 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;
theorem :: INT_3:9
for n being Nat st n > 0 for a being Element of Segm(n)
holds (a = 0 iff (compint(n)).(a) = 0) & (a <> 0 iff (compint(n)).(a) = n - a);
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))#);
end;
registration
let n be non zero Nat;
cluster INT.Ring(n) -> strict non empty;
end;
theorem :: INT_3:10
INT.Ring 1 is degenerated & INT.Ring 1 is Ring & INT.Ring 1 is
almost_left_invertible unital distributive commutative;
registration
cluster strict degenerated unital distributive almost_left_invertible
commutative for Ring;
end;
theorem :: INT_3:11
for n being Nat st n > 1 holds INT.Ring(n) is non
degenerated & INT.Ring(n) is well-unital distributive commutative Ring;
theorem :: INT_3:12
for p being Nat st p > 1 holds INT.Ring(p) is
add-associative right_zeroed right_complementable Abelian commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr iff p is Prime;
registration
cluster -> non zero for Prime;
end;
registration
let p be Prime;
cluster INT.Ring(p) -> add-associative right_zeroed right_complementable
Abelian commutative associative well-unital distributive almost_left_invertible
non degenerated;
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;
begin
:: from SCMRING3, 2011.08.19, A.T.
registration
cluster INT.Ring -> infinite;
end;
registration
cluster strict infinite for Ring;
end;