:: The Ring of Integers, Euclidean Rings and Modulo Integers
:: by Christoph Schwarzweller
::
:: Received February 4, 1999
:: Copyright (c) 1999-2026 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;
definitions RLVECT_1, STRUCT_0, GROUP_1, VECTSP_1, VECTSP_2, ALGSTR_0;
equalities STRUCT_0, ALGSTR_0, ORDINAL1;
expansions STRUCT_0, GROUP_1, VECTSP_1;
theorems TARSKI, BINOP_1, FUNCT_1, FUNCT_2, VECTSP_1, INT_1, RELAT_1, GCD_1,
RLVECT_1, EUCLID, ABSVALUE, GR_CY_1, NAT_1, INT_2, RELSET_1, ORDINAL1,
XCMPLX_1, NUMBERS, BINOP_2, GROUP_1, XREAL_1, COMPLEX1, XXREAL_0, NAT_D,
NEWTON, CARD_1, XTUPLE_0, SUBSET_1;
schemes NAT_1, BINOP_1, LMOD_7, BINOP_2;
begin
definition
redefine func multint means :: redefines multint (BINOP_2, definition)
:Def1:
for a,b being Element of INT holds it.(a, b) = multreal.(a,b);
compatibility
proof
let b be BinOp of INT;
hereby
assume
A1: b = multint;
let i1,i2 be Element of INT;
thus b.(i1,i2) = i1 * i2 by A1,BINOP_2:def 22
.= multreal.(i1,i2) by BINOP_2:def 11;
end;
assume
A2: for i1,i2 being Element of INT holds b.(i1,i2) = multreal.(i1,i2);
now
let i1,i2 be Element of INT;
thus b.(i1,i2) = multreal.(i1,i2) by A2
.= i1 * i2 by BINOP_2:def 11
.= multint.(i1,i2) by BINOP_2:def 22;
end;
hence b = multint by BINOP_1:2;
end;
end;
definition
redefine func compint means :: redefines compint (BINOP_2, definition)
for a being Element of INT holds it.(a) = compreal.(a);
compatibility
proof
let b be UnOp of INT;
hereby
assume
A1: b = compint;
let i be Element of INT;
thus b.i = -i by A1,BINOP_2:def 19
.= compreal.i by BINOP_2:def 7;
end;
assume
A2: for i being Element of INT holds b.i = compreal.i;
now
let i be Element of INT;
thus b.i = compreal.i by A2
.= -i by BINOP_2:def 7
.= compint.i by BINOP_2:def 19;
end;
hence b = compint by FUNCT_2:63;
end;
end;
definition
func INT.Ring -> doubleLoopStr equals
doubleLoopStr(#INT,addint,multint,In(1,INT),In(0,INT)#);
coherence;
end;
registration
cluster INT.Ring -> strict non empty;
coherence;
end;
registration
cluster the carrier of INT.Ring -> integer-membered;
coherence;
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;
compatibility
proof
assume
A1: a = c & b = d;
multint.(a,b) = multreal.(a,b) by Def1
.= c * d by A1,BINOP_2:def 11;
hence thesis;
end;
identify a + b with c + d when a = c, b = d;
compatibility
proof
assume
A2: a = c & b = d;
addint.(a,b) = addreal.(a,b) by GR_CY_1:def 1
.= c + d by A2,BINOP_2:def 9;
hence thesis;
end;
end;
set M = INT.Ring;
registration
cluster INT.Ring -> well-unital;
coherence;
end;
registration
cluster INT.Ring -> Abelian add-associative right_zeroed
right_complementable distributive commutative associative domRing-like non
degenerated;
coherence
proof
thus for a,b be Element of M holds a + b = b + a;
thus for a,b,c be Element of M holds (a + b) + c = a + (b + c);
thus for a being Element of M holds a + 0.M = a;
thus M is right_complementable
proof
let a be Element of M;
reconsider a9 = a as Integer;
reconsider v = -a9 as Element of M by INT_1:def 2;
take v;
thus thesis;
end;
thus for a,b,c be Element of M holds a*(b+c) = a*b+a*c & (b + c) * a = b *
a + c * a;
thus for x,y be Element of M holds x*y = y*x;
thus for a,b,c be Element of M holds a*b*c = a*(b*c);
thus for a,b be Element of M st a * b = 0.M holds a = 0.M or b = 0.M
by XCMPLX_1:6;
thus 0.M <> 1.M;
end;
end;
registration
let a be Element of INT.Ring, b be Integer;
identify -a with -b when a = b;
compatibility
proof
reconsider b9 = -b as Element of M by INT_1:def 2;
assume b = a;
then b9 + a = 0.M;
hence thesis by RLVECT_1:6;
end;
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;
compatibility;
end;
definition
::$CD
let a be Element of INT.Ring;
redefine func |.a.| -> Element of INT.Ring; :: redefines |. (COMPLEX1, definition)
coherence
proof
|.a.| in INT by INT_1:def 2;
hence thesis;
end;
end;
definition
func absint -> Function of INT.Ring,NAT means
:Def5:
for a being Element of INT.Ring holds it.a = absreal.(a);
existence
proof
dom(absreal) = REAL by FUNCT_2:def 1;
then
A1: dom((absreal)|INT) = the carrier of INT.Ring by NUMBERS:15,RELAT_1:62;
for y being object holds y in rng((absreal)|INT) implies y in NAT
proof
let y be object;
assume y in rng((absreal)|INT);
then consider x being object such that
A2: [x,y] in (absreal)|INT by XTUPLE_0:def 13;
A3: ((absreal)|INT).x = y by A2,FUNCT_1:1;
A4: x in dom((absreal)|INT) by A2,XTUPLE_0:def 12;
then reconsider x as Integer by A1;
A5: ((absreal)|INT).x = (absreal).x by A1,A4,FUNCT_1:49;
now
per cases;
case
A6: 0 <= x;
((absreal)|INT).x = |.x.| by A5,EUCLID:def 2
.= x by A6,ABSVALUE:def 1;
hence ((absreal)|INT).x is Element of NAT by A6,INT_1:3;
end;
case
A7: not 0 <= x;
((absreal)|INT).x = |.x.| by A5,EUCLID:def 2
.= -x by A7,ABSVALUE:def 1;
hence ((absreal)|INT).x is Element of NAT by A7,INT_1:3;
end;
end;
hence thesis by A3;
end;
then rng((absreal)|INT) c= NAT by TARSKI:def 3;
then reconsider
f = (absreal)|INT as Function of INT.Ring,NAT
by A1,FUNCT_2:def 1,RELSET_1:4;
take f;
thus thesis by FUNCT_1:49;
end;
uniqueness
proof
deffunc F(Element of INT.Ring)=absreal.($1);
thus for f1,f2 being Function of INT.Ring,NAT st (for x
being Element of INT.Ring holds f1.x = F(x)) & (for x being Element of INT.Ring
holds f2.x = F(x)) holds f1 = f2 from BINOP_2:sch 1;
end;
end;
theorem Th1:
for a being Element of INT.Ring holds absint.a = |.a.|
proof
let a be Element of INT.Ring;
reconsider a9 = a as Integer;
absint.a = absreal.a9 by Def5
.= |.a9.| by EUCLID:def 2;
hence thesis;
end;
Lm1: for a being Integer holds a = 0 or absreal.a >= 1
proof
let a be Integer;
assume
A1: a <> 0;
per cases;
suppose
0 <= a;
then reconsider a as Element of NAT by INT_1:3;
A2: absreal.(a) = |.a.| by EUCLID:def 2
.= a by ABSVALUE:def 1;
0 + 1 < a + 1 by A1,XREAL_1:6;
hence thesis by A2,NAT_1:13;
end;
suppose
A3: a < 0;
then a <= -1 by INT_1:8;
then
A4: -(-1) <= -a by XREAL_1:24;
absreal.(a) = |.a.| by EUCLID:def 2
.= -a by A3,ABSVALUE:def 1;
hence thesis by A4;
end;
end;
Lm2: for a,b being Element of INT.Ring st b <> 0.INT.Ring for b9 being Integer
st b9 = b holds 0 <= b9 implies ex q,r being Element of INT.Ring st a = q * b +
r & (r = 0.INT.Ring or absint.r < absint.b)
proof
let a,b be Element of M;
assume
A1: b <> 0.M;
reconsider a9 = a as Integer;
let b9 be Integer;
assume
A2: b9 = b;
defpred P[Nat] means ex s being Integer st $1 = a9 - s * b9;
assume
A3: 0 <= b9;
A4: ex k being Nat st P[k]
proof
now
per cases;
case
0 <= a9;
then reconsider a9 as Element of NAT by INT_1:3;
a9 - 0 * b9 = a9;
hence thesis;
end;
case
A5: a9 < 0;
1 + 0 <= b9 by A1,A2,A3,INT_1:7;
then 1 - 1 <= b9 - 1 by XREAL_1:9;
then reconsider m = b9 - 1 as Element of NAT by INT_1:3;
reconsider n = -a9 as Element of NAT by A5,INT_1:3;
a9 - a9 * b9 = (-a9) * (b9 - 1) & n * m is Element of NAT
by ORDINAL1:def 12;
hence thesis;
end;
end;
hence thesis;
end;
ex k being Nat st P[k] & for n being Nat st P[n] holds k <= n from
NAT_1:sch 5(A4);
then consider k9 being Nat such that
A6: ex s being Integer st k9 = a9 - s * b9 & for n being Nat st ex s9
being Integer st n = a9 - s9 * b9 holds k9 <= n;
consider l9 being Integer such that
A7: k9 = a9 - l9 * b9 by A6;
reconsider k = k9,l = l9 as Element of M by INT_1:def 2;
A8: k9 = 0 or k9 < b9
proof
assume k9 <> 0;
assume b9 <= k9;
then reconsider k = k9 - b9 as Element of NAT by INT_1:5;
A9: k9 > k
proof
reconsider b9 as Element of NAT by A3,INT_1:3;
assume k9 <= k;
then consider x being Nat such that
A10: k = k9 + x by NAT_1:10;
- x = b9 by A10;
hence contradiction by A1,A2;
end;
k9 - b9 = a9 - (l9 + 1) * b9 by A7;
hence thesis by A6,A9;
end;
A11: k = 0.M or absint.k < absint.b
proof
reconsider b9 as Element of NAT by A3,INT_1:3;
assume
A12: k <> 0.M;
A13: absint.k = absreal.(k) by Def5
.= |.k9.| by EUCLID:def 2
.= k9 by ABSVALUE:def 1;
absint.b = absreal.(b9) by A2,Def5
.= |.b9.| by EUCLID:def 2
.= b9 by ABSVALUE:def 1;
hence thesis by A8,A12,A13;
end;
k + l * b = a by A2,A7;
hence thesis by A11;
end;
theorem
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
let a,b,q1,q2,r1,r2 be Element of INT.Ring;
assume that
A1: b <> 0.INT.Ring and
A2: a = q1 * b + r1 and
A3: 0.INT.Ring <= r1 and
A4: r1 < |.b.| and
A5: a = q2 * b + r2 and
A6: 0.INT.Ring <= r2 and
A7: r2 < |.b.|;
reconsider r29 = r2, r19 = r1, q29 = q2, q19 = q1, b9 = b as Integer;
now
per cases;
case
A8: 0 <= r19 - r29;
A9: (q29 - q19) * b9 = r19 - r29 by A2,A5;
now
per cases;
case
0 = r19 - r29;
then q29 - q19 = 0 or b9 = 0 by A9,XCMPLX_1:6;
hence q1 = q2 by A1;
end;
case
0 <> r19 - r29;
then
A10: 0 <> q29 - q19 by A9;
A11: absreal.(q29 - q19) * absreal.b9 >= absreal.b9
proof
reconsider e = q2 + -q1 as Element of M;
reconsider d9 = q29 - q19 as Integer;
absreal.b9 = absint.b by Def5;
then reconsider c = absreal.b9 as Element of NAT;
absreal.d9 = absint.e by Def5;
then reconsider d = absreal.d9 as Element of NAT;
d * c >= 1 * c by A10,Lm1,NAT_1:4;
hence thesis;
end;
A12: r19 + -r29 <= r19 + 0 by A6,XREAL_1:6;
A13: |.b.| = absint.b by Th1
.= absreal.b by Def5;
r19 - r29 = |.((q29 - q19) * b9).| by A2,A5,A8,ABSVALUE:def 1
.= |.(q29 - q19).| * |.b9.| by COMPLEX1:65
.= absreal.(q29 - q19) * |.b9.| by EUCLID:def 2
.= absreal.(q29 - q19) * absreal.b9 by EUCLID:def 2;
hence q1 = q2 by A4,A11,A12,A13,XXREAL_0:2;
end;
end;
hence q1 = q2;
end;
case
A14: r19 - r29 < 0;
-(r19 - r29) = r29 - r19 & (q19 - q29) * b9 = r29 - r19 by A2,A5;
then
A15: 0 <> q19 - q29 by A14,XREAL_1:58;
A16: absreal.(q19 - q29) * absreal.b9 >= absreal.b9
proof
reconsider e = q1 + -q2 as Element of M;
reconsider d9 = q19 - q29 as Integer;
absreal.b9 = absint.b by Def5;
then reconsider c = absreal.b9 as Element of NAT;
absreal.d9 = absint.e by Def5;
then reconsider d = absreal.d9 as Element of NAT;
d * c >= 1 * c by A15,Lm1,NAT_1:4;
hence thesis;
end;
A17: |.b.| = absint.b by Th1
.= absreal.b by Def5;
-(r19 - r29) > 0 by A14,XREAL_1:58;
then
A18: r29 - r19 = |.((q19 - q29) * b9).| by A2,A5,ABSVALUE:def 1
.= |.(q19 - q29).| * |.b9.| by COMPLEX1:65
.= absreal.(q19 - q29) * |.b9.| by EUCLID:def 2
.= absreal.(q19 - q29) * absreal.b9 by EUCLID:def 2;
r29 + -r19 <= r29 + 0 by A3,XREAL_1:6;
hence q1 = q2 by A7,A16,A17,A18,XXREAL_0:2;
end;
end;
hence thesis by A2,A5;
end;
definition
::$CD 2
let a,b be Element of INT.Ring;
redefine func a div b -> Element of INT.Ring; :: redefines div (INT_1, definition)
coherence by INT_1:def 2;
redefine func a mod b -> Element of INT.Ring; :: redefines mod (INT_1, definition)
coherence by INT_1:def 2;
end;
theorem
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;
begin :: Euclidian Domains
definition
let I be non empty doubleLoopStr;
attr I is Euclidian means
:Def8:
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;
coherence
proof
take absint;
let a,b be Element of M;
reconsider b9 = b as Integer;
assume
A1: b <> 0.M;
now
per cases;
case
0 <= b9;
hence thesis by A1,Lm2;
end;
case
A2: b9 < 0;
reconsider c = -b9 as Element of M by INT_1:def 2;
0 < -b9 by A2,XREAL_1:58;
then consider q,r being Element of M such that
A3: a = q * c + r and
A4: r = 0.M or absint.r < absint.c by Lm2;
A5: r = 0.M or absint.r < absint.b
proof
assume
A6: r <> 0.M;
absint.c = absreal.c by Def5
.= |.-b9.| by EUCLID:def 2
.= -b9 by A2,ABSVALUE:def 1
.= |.b9.| by A2,ABSVALUE:def 1
.= absreal.(b9) by EUCLID:def 2
.= absint.b by Def5;
hence thesis by A4,A6;
end;
reconsider t = -q as Element of M;
t * b + r = a by A3;
hence
ex q,r being Element of M st a = q * b + r & (r = 0.M or absint.r
< absint.b) by A5;
end;
end;
hence thesis;
end;
end;
Lm4: for F being commutative associative well-unital almost_left_invertible
right_zeroed non empty doubleLoopStr for f being Function of F
,NAT for a,b being Element of F st b <> 0.F ex q,r being Element
of F st a = q * b + r & (r = 0.F or f.r < f.b)
proof
let F be commutative associative well-unital almost_left_invertible
right_zeroed non empty doubleLoopStr;
let f be Function of F,NAT;
now
let a,b be Element of F;
assume
A1: b <> 0.F;
ex q,r being Element of F st a = q * b + r & (r = 0.F or f.r < f.b)
proof
consider x being Element of F such that
A2: x * b = 1.F by A1,VECTSP_1:def 9;
(a * x) * b + 0.F = a * 1.F + 0.F by A2,GROUP_1:def 3
.= a + 0.F
.= a by RLVECT_1:def 4;
hence thesis;
end;
hence
b <> 0.F implies ex q,r being Element of F st a = q * b + r & (r = 0.
F or f.r < f.b);
end;
hence thesis;
end;
registration
cluster strict Euclidian domRing-like non degenerated distributive
commutative for Ring;
existence
proof
take INT.Ring;
thus thesis;
end;
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
:Def9:
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);
existence by Def8;
end;
theorem Th4:
for E being EuclidianRing holds E is gcdDomain
proof
let E be EuclidianRing;
set d = the DegreeFunction of E;
now
let x,y be Element of E;
now
per cases;
case
A1: x = 0.E;
y * 0.E = 0.E;
then
A2: y divides 0.E by GCD_1:def 1;
for zz being Element of E st zz divides x & zz divides y holds zz
divides y;
hence ex z being Element of E st z divides x & z divides y & for zz
being Element of E st zz divides x & zz divides y holds zz divides z by A1,A2;
end;
case
A3: x <> 0.E;
set M = { z where z is Element of E: ex s,t being Element of E st z =
s * x + t * y};
defpred P[Nat] means ex z being Element of E st (z in M & z <> 0.E &
$1 = d.z);
1.E * x + 0.E * y = 1.E * x by RLVECT_1:def 4
.= x;
then
A4: x in M;
ex k being Element of NAT st k = d.x;
then
A5: ex k being Nat st P[k] by A3,A4;
ex k being Nat st P[k] & for n being Nat st P[n] holds k <= n
from NAT_1:sch 5(A5);
then consider k being Nat such that
A6: ( P[k])& for n being Nat st P[n] holds k <= n;
consider g being Element of E such that
A7: g in M and
A8: g <> 0.E and
A9: k = d.g & for n being Nat st (ex z being Element of E st z in
M & z <> 0.E & n = d.z) holds k <= n by A6;
set G = { z where z is Element of E: ex r being Element of E st z = r
* g};
A10: for z being object holds z in M implies z in G
proof
let z be object;
assume z in M;
then consider z2 being Element of E such that
A11: z = z2 and
A12: ex s,t being Element of E st z2 = s * x + t * y;
consider u,v being Element of E such that
A13: z2 = u * x + v * y by A12;
reconsider z as Element of E by A11;
consider q,r being Element of E such that
A14: z = q * g + r and
A15: r = 0.E or d.r < d.g by A8,Def9;
r in M
proof
consider z1 being Element of E such that
A16: g = z1 and
A17: ex s,t being Element of E st z1 = s * x + t * y by A7;
consider s,t being Element of E such that
A18: z1 = s * x + t * y by A17;
z + (-(q * g)) = r + ((q * g) + (-(q * g))) by A14,RLVECT_1:def 3
.= r + 0.E by RLVECT_1:def 10
.= r by RLVECT_1:def 4;
then r = z + (-(q * (s * x) + q * (t * y))) by A16,A18,
VECTSP_1:def 7
.= z + ((-(q * (s * x))) + (-(q * (t * y)))) by RLVECT_1:31
.= ((u * x + v * y) + (-(q * (s * x)))) + (-(q * (t * y))) by A11
,A13,RLVECT_1:def 3
.= ((u * x + (-(q * (s * x)))) + v * y) + (-(q * (t * y))) by
RLVECT_1:def 3
.= (u * x + (-(q * (s * x)))) + (v * y + (-(q * (t * y)))) by
RLVECT_1:def 3
.= (u * x + ((-q) * (s * x))) + (v * y + (-(q * (t * y)))) by
GCD_1:48
.= (u * x + ((-q) * (s * x))) + (v * y + ((-q) * (t * y))) by
GCD_1:48
.= (u * x + ((-q) * s) * x) + (v * y + ((-q) * (t * y))) by
GROUP_1:def 3
.= (u * x + ((-q) * s) * x) + (v * y + ((-q) * t) * y) by
GROUP_1:def 3
.= (u + ((-q) * s)) * x + (v * y + ((-q) * t) * y) by
VECTSP_1:def 7
.= (u + ((-q) * s)) * x + (v + ((-q) * t)) * y by VECTSP_1:def 7;
hence thesis;
end;
then r = 0.E by A9,A15;
then z = q * g by A14,RLVECT_1:def 4;
hence thesis;
end;
A19: for z being Element of E holds z divides x & z divides y implies
z divides g
proof
let z be Element of E;
assume that
A20: z divides x and
A21: z divides y;
consider u being Element of E such that
A22: x = z * u by A20,GCD_1:def 1;
consider zz being Element of E such that
A23: g = zz and
A24: ex s,t being Element of E st zz = s * x + t * y by A7;
consider s,t being Element of E such that
A25: zz = s * x + t * y by A24;
consider v being Element of E such that
A26: y = z * v by A21,GCD_1:def 1;
g = (s * u) * z + t * (v * z) by A22,A26,A23,A25,GROUP_1:def 3
.= (s * u) * z + (t * v) * z by GROUP_1:def 3
.= (s * u + t * v) * z by VECTSP_1:def 7;
hence thesis by GCD_1:def 1;
end;
0.E * x + 1.E * y = 1.E * y by RLVECT_1:4
.= y;
then
A27: y in M;
for z being object holds z in G implies z in M
proof
let z be object;
assume z in G;
then consider z2 being Element of E such that
A28: z = z2 and
A29: ex s being Element of E st z2 = s * g;
reconsider z as Element of E by A28;
consider u being Element of E such that
A30: z2 = u * g by A29;
consider z1 being Element of E such that
A31: g = z1 and
A32: ex s,t being Element of E st z1 = s * x + t * y by A7;
consider s,t being Element of E such that
A33: z1 = s * x + t * y by A32;
z = u * (s * x) + u * (t * y) by A28,A30,A31,A33,VECTSP_1:def 2
.= (u * s) * x + u * (t * y) by GROUP_1:def 3
.= (u * s) * x + (u * t) * y by GROUP_1:def 3;
hence thesis;
end;
then
A34: M = G by A10,TARSKI:2;
g divides x & g divides y
proof
(ex zz being Element of E st x = zz & ex r being Element of E
st zz = r * g )& ex zzz being Element of E st y = zzz & ex r being Element of E
st zzz = r * g by A4,A27,A34;
hence thesis by GCD_1:def 1;
end;
hence ex z being Element of E st z divides x & z divides y & for zz
being Element of E st zz divides x & zz divides y holds zz divides z by A19;
end;
end;
hence ex z being Element of E st z divides x & z divides y & for zz being
Element of E st zz divides x & zz divides y holds zz divides z;
end;
hence thesis by GCD_1:def 11;
end;
registration
cluster Euclidian -> gcd-like for domRing-like Abelian
add-associative right_zeroed right_complementable associative commutative
well-unital right-distributive non degenerated doubleLoopStr;
coherence by Th4;
end;
definition
redefine func absint -> DegreeFunction of INT.Ring; :: redefines absint (INT_3, definition)
coherence
proof
let a,b be Element of M;
assume
A1: b <> 0.M;
per cases;
suppose 0 <= b;
hence thesis by A1,Lm2;
end;
suppose
A2: b < 0;
reconsider c = -b as Element of M;
0 < -b by A2,XREAL_1:58;
then consider q,r being Element of M such that
A3: a = q * c + r and
A4: r = 0.M or absint.r < absint.c by Lm2;
A5: r = 0.M or absint.r < absint.b
proof
assume
A6: r <> 0.M;
absint.c = absreal.c by Def5
.= |.-b.| by EUCLID:def 2
.= -b by A2,ABSVALUE:def 1
.= |.b.| by A2,ABSVALUE:def 1
.= absreal.(b) by EUCLID:def 2
.= absint.b by Def5;
hence thesis by A4,A6;
end;
reconsider t = -q as Element of M;
t * b + r = a by A3;
hence thesis by A5;
end;
end;
end;
theorem Th5:
for F being commutative associative well-unital
almost_left_invertible right_zeroed non empty doubleLoopStr holds
F is Euclidian
proof
let F be commutative associative well-unital almost_left_invertible
right_zeroed non empty doubleLoopStr;
set f = the Function of F,NAT;
for a,b being Element of F st b <> 0.F ex q,r being Element of F
st a = q * b + r & (r = 0.F or f.r < f.b) by Lm4;
hence thesis;
end;
registration
cluster commutative associative well-unital almost_left_invertible
right_zeroed -> Euclidian for non empty doubleLoopStr;
coherence by Th5;
end;
theorem
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
proof
let F be commutative associative well-unital almost_left_invertible
right_zeroed non empty doubleLoopStr;
let f be Function of F,NAT;
for a,b being Element of F st b <> 0.F ex q,r being Element of F
st a = q * b + r & (r = 0.F or f.r < f.b) by Lm4;
hence thesis by Def9;
end;
begin :: Modulo Integers
definition
let n be natural Number such that
A1: n > 0;
func multint(n) -> BinOp of Segm(n) means
:Def10:
for k,l being Element of Segm(n) holds it.(k,l) = (k * l) mod n;
existence
proof
reconsider n as non zero Nat by A1,TARSKI:1;
defpred P[Element of Segm(n),Element of Segm(n),set] means $3 = ($1 * $2)
mod n;
A2: for k,l being Element of Segm(n) ex c being Element of Segm(n) st P[k, l,c]
proof
let k,l be Element of Segm(n);
reconsider k9 = k,l9 = l as Element of NAT;
((k9*l9) mod n) < n by NAT_D:1;
then reconsider c = (k9*l9) mod n as Element of Segm(n) by NAT_1:44;
take c;
thus thesis;
end;
ex c being BinOp of Segm(n) st for k,l being Element of Segm(n) holds
P[k,l,c.(k,l)] from BINOP_1:sch 3(A2);
hence thesis;
end;
uniqueness
proof
reconsider n as non zero natural Number by A1;
deffunc O(Element of Segm(n),Element of Segm(n))=($1 * $2) mod n;
for o1,o2 being BinOp of Segm(n) st (for a,b being Element of Segm(n)
holds o1.(a,b) = O(a,b)) & (for a,b being Element of Segm(n) holds o2.(a,b) = O
(a,b)) holds o1 = o2 from BINOP_2:sch 2;
hence thesis;
end;
end;
definition
let n be natural Number such that
A1: n > 0;
func compint(n) -> UnOp of Segm(n) means
:Def11:
for k being Element of Segm (n) holds it.k = (n - k) mod n;
existence
proof
reconsider n as non zero Nat by A1,TARSKI:1;
set f = {[k,(n-k) mod n] where k is Element of NAT : k < n };
A2: for x being object st x in f ex y,z being object st x = [y,z]
proof
let x be object;
assume x in f;
then ex k being Element of NAT st x = [k,(n-k) mod n] & k < n;
hence thesis;
end;
for x,y1,y2 being object st [x,y1] in f & [x,y2] in f holds y1 = y2
proof
let x,y1,y2 be object;
assume that
A3: [x,y1] in f and
A4: [x,y2] in f;
consider k being Element of NAT such that
A5: [x,y1] = [k,(n-k)mod n] and
k < n by A3;
A6: y1 = (n-k)mod n by A5,XTUPLE_0:1;
consider k9 being Element of NAT such that
A7: [x,y2] = [k9,(n-k9) mod n] and
k9 < n by A4;
A8: y2 = (n-k9)mod n by A7,XTUPLE_0:1;
k = x by A5,XTUPLE_0:1
.= k9 by A7,XTUPLE_0:1;
hence thesis by A6,A8;
end;
then reconsider f as Function by A2,FUNCT_1:def 1,RELAT_1:def 1;
A9: for x being object holds x in Segm(n) implies x in dom f
proof
let x be object;
assume
A10: x in Segm(n);
then reconsider x as Element of NAT;
x < n by A10,NAT_1:44;
then [x,(n-x)mod n] in f;
hence thesis by XTUPLE_0:def 12;
end;
for x being object holds x in dom f implies x in Segm(n)
proof
let x be object;
assume x in dom f;
then consider y being object such that
A11: [x,y] in f by XTUPLE_0:def 12;
consider k being Element of NAT such that
A12: [x,y] = [k,(n-k)mod n] and
A13: k < n by A11;
x = k by A12,XTUPLE_0:1;
hence thesis by A13,NAT_1:44;
end;
then
A14: dom f = Segm(n) by A9,TARSKI:2;
for y being object holds y in rng f implies y in Segm(n)
proof
let y be object;
assume y in rng f;
then consider x being object such that
A15: [x,y] in f by XTUPLE_0:def 13;
consider k being Element of NAT such that
A16: [x,y] = [k,(n-k)mod n] and
A17: k < n by A15;
k - k < n - k by A17,XREAL_1:9;
then reconsider z = n - k as Element of NAT by INT_1:3;
A18: z mod n < n by NAT_D:1;
y = (n-k)mod n by A16,XTUPLE_0:1;
hence thesis by A18,NAT_1:44;
end;
then rng f c= Segm(n) by TARSKI:def 3;
then reconsider f as UnOp of Segm(n) by A14,FUNCT_2:def 1,RELSET_1:4;
for k being Element of Segm(n) holds f.k = (n - k) mod n
proof
let k be Element of Segm(n);
reconsider k as Element of NAT;
A0: (n-k)mod n is set by TARSKI:1;
k < n by NAT_1:44;
then [k,(n-k)mod n] in f;
hence thesis by A14,A0,FUNCT_1:def 2;
end;
hence thesis;
end;
uniqueness
proof
reconsider n as non zero Nat by A1,TARSKI:1;
deffunc F(Element of Segm(n))=(n - $1) mod n;
for f1,f2 being UnOp of Segm(n) st (for a being Element of Segm(n)
holds f1.a = F(a)) & (for a being Element of Segm(n) holds f2.a = F(a)) holds
f1 = f2 from LMOD_7:sch 2;
hence thesis;
end;
end;
theorem Th7:
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)
proof
let n be Nat;
assume
A1: n > 0;
let a,b be Element of Segm(n);
reconsider n as non zero Nat by A1;
consider c being Element of NAT such that
A2: c = (a + b) mod n;
consider t being Nat such that
A3: a + b = n * t + c & c < n or c = 0 & n = 0 by A2,NAT_D:def 2;
A4: now
assume
A5: a + b >= n;
t = 1
proof
now
per cases;
case
t = 0;
hence thesis by A3,A5;
end;
case
A6: t <> 0;
t < 2
proof
a < n & b < n by NAT_1:44;
then
A7: n * t + c >= n * t & a + b < n * 1 + n * 1 by NAT_1:11,XREAL_1:8;
assume t >= 2;
then n * t >= n * 2 by XREAL_1:64;
hence thesis by A3,A7,XXREAL_0:2;
end;
then t < 1 + 1;
then
A8: t <= 1 by NAT_1:13;
1 + 0 <= t by A6,INT_1:7;
hence thesis by A8,XXREAL_0:1;
end;
end;
hence thesis;
end;
hence (addint(n)).(a,b) = (a + b) - n by A2,A3,GR_CY_1:def 4;
end;
A9: (addint(n)).(a,b) = (a + b) - n implies a + b >= n
proof
assume (addint(n)).(a,b) = (a + b) - n;
then
A10: (a + b) mod n = (a + b) - n by GR_CY_1:def 4;
consider t being Nat such that
A11: a + b = n * t + ((a + b) mod n) and
((a + b) mod n) < n by NAT_D:def 2;
assume
A12: a + b < n;
t = 0
proof
assume t <> 0;
then 1 + 0 <= t by INT_1:7;
then
A13: 1 * n <= t * n by XREAL_1:64;
t * n <= t * n + ((a + b) mod n) by NAT_1:11;
hence thesis by A12,A11,A13,XXREAL_0:2;
end;
hence thesis by A10,A11;
end;
A14: now
assume
A15: a + b < n;
t = 0
proof
assume t <> 0;
then 1 + 0 <= t by INT_1:7;
then
A16: 1 * n <= t * n by XREAL_1:64;
n * t <= n * t + c by NAT_1:11;
hence thesis by A3,A15,A16,XXREAL_0:2;
end;
hence (addint(n)).(a,b) = a + b by A2,A3,GR_CY_1:def 4;
end;
(addint(n)).(a,b) = (a + b) implies a + b < n
proof
assume (addint(n)).(a,b) = (a + b);
then (a + b) mod n = a + b by GR_CY_1:def 4;
hence thesis by NAT_D:1;
end;
hence thesis by A14,A9,A4;
end;
Lm5: for a,b being Nat st b <> 0
ex k being Element of NAT st k * b <= a & a < (k + 1) * b
proof
let a,b be Nat;
set k9 = a div b;
assume b <> 0;
then
A1: ex t being Nat st a = b * k9 + t & t < b by NAT_D:def 1;
(k9 + 1) * b = k9 * b + b;
then (k9 + 1) * b > a by A1,XREAL_1:6;
hence thesis by A1,NAT_1:11;
end;
theorem Th8:
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
proof
let n be Nat;
assume
A1: n > 0;
let a,b be Element of Segm(n);
reconsider a, b as Element of NAT by ORDINAL1:def 12;
let k be Nat;
A2: now
assume that
A3: k * n <= a * b and
A4: a * b < (k + 1) * n;
consider c being Element of NAT such that
A5: c = (a * b) mod n;
consider t being Nat such that
A6: a * b = n * t + c & c < n or c = 0 & n = 0 by A5,NAT_D:def 2;
now
consider q being Nat such that
A7: a * b = k * n + q by A3,NAT_1:10;
t = k
proof
now
per cases;
case
t <= k;
then consider r being Nat such that
A8: t + r = k by NAT_1:10;
A9: n * t + c = t * n + (r * n + q) by A1,A6,A7,A8;
now
per cases;
case
t = k;
hence thesis;
end;
case
A10: t <> k;
r >= 1
proof
assume
A11: r < 1;
r = 0
proof
assume r <> 0;
then 1 + 0 <= r by INT_1:7;
hence thesis by A11;
end;
hence thesis by A8,A10;
end;
then r * n >= 1 * n by NAT_1:4;
then
A12: r * n + q >= 1 * n + q by XREAL_1:6;
1 * n + q >= n by NAT_1:11;
hence thesis by A1,A6,A9,A12,XXREAL_0:2;
end;
end;
hence thesis;
end;
case
t > k;
then t >= k + 1 by INT_1:7;
then
A13: n * t >= n * (k + 1) by NAT_1:4;
n * t + c >= n * t by NAT_1:11;
hence thesis by A4,A6,A13,XXREAL_0:2;
end;
end;
hence thesis;
end;
hence (multint(n)).(a,b) = a * b - k * n by A1,A5,A6,Def10;
end;
hence (multint(n)).(a,b) = a * b - k * n;
end;
now
assume (multint(n)).(a,b) = a * b - k * n;
then (a * b) mod n = a * b - k * n by A1,Def10;
then
A14: (a * b - k * n) + k * n >= 0 + k * n & ex t being Nat st a * b = n * t
+ (a * b - n * k) & (a * b - n * k) < n by A1,NAT_D:def 2,XREAL_1:6;
(k + 1) * n = k * n + n;
hence k * n <= a * b & a * b < (k + 1) * n by A14,XREAL_1:6;
end;
hence thesis by A2;
end;
theorem
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)
proof
let n be Nat;
assume
A1: n > 0;
let a be Element of Segm(n);
reconsider n as non zero Nat by A1;
reconsider a as Element of NAT by ORDINAL1:def 12;
A2: a < n by NAT_1:44;
then a - a < n - a by XREAL_1:9;
then reconsider b = n - a as Element of NAT by INT_1:3;
consider c being Element of NAT such that
A3: c = b mod n;
A4: (compint(n)).(a) = 0 implies a = 0
proof
a - a < n - a by A2,XREAL_1:9;
then reconsider a9 = n - a as Element of NAT by INT_1:3;
assume
A5: (compint(n)).(a) = 0;
n <= n + a by NAT_1:11;
then
A6: n - a <= (n + a) - a by XREAL_1:9;
consider t being Nat such that
A7: a9 = n * t + (a9 mod n) and
a9 mod n < n by NAT_D:def 2;
assume a <> 0;
then n - a <> n;
then
A8: n - a < n by A6,XXREAL_0:1;
t = 0
proof
assume t <> 0;
then 1 + 0 <= t by INT_1:7;
then
A9: 1 * n <= t * n by XREAL_1:64;
t * n <= t * n + (a9 mod n) by NAT_1:11;
hence thesis by A8,A7,A9,XXREAL_0:2;
end;
then a9 = 0 by A5,A7,Def11;
hence thesis by NAT_1:44;
end;
consider t being Nat such that
A10: b = n * t + c & c < n or c = 0 & n = 0 by A3,NAT_D:def 2;
A11: n - a <= n
proof
assume n - a > n;
then (n - a) + a > n + a by XREAL_1:6;
hence thesis by NAT_1:11;
end;
A12: now
assume
A13: a = 0;
A14: t = 1
proof
now
per cases;
case
t = 0;
hence thesis by A10,A13;
end;
case
A15: t <> 0;
t < 2
proof
assume t >= 2;
then
A16: n * t >= n * 2 by XREAL_1:64;
A17: n <= n * 1 + n * 1 by NAT_1:11;
n * t + c >= n * t by NAT_1:11;
then n - a >= n * 2 by A10,A16,XXREAL_0:2;
then n * 1 = 2 * n by A13,A17,XXREAL_0:1;
hence thesis by A1;
end;
then t < 1 + 1;
then
A18: t <= 1 by NAT_1:13;
1 + 0 <= t by A15,INT_1:7;
hence thesis by A18,XXREAL_0:1;
end;
end;
hence thesis;
end;
c = 0
proof
assume c <> 0;
then n + c > n + 0 by XREAL_1:6;
hence thesis by A10,A11,A14;
end;
hence (compint(n)).(a) = 0 by A3,Def11;
end;
now
assume
A19: a <> 0;
A20: n - a < n
proof
assume n - a >= n;
then n - a = n by A11,XXREAL_0:1;
hence thesis by A19;
end;
t = 0
proof
assume t <> 0;
then 1 + 0 <= t by INT_1:7;
then
A21: 1 * n <= t * n by XREAL_1:64;
n * t <= n * t + c by NAT_1:11;
hence thesis by A10,A20,A21,XXREAL_0:2;
end;
hence (compint(n)).(a) = n - a by A3,A10,Def11;
end;
hence thesis by A12,A4;
end;
definition
let n be natural Number;
func INT.Ring(n) -> doubleLoopStr equals
doubleLoopStr(#Segm(n),addint(n),
multint(n),In (1,Segm(n)),In (0,Segm(n))#);
coherence;
end;
registration
let n be non zero Nat;
cluster INT.Ring(n) -> strict non empty;
coherence;
end;
theorem Th10:
INT.Ring 1 is degenerated & INT.Ring 1 is Ring & INT.Ring 1 is
almost_left_invertible unital distributive commutative
proof
set n = 1, R = INT.Ring n;
A1: for x being Element of R st x <> 0.R ex y be Element of R st y*x = 1.R
proof
let x be Element of R;
assume x <> 0.R;
then x <> 0 by SUBSET_1:def 8;
hence thesis by CARD_1:49,TARSKI:def 1;
end;
A2: for a,b being Element of R holds a + b = b + a
proof
let a,b be Element of R;
thus a + b = 0 by CARD_1:49,TARSKI:def 1
.= b + a by CARD_1:49,TARSKI:def 1;
end;
A3: for a being Element of R holds a + 0.R = a
proof
let a be Element of R;
a = 0 by CARD_1:49,TARSKI:def 1;
hence thesis by CARD_1:49,TARSKI:def 1;
end;
A4: for a,b,c being Element of R holds (a * b) * c = a * (b * c)
proof
let a,b,c be Element of R;
thus (a * b) * c = 0 by CARD_1:49,TARSKI:def 1
.= a * (b * c) by CARD_1:49,TARSKI:def 1;
end;
A5: for a being Element of R holds a + (-a) = 0.R
proof
let a be Element of R;
thus a + (-a) = 0 by CARD_1:49,TARSKI:def 1
.= 0.R by CARD_1:49,TARSKI:def 1;
end;
A6: R is right_complementable
proof
let v be Element of R;
take -v;
thus thesis by A5;
end;
A7: for a,b,c being Element of R holds (a + b) + c = a + (b + c)
proof
let a,b,c be Element of R;
thus (a + b) + c = 0 by CARD_1:49,TARSKI:def 1
.= a + (b + c) by CARD_1:49,TARSKI:def 1;
end;
A8: for a being Element of R holds 1.R * a = a & a * 1.R = a
proof
let a be Element of R;
A9: a * 1.R = 0 by CARD_1:49,TARSKI:def 1
.= a by CARD_1:49,TARSKI:def 1;
1.R * a = 0 by CARD_1:49,TARSKI:def 1
.= a by CARD_1:49,TARSKI:def 1;
hence thesis by A9;
end;
A10: R is well-unital
by A8;
A11: for a,b being Element of R holds a * b = b * a
proof
let a,b be Element of R;
thus a * b = 0 by CARD_1:49,TARSKI:def 1
.= b * a by CARD_1:49,TARSKI:def 1;
end;
A12: for a,b,c being Element of R holds a * (b + c) = a * b + a * c
proof
let a,b,c be Element of R;
thus a * (b + c) = 0 by CARD_1:49,TARSKI:def 1
.= a * b + a * c by CARD_1:49,TARSKI:def 1;
end;
A13: for a,b,c being Element of R holds (b + c) * a = b * a + c * a
proof
let a,b,c be Element of R;
thus (b + c) * a = 0 by CARD_1:49,TARSKI:def 1
.= b * a + c * a by CARD_1:49,TARSKI:def 1;
end;
0.R = 0 by CARD_1:49,TARSKI:def 1
.= 1.R by CARD_1:49,TARSKI:def 1;
hence thesis by A1,A2,A11,A7,A4,A3,A13,A12,A6,A10,GROUP_1:def 3,RLVECT_1:def
2,def 3,def 4,VECTSP_1:def 7;
end;
registration
cluster strict degenerated unital distributive almost_left_invertible
commutative for Ring;
existence by Th10;
end;
Lm6: now
let a, n be Nat;
assume 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;
then n-a < n-0 by XREAL_1:15;
hence n-a in Segm n by A1,NAT_1:44;
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:
for n being Nat st n > 1 holds INT.Ring(n) is non
degenerated & INT.Ring(n) is well-unital distributive commutative Ring
proof
let n be Nat;
assume
A1: n > 1;
then reconsider n as non zero Nat;
set F = INT.Ring(n);
A2: 1.F = 1 by A1,Lm7;
A3: for a being Element of F holds 1.F * a = a & a * 1.F = a
proof
let a be Element of F;
reconsider a9 = a as Element of Segm(n);
A4: 1 * a9 < (0 + 1) * n & 1 is Element of Segm(n) by A1,NAT_1:44;
then
A5: (multint(n)).(a,1) = a9 - 0 * n by Th8
.= a9;
(multint(n)).(1,a) = a9 - 0 * n by A4,Th8
.= a9;
hence thesis by A1,A5,Lm7;
end;
A6: F is well-unital
by A3;
A7: for a,b being Element of F holds a + b = b + a
proof
let a,b be Element of F;
reconsider a9 = a as Element of Segm(n);
reconsider b9 = b as Element of Segm(n);
now
per cases;
case
A8: a9 + b9 < n;
hence (addint(n)).(a,b) = a9 + b9 by Th7
.= (addint(n)).(b,a) by A8,Th7;
end;
case
A9: a9 + b9 >= n;
hence (addint(n)).(a,b) = (a9 + b9) - n by Th7
.= (addint(n)).(b,a) by A9,Th7;
end;
end;
hence thesis;
end;
A10: for a,b,c being Element of F holds (a * b) * c = a * (b * c)
proof
let a,b,c be Element of F;
reconsider a9 = a, b9 = b, c9 = c as Element of Segm(n);
reconsider aa = a9 as Element of NAT;
reconsider aa as Integer;
reconsider bb = b9 as Element of NAT;
reconsider bb as Integer;
reconsider cc = c9 as Element of NAT;
reconsider cc as Integer;
A11: cc < n by NAT_1:44;
aa < n by NAT_1:44;
then
A12: (a9 * ((b9 * c9) mod n)) mod n = ((aa mod n) * (bb * cc mod n)) mod n
by NAT_D:63
.= (aa * (bb * cc)) mod n by NAT_D:67
.= ((aa * bb) * cc) mod n
.= (((aa * bb) mod n) * (cc mod n)) mod n by NAT_D:67
.= (((a9 * b9) mod n) * c9) mod n by A11,NAT_D:63;
(aa * bb) mod n < n by NAT_D:62;
then
A13: (a9 * b9) mod n is Element of Segm(n) by NAT_1:44;
(bb * cc) mod n < n by NAT_D:62;
then
A14: (b9 * c9) mod n is Element of Segm(n) by NAT_1:44;
A15: a * (b * c) = (multint(n)).(a9, (b9 * c9) mod n) by Def10
.= (a9 * ((b9 * c9) mod n)) mod n by A14,Def10;
(a * b) * c = (multint(n)).((a9 * b9) mod n, c9) by Def10
.= (((a9 * b9) mod n) * c9) mod n by A13,Def10;
hence thesis by A15,A12;
end;
A16: for a,b being Element of F holds a * b = b * a
proof
let a,b be Element of F;
reconsider a9 = a as Element of Segm(n);
reconsider b9 = b as Element of Segm(n);
consider k being Element of NAT such that
A17: k * n <= a9 * b9 & a9 * b9 < (k + 1) * n by Lm5;
(multint(n)).(a9,b9) = a9 * b9 - k * n by A17,Th8
.= (multint(n)).(b9,a9) by A17,Th8;
hence thesis;
end;
A18: for a,b,c being Element of F holds (a + b) + c = a + (b + c)
proof
let a,b,c be Element of F;
reconsider a9 = a, b9 = b, c9 = c as Element of Segm(n);
reconsider aa = a9 as Element of NAT;
reconsider aa as Integer;
reconsider bb = b9 as Element of NAT;
reconsider bb as Integer;
reconsider cc = c9 as Element of NAT;
reconsider cc as Integer;
A19: cc < n by NAT_1:44;
aa < n by NAT_1:44;
then
A20: (a9 + ((b9 + c9) mod n)) mod n = ((aa mod n) + (bb + cc mod n)) mod n
by NAT_D:63
.= (aa + (bb + cc)) mod n by NAT_D:66
.= ((aa + bb) + cc) mod n
.= (((aa + bb) mod n) + (cc mod n)) mod n by NAT_D:66
.= (((a9 + b9) mod n) + c9) mod n by A19,NAT_D:63;
(aa + bb) mod n < n by NAT_D:62;
then
A21: (a9 + b9) mod n is Element of Segm(n) by NAT_1:44;
(bb + cc) mod n < n by NAT_D:62;
then
A22: (b9 + c9) mod n is Element of Segm(n) by NAT_1:44;
A23: a + (b + c) = (addint(n)).(a9, (b9 + c9) mod n) by GR_CY_1:def 4
.= (a9 + ((b9 + c9) mod n)) mod n by A22,GR_CY_1:def 4;
(a + b) + c = (addint(n)).((a9 + b9) mod n, c9) by GR_CY_1:def 4
.= (((a9 + b9) mod n) + c9) mod n by A21,GR_CY_1:def 4;
hence thesis by A23,A20;
end;
0 in Segm(n) by NAT_1:44;
then
A24: 0.F = 0 by SUBSET_1:def 8;
A25: for a being Element of F holds a + 0.F = a
proof
let a be Element of F;
reconsider a9 = a as Element of Segm(n);
a9 + 0 < n by NAT_1:44;
hence thesis by A24,Th7;
end;
A26: F is right_complementable
proof
let a be Element of F;
reconsider a9 = a as Element of Segm(n);
reconsider a9 as Element of NAT;
per cases;
suppose
A27: a9 = 0;
take 0.F;
thus thesis by A24,A25,A27;
end;
suppose
a9 <> 0;
then reconsider b = n-a9 as Element of Segm n by Lm6;
reconsider v = b as Element of F;
take v;
thus a + v = (a9+b) mod n by GR_CY_1:def 4
.= 0.F by A24,NAT_D:25;
end;
end;
A28: for a,b,c being Element of F holds (b + c) * a = b * a + c * a
proof
let a,b,c be Element of F;
reconsider a9 = a, b9 = b, c9 = c as Element of Segm(n);
reconsider aa = a9 as Element of NAT;
reconsider aa as Integer;
reconsider bb = b9 as Element of NAT;
reconsider bb as Integer;
reconsider cc = c9 as Element of NAT;
reconsider cc as Integer;
A29: aa < n by NAT_1:44;
A30: (((b9 * a9) mod n) + ((c9 * a9) mod n)) mod n = (bb * aa + cc * aa)
mod n by NAT_D:66
.= ((bb + cc) * aa) mod n
.= (((bb + cc) mod n) * (aa mod n)) mod n by NAT_D:67
.= (((b9 + c9) mod n) * a9) mod n by A29,NAT_D:63;
(bb + cc) mod n < n by NAT_D:62;
then
A31: (b9 + c9) mod n is Element of Segm(n) by NAT_1:44;
(cc * aa) mod n < n by NAT_D:62;
then
A32: (c9 * a9) mod n is Element of Segm(n) by NAT_1:44;
(bb * aa) mod n < n by NAT_D:62;
then
A33: (b9 * a9) mod n is Element of Segm(n) by NAT_1:44;
A34: (b + c) * a = (multint(n)).((b9 + c9) mod n, a9) by GR_CY_1:def 4
.= (((b9 + c9) mod n) * a9) mod n by A31,Def10;
b * a + c * a = (addint(n)).((multint(n)).(b,a),(c9 * a9) mod n) by Def10
.= (addint(n)).((b9 * a9) mod n,(c9 * a9) mod n) by Def10
.= (((b9 * a9) mod n) + ((c9 * a9) mod n)) mod n by A33,A32,GR_CY_1:def 4
;
hence thesis by A34,A30;
end;
for a,b,c being Element of F holds a * (b + c) = a * b + a * c
proof
let a,b,c be Element of F;
thus a * (b + c) = (b + c) * a by A16
.= b * a + c * a by A28
.= a * b + c * a by A16
.= a * b + a * c by A16;
end;
then reconsider F as commutative Ring by A7,A16,A18,A10,A25,A28,A26,A6,
GROUP_1:def 3,def 12,RLVECT_1:def 2,def 3,def 4,VECTSP_1:def 7;
F is non degenerated by A24,A2;
hence thesis;
end;
theorem Th12:
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
proof
let p be Nat;
assume
A1: p > 1;
then reconsider p as non zero Nat;
reconsider P = INT.Ring(p) as Ring by A1,Th11;
reconsider p as non zero Element of NAT by ORDINAL1:def 12;
A2: now
assume
A3: INT.Ring(p) is add-associative right_zeroed right_complementable
Abelian commutative associative well-unital distributive almost_left_invertible
non degenerated non empty doubleLoopStr;
for n being Nat holds n divides p implies n = 1 or n = p
proof
let n be Nat;
assume n divides p;
then consider k being Nat such that
A4: p = n * k by NAT_D:def 3;
A5: n <= p
proof
assume
A6: n > p;
now
per cases;
case
k = 0;
hence thesis by A4;
end;
case
A7: k <> 0;
then k >= 1 + 0 by INT_1:7;
then k * p >= 1 * p by XREAL_1:64;
hence thesis by A4,A6,A7,XREAL_1:68;
end;
end;
hence thesis;
end;
A8: k <= p
proof
assume
A9: k > p;
now
per cases;
case
n = 0;
hence thesis by A4;
end;
case
A10: n <> 0;
then n >= 1 + 0 by INT_1:7;
then n * p >= 1 * p by XREAL_1:64;
hence thesis by A4,A9,A10,XREAL_1:68;
end;
end;
hence thesis;
end;
now
per cases;
case
k = p;
then 1 * p = p * n by A4;
hence thesis by XCMPLX_1:5;
end;
case
k <> p;
then
A11: k < p by A8,XXREAL_0:1;
now
per cases;
case
n = p;
then 1 * p = k * p by A4;
then k = 1 by XCMPLX_1:5;
hence thesis by A4;
end;
case
n <> p;
then n < p by A5,XXREAL_0:1;
then reconsider n2 = n as Element of Segm(p) by NAT_1:44;
0 in Segm p by NAT_1:44;
then
A12: 0 = 0.(INT.Ring p) by SUBSET_1:def 8;
k <> 0 by A4;
then
A13: k <> 0.(INT.Ring(p)) by A12;
reconsider k2 = k as Element of Segm(p) by A11,NAT_1:44;
reconsider n9 = n2 as Element of INT.Ring(p);
reconsider k9 = k2 as Element of INT.Ring(p);
n <> 0 by A4;
then
A14: n <> 0.(INT.Ring(p)) by A12;
n9 * k9 = (n2 * k2) mod p by Def10
.= 0.(INT.Ring(p)) by A12,A4,INT_1:62;
hence contradiction by A3,A14,A13,VECTSP_1:12;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence p is Prime by A1,INT_2:def 4;
end;
now
assume
A15: p is Prime;
for a being Element of P st a <> 0.P ex b be Element of P st b * a = 1.P
proof
reconsider e = 1 as Integer;
let a be Element of P;
reconsider a9 = a as Element of Segm(p);
reconsider a9 as Element of NAT;
reconsider a2 = a9 as Integer;
1 * p = p;
then
A16: 1 divides p by NAT_D:def 3;
assume
A17: a <> 0.P;
A18: for m being Nat st m divides a9 & m divides p holds m divides 1
proof
let m be Nat;
assume that
A19: m divides a9 and
A20: m divides p;
consider k being Nat such that
A21: a9 = m * k by A19,NAT_D:def 3;
m <= a9
proof
assume
A22: m > a9;
now
per cases;
case
k = 0;
hence thesis by A17,A21,SUBSET_1:def 8;
end;
case
A23: k <> 0;
then k >= 1 + 0 by INT_1:7;
then k * a9 >= 1 * a9 by XREAL_1:64;
hence thesis by A21,A22,A23,XREAL_1:68;
end;
end;
hence thesis;
end;
then m <> p by NAT_1:44;
hence thesis by A15,A20,INT_2:def 4;
end;
1 * a9 = a9;
then 1 divides a9 by NAT_D:def 3;
then a9 gcd p = 1 by A16,A18,NAT_D:def 5;
then consider s,t being Integer such that
A24: 1 = s * a9 + t * p by NAT_D:68;
s mod p >= 0;
A25: s mod p is Element of NAT by INT_1:3;
s mod p < p by NAT_D:62;
then reconsider b9 = s mod p as Element of Segm(p) by NAT_1:44;
reconsider b = b9 as Element of P;
b * a = (a9 * b9) mod p by Def10
.= ((a2 mod p) * ((s mod p) mod p)) mod p by NAT_D:67
.= ((a2 mod p) * (s mod p)) mod p by NAT_D:65
.= (a2 * s) mod p by NAT_D:67
.= e mod p by A24,NAT_D:61
.= e by A1,NAT_D:63
.= 1.P by A1,Lm7;
hence thesis;
end;
hence INT.Ring(p) is add-associative right_zeroed right_complementable
Abelian commutative associative well-unital distributive almost_left_invertible
non degenerated non empty doubleLoopStr by A1,Th11,VECTSP_1:def 9;
end;
hence thesis by A2;
end;
registration
cluster -> non zero for Prime;
coherence
proof
let k be Prime;
assume k is zero;
then k in SetPrimenumber 2 by NEWTON:def 7;
hence contradiction;
end;
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;
coherence
proof
p > 1 by INT_2:def 4;
hence thesis by Th12;
end;
end;
theorem
1.INT.Ring = 1;
theorem
for n being Nat st 1 < n holds 1.INT.Ring(n) = 1 by Lm7;
begin
:: from SCMRING3, 2011.08.19, A.T.
registration
cluster INT.Ring -> infinite;
coherence;
end;
registration
cluster strict infinite for Ring;
existence
proof
take INT.Ring;
thus thesis;
end;
end;