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