Volume 11, 1999

University of Bialystok

Copyright (c) 1999 Association of Mizar Users

### The abstract of the Mizar article:

### The Ring of Integers, Euclidean Rings and Modulo Integers

**by****Christoph Schwarzweller**- Received February 4, 1999
- MML identifier: INT_3

- [ Mizar article, MML identifier index ]

environ vocabulary BINOP_1, INT_1, FUNCT_1, VECTSP_1, RELAT_1, ARYTM_1, GR_CY_1, FUNCT_7, RLVECT_1, VECTSP_2, LATTICES, ABSVALUE, EUCLID, NAT_1, FUNCSDOM, GCD_1, ARYTM_3, INT_2, MCART_1, ORDINAL2, NAT_LAT, INT_3; notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL2, NUMBERS, XCMPLX_0, XREAL_0, RLVECT_1, MCART_1, RELAT_1, FUNCT_1, STRUCT_0, FUNCT_2, GCD_1, VECTSP_1, VECTSP_2, FUNCSDOM, BINOP_1, REAL_1, EUCLID, GR_CY_1, INT_1, FUNCT_7, NAT_LAT, INT_2, NAT_1, GROUP_1; constructors DOMAIN_1, GROUP_2, REAL_1, GCD_1, NAT_1, EUCLID, GR_CY_1, FUNCT_7, NAT_LAT, ALGSTR_2, SEQ_1, MEMBERED; clusters STRUCT_0, FUNCT_1, VECTSP_2, XREAL_0, INT_1, RELSET_1, GCD_1, SEQ_1, MEMBERED, NUMBERS, ORDINAL2; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin definition func multint -> BinOp of INT means :: INT_3:def 1 for a,b being Element of INT holds it.(a,b) = multreal.(a,b); end; definition func compint -> UnOp of INT 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; definition cluster INT.Ring -> strict non empty; end; definition cluster INT.Ring -> Abelian add-associative right_zeroed right_complementable well-unital distributive commutative associative domRing-like non degenerated; end; definition let a,b be Element of INT.Ring; pred a <= b means :: INT_3:def 4 ex a',b' being Integer st a' = a & b' = b & a' <= b'; reflexivity; connectedness; synonym b >= a; antonym b < a; antonym a > b; end; definition let a be Element of INT.Ring; func abs(a) -> Element of INT.Ring equals :: INT_3:def 5 a if a >= 0.INT.Ring otherwise - a; end; definition func absint -> Function of the carrier of INT.Ring,NAT means :: INT_3:def 6 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 = abs(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 < abs(b) & a = q2 * b + r2 & 0.INT.Ring <= r2 & r2 < abs(b) holds q1 = q2 & r1 = r2; definition let a,b be Element of INT.Ring; assume b <> 0.INT.Ring; func a div b -> Element of INT.Ring means :: INT_3:def 7 ex r being Element of INT.Ring st a = it * b + r & 0.INT.Ring <= r & r < abs(b); end; definition let a,b be Element of INT.Ring; assume b <> 0.INT.Ring; func a mod b -> Element of INT.Ring means :: INT_3:def 8 ex q being Element of INT.Ring st a = q * b + it & 0.INT.Ring <= it & it < abs(b); 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); ::: Euclidian Domains :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: begin definition let I be non empty doubleLoopStr; attr I is Euclidian means :: INT_3:def 9 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; definition cluster INT.Ring -> Euclidian; end; definition cluster strict Euclidian domRing-like non degenerated well-unital distributive commutative Ring; end; definition mode EuclidianRing is Euclidian domRing-like non degenerated well-unital distributive commutative Ring; end; definition cluster strict EuclidianRing; end; definition let E be Euclidian (non empty doubleLoopStr); mode DegreeFunction of E -> Function of the carrier of E,NAT means :: INT_3:def 10 (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)))); end; theorem :: INT_3:4 for E being EuclidianRing holds E is gcdDomain; definition cluster Euclidian -> gcd-like (domRing-like non degenerated Abelian add-associative right_zeroed right_complementable associative commutative right_unital right-distributive (non empty doubleLoopStr)); end; definition redefine func absint -> DegreeFunction of INT.Ring; end; theorem :: INT_3:5 for F being commutative associative left_unital Field-like right_zeroed (non empty doubleLoopStr) holds F is Euclidian; definition cluster commutative associative left_unital Field-like right_zeroed Field-like -> Euclidian (non empty doubleLoopStr); end; theorem :: INT_3:6 for F being commutative associative left_unital Field-like right_zeroed (non empty doubleLoopStr) for f being Function of the carrier of F,NAT holds f is DegreeFunction of F; ::: Some Theorems about DIV and MOD :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: begin canceled; theorem :: INT_3:8 for n being Nat st n > 0 for a,k being Integer holds (a + n * k) div n = (a div n) + k & (a + n * k) mod n = a mod n; theorem :: INT_3:9 for n being Nat st n > 0 for a being Integer holds a mod n >= 0 & a mod n < n; theorem :: INT_3:10 for n being Nat st n > 0 for a being Integer holds ((0 <= a & a < n) implies a mod n = a) & ((0 > a & a >= -n) implies a mod n = n + a); theorem :: INT_3:11 for n being Nat st n > 0 for a being Integer holds a mod n = 0 iff n divides a; theorem :: INT_3:12 for n being Nat st n > 0 for a,b being Integer holds a mod n = b mod n iff a,b are_congruent_mod n; theorem :: INT_3:13 for n being Nat st n > 0 for a being Integer holds (a mod n) mod n = a mod n; theorem :: INT_3:14 for n being Nat st n > 0 for a,b being Integer holds (a + b) mod n = ((a mod n) + (b mod n)) mod n; theorem :: INT_3:15 for n being Nat st n > 0 for a,b being Integer holds (a * b) mod n = ((a mod n) * (b mod n)) mod n; theorem :: INT_3:16 for a,b being Integer ex s,t being Integer st a gcd b = s * a + t * b; ::: Modulo Integers :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: begin definition let n be Nat such that n > 0; func multint(n) -> BinOp of Segm(n) means :: INT_3:def 11 for k,l being Element of Segm(n) holds it.(k,l) = (k * l) mod n; end; definition let n be Nat such that n > 0; func compint(n) -> UnOp of Segm(n) means :: INT_3:def 12 for k being Element of Segm(n) holds it.k = (n - k) mod n; end; theorem :: INT_3:17 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:18 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:19 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 Nat; func INT.Ring(n) -> doubleLoopStr equals :: INT_3:def 13 doubleLoopStr(#Segm(n),addint(n),multint(n),In (1,Segm(n)),In (0,Segm(n))#); end; definition let n be Nat; cluster INT.Ring(n) -> strict non empty; end; theorem :: INT_3:20 INT.Ring 1 is degenerated & INT.Ring 1 is Ring & INT.Ring 1 is Field-like well-unital distributive commutative; definition cluster strict degenerated well-unital distributive Field-like commutative Ring; end; theorem :: INT_3:21 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:22 for p being Nat st p > 1 holds INT.Ring(p) is add-associative right_zeroed right_complementable Abelian commutative associative left_unital distributive Field-like non degenerated (non empty doubleLoopStr) iff p is Prime; definition let p be Prime; cluster INT.Ring(p) -> add-associative right_zeroed right_complementable Abelian commutative associative left_unital distributive Field-like non degenerated; end;

Back to top