:: Linear Congruence Relation and Complete Residue Systems
:: by Xiquan Liang , Li Yan and Junjie Zhao
::
:: Received August 28, 2007
:: Copyright (c) 2007-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, INT_1, NAT_1, SUBSET_1, MEMBERED, MEMBER_1, TARSKI,
REAL_1, ARYTM_3, FUNCT_1, RELAT_1, FINSET_1, CARD_1, XBOOLE_0, ARYTM_1,
INT_2, XXREAL_0, COMPLEX1, NEWTON, SQUARE_1, PARTFUN1, EQREL_1, RELAT_2,
EULER_1, FINSEQ_1, FINSEQ_3, ORDINAL4, CARD_3, XCMPLX_0, PRE_POLY, NAT_3,
UPROOTS, INT_4;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, MEMBERED,
XXREAL_0, XCMPLX_0, XREAL_0, INT_1, REAL_1, INT_2, NAT_D, NEWTON,
SQUARE_1, RELAT_1, FUNCT_1, FINSEQ_1, RELSET_1, RVSUM_1, EULER_1,
EQREL_1, RELAT_2, PARTFUN1, FINSET_1, NAT_3, UPROOTS, TREES_4, WSIERP_1,
MEASURE6, INTEGRA2, RECDEF_1, PRE_POLY;
constructors EULER_1, REAL_1, WELLORD2, BINARITH, WSIERP_1, PEPIN, UPROOTS,
NAT_3, NAT_D, MEASURE6, INTEGRA2, RECDEF_1, RELSET_1, NUMBERS;
registrations RELAT_1, FINSEQ_1, CARD_1, PARTFUN1, NAT_1, INT_1, MEMBERED,
FINSET_1, NEWTON, NAT_3, XXREAL_0, NUMBERS, XREAL_0, ORDINAL1, FUNCT_1,
VALUED_0, RELSET_1, PEPIN;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions FUNCT_1, RELAT_2, PARTFUN1, TARSKI, XBOOLE_0, WELLORD2;
equalities FINSEQ_1, XCMPLX_0, EULER_1, XBOOLE_0, ORDINAL1;
expansions FUNCT_1, INT_1, FINSEQ_1, XBOOLE_0;
theorems FINSEQ_3, FINSEQ_2, ABSVALUE, FINSEQ_5, EULER_2, CARD_2, SEQ_2,
RELAT_2, RELSET_1, EQREL_1, ORDERS_1, FINSEQ_4, MOEBIUS1, XBOOLE_0,
NAT_3, NEWTON, INT_2, WSIERP_1, CARD_1, PEPIN, NAT_1, XCMPLX_1, XREAL_1,
ORDINAL1, EULER_1, FINSEQ_1, XBOOLE_1, TARSKI, ZFMISC_1, RVSUM_1, INT_1,
FUNCT_1, XXREAL_0, NAT_D, XREAL_0, INTEGRA2, VALUED_0, FUNCT_2, MEMBER_1,
MEMBERED, XTUPLE_0, NUMBERS;
schemes NAT_1, FINSEQ_1, FINSEQ_2, RELSET_1, CLASSES1;
begin
reserve a,b,m,x,y,i1,i2,i3,i for Integer,
k,p,q,n for Nat,
c,c1,c2 for Element of NAT,
z for set;
theorem Th1:
for X being real-membered set, a being Real holds X, a ++ X are_equipotent
proof
let X be real-membered set, a be Real;
deffunc F(Real) = a + $1;
consider f being Function such that
A1: dom f = X & for x being Element of REAL st x in X holds f.x = F(x)
from CLASSES1:sch 2;
A2: rng f = a ++ X
proof
thus rng f c= a ++ X
proof
let z be object;
assume z in rng f;
then consider x being object such that
A3: x in dom f and
A4: z = f.x by FUNCT_1:def 3;
reconsider x as Real by A1,A3;
reconsider x as Element of REAL by XREAL_0:def 1;
a + x in REAL by XREAL_0:def 1;
then reconsider z9= z as Element of REAL by A1,A3,A4;
z9 = a + x by A1,A3,A4;
hence thesis by A1,A3,MEMBER_1:141;
end;
let z be object;
assume
A5: z in (a ++ X);
then reconsider z as Element of REAL;
consider x being Complex such that
A6: z = a + x and
A7: x in X by A5,MEMBER_1:143;
X c= REAL by MEMBERED:3; then
reconsider x as Element of REAL by A7;
f.x = z by A1,A7,A6;
hence thesis by A1,A7,FUNCT_1:def 3;
end;
take f;
f is one-to-one
proof
let x,y be object;
assume that
A8: x in dom f and
A9: y in dom f and
A10: f.x = f.y;
reconsider x,y as Element of REAL by A1,A8,A9,XREAL_0:def 1;
f.x = a + x by A1,A8;
then a + x = a + y by A1,A9,A10;
hence thesis;
end;
hence thesis by A1,A2;
end;
registration
let X be finite real-membered set, a be Real;
cluster a ++ X -> finite;
coherence by Th1,CARD_1:38;
end;
theorem Th2:
for X being real-membered set, a being Real holds card X = card (a ++ X)
by Th1,CARD_1:5;
Lm1: for a being Integer, X being Subset of INT holds a ++ X c= INT
proof
let a be Integer, X be Subset of INT;
let x be object;
assume
A1: x in a ++ X;
then reconsider x9 = x as Real;
consider y being Complex such that
A2: x9 = a + y and
A3: y in X by A1,MEMBER_1:143;
reconsider y9 = y as Integer by A3;
x9 = a + y9 by A2;
hence thesis by INT_1:def 2;
end;
Lm2: for a being Integer, X being Subset of INT holds a ** X c= INT
proof
let a be Integer, X be Subset of INT;
let x be object;
assume
A1: x in a ** X;
then reconsider x9 = x as Real;
consider y being Complex such that
A2: x9 = a * y and
A3: y in X by A1,MEMBER_1:195;
reconsider y9 = y as Integer by A3;
x9 = a * y9 by A2;
hence thesis by INT_1:def 2;
end;
Lm3: for X being Subset of INT, a being Integer holds x in a ** X iff ex y
being Integer st y in X & x = a * y
proof
let X be Subset of INT, a be Integer;
hereby
assume x in a ** X;
then consider z being Complex such that
A1: x = a * z and
A2: z in X by MEMBER_1:195;
reconsider z as Integer by A2;
take z;
thus z in X & x = a * z by A2,A1;
end;
given y being Integer such that
A3: y in X & x = a * y;
reconsider x9 = x as Real;
reconsider y as Real;
ex z being Real st z in X & x9 = a * z
by A3;
hence thesis by MEMBER_1:193;
end;
theorem Th3:
for X being real-membered set, a being Real st a <> 0
holds X, a ** X are_equipotent
proof
let X be real-membered set, a be Real;
deffunc F(Real) = a * $1;
consider f being Function such that
A1: dom f = X & for x being Element of REAL st x in X holds f.x = F(x)
from CLASSES1:sch 2;
assume
A2: a <> 0;
A3: f is one-to-one
proof
let x,y be object;
assume that
A4: x in dom f & y in dom f and
A5: f.x = f.y;
reconsider x,y as Element of REAL by A1,A4,XREAL_0:def 1;
f.x = a * x & f.y = a * y by A1,A4;
hence thesis by A2,A5,XCMPLX_1:5;
end;
take f;
rng f = a ** X
proof
thus rng f c= a ** X
proof
let z be object;
assume z in rng f;
then consider x being object such that
A6: x in dom f and
A7: z = f.x by FUNCT_1:def 3;
reconsider x9 = x as Element of REAL by A1,A6,XREAL_0:def 1;
z = a * x9 by A1,A6,A7;
hence thesis by A1,A6,MEMBER_1:193;
end;
let z be object;
assume
A8: z in (a ** X);
then reconsider z as Element of REAL;
consider x being Complex such that
A9: z = a * x and
A10: x in X by A8,MEMBER_1:195;
reconsider x as Element of REAL by A10,XREAL_0:def 1;
f.x = z by A1,A10,A9;
hence thesis by A1,A10,FUNCT_1:def 3;
end;
hence thesis by A1,A3;
end;
theorem Th4:
for X being real-membered set, a being Real holds (a = 0 &
X is non empty implies a ** X = {0}) & (a ** X = {0} implies a = 0 or X = {0})
proof
let X be real-membered set, a be Real;
thus a = 0 & X is non empty implies a ** X = {0}
proof
assume that
A1: a = 0 and
A2: X is non empty;
thus a ** X c= {0}
proof
let i be object;
assume
A3: i in a ** X;
then reconsider i as Real;
ex x being Complex st
i = a * x & x in X by A3,MEMBER_1:195;
hence thesis by A1,TARSKI:def 1;
end;
then a ** X = {} or a ** X = {0} by ZFMISC_1:33;
hence thesis by A2,INTEGRA2:7;
end;
assume that
A4: a ** X = {0} and
A5: a <> 0;
X,a ** X are_equipotent by A5,Th3;
then consider x being object such that
A6: X = {x} by A4,CARD_1:28;
A7: x in X by A6,TARSKI:def 1;
then reconsider x as Real;
a * x in a ** X by A7,MEMBER_1:193;
then a * x = 0 by A4,TARSKI:def 1;
hence thesis by A5,A6,XCMPLX_1:6;
end;
registration
let X be finite real-membered set, a be Real;
cluster a ** X -> finite;
coherence
proof
per cases;
suppose
a <> 0;
hence thesis by Th3,CARD_1:38;
end;
suppose
A1: a = 0;
per cases;
suppose
X is empty;
hence thesis by INTEGRA2:7;
end;
suppose
X is non empty;
hence thesis by A1,Th4;
end;
end;
end;
end;
theorem Th5:
for X being real-membered set, a being Real st a <> 0
holds card X = card (a ** X)
by Th3,CARD_1:5;
begin
Lm4: i1 divides i2 & i1 divides i3 implies i1 divides (i2-i3)
proof
assume that
A1: i1 divides i2 and
A2: i1 divides i3;
consider i4 being Integer such that
A3: i2=i1*i4 by A1;
consider i5 being Integer such that
A4: i3=i1*i5 by A2;
i2-i3=i1*(i4-i5) by A3,A4;
hence thesis;
end;
Lm5: i divides a & i divides (a-b) implies i divides b
proof
assume that
A1: i divides a and
A2: i divides (a-b);
A3: b=-(a-b)+a;
i divides -(a-b) by A2,INT_2:10;
hence thesis by A1,A3,WSIERP_1:4;
end;
Lm6: p is prime & p,n are_coprime implies not p divides n
proof
assume that
A1: p is prime and
A2: p,n are_coprime;
assume p divides n;
then n gcd p = p by NEWTON:49;
then n gcd p >1 by A1,INT_2:def 4;
hence contradiction by A2,INT_2:def 3;
end;
Lm7: p>0 implies p >= 1+0 by NAT_1:13;
theorem Th6:
i divides i1 & i1<>0 implies |.i.|<=|.i1.|
proof
assume i divides i1 & i1<>0;
then |.i1.|<>0 & |.i.| divides |.i1.| by ABSVALUE:2,INT_2:16;
hence thesis by NAT_D:7;
end;
theorem Th7:
for i3 st i3 <> 0 holds i1 divides i2 iff i1*i3 divides i2*i3
proof
let i3;
assume
A1: i3<>0;
thus i1 divides i2 implies i1*i3 divides i2*i3
proof
assume i1 divides i2;
then consider i4 being Integer such that
A2: i2=i1*i4;
i2*i3=(i1*i3)*i4 by A2;
hence thesis;
end;
assume (i1*i3) divides (i2*i3);
then consider i5 being Integer such that
A3: (i2*i3)=(i1*i3)*i5;
i2*i3=(i1*i5)*i3 by A3;
then i2=i1*i5 by A1,XCMPLX_1:5;
hence thesis;
end;
theorem
for a,b,m,n being Nat st a mod m = b mod m
holds (a|^n) mod m = (b|^n) mod m
proof
let a,b,m,n be Nat;
defpred P[Nat] means (a|^$1) mod m = (b|^$1) mod m;
assume
A1: a mod m = b mod m;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A3: P[k];
reconsider l1=a|^k,l2=b|^k,a,b,m as Element of NAT by ORDINAL1:def 12;
(a|^(k+1)) mod m = ((a|^k)*a) mod m by NEWTON:6
.=((l1 mod m)*(a mod m)) mod m by NAT_D:67
.= (l2*b) mod m by A1,A3,NAT_D:67
.= (b|^(k+1)) mod m by NEWTON:6;
hence thesis;
end;
a|^0 = 1 by NEWTON:4;
then
A4: P[0] by NEWTON:4;
for k being Nat holds P[k] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem Th9:
i1*i,i2*i are_congruent_mod i3 & i,i3 are_coprime implies
i1,i2 are_congruent_mod i3
proof
assume that
A1: i1*i,i2*i are_congruent_mod i3 and
A2: i,i3 are_coprime;
i3 divides (i1*i-i2*i) by A1;
then i3 divides (i1-i2)*i;
then i3 divides (i1-i2) by A2,INT_2:25;
hence thesis;
end;
theorem Th10:
i1,i2 are_congruent_mod i3 implies i1*k,i2*k are_congruent_mod i3*k
proof
assume i1,i2 are_congruent_mod i3;
then consider i4 being Integer such that
A1: i3*i4=i1-i2;
(i3*k)*i4=(i3*i4)*k .=(i1+(-i2))*k by A1
.=i1*k-i2*k;
hence thesis;
end;
theorem Th11:
i1,i2 are_congruent_mod i implies i1*i3,i2*i3 are_congruent_mod i
proof
assume i1,i2 are_congruent_mod i;
then i divides (i1-i2);
then i divides (i1-i2)*i3 by INT_2:2;
then i divides (i1*i3-i2*i3);
hence thesis;
end;
::$CT
Th12:
for i being Integer holds 0 = 0 mod i by INT_1:73;
theorem Th13:
for b st b>0 for a ex q,r being Integer st a=(b*q)+r & r>=0 & r< b
proof
let b;
assume
A1: b>0;
let a be Integer;
per cases;
suppose
A2: a>=0;
A3: b in NAT by A1,INT_1:3;
a in NAT by A2,INT_1:3;
then consider k,t being Nat such that
A4: a=(b*k)+t & t<b by A1,A3,NAT_1:17;
take k,t;
thus thesis by A4;
end;
suppose
A5: a<0;
A6: b in NAT by A1,INT_1:3;
-a in NAT by A5,INT_1:3;
then consider k,t being Nat such that
A7: -a=(b*k)+t and
A8: t<b by A1,A6,NAT_1:17;
per cases;
suppose
A9: t=0;
take q=-k,r=0;
a=b*(-k) by A7,A9;
hence a=b*q+r;
thus thesis by A1;
end;
suppose
A10: t<>0;
take q=-k-1,r=b-t;
a=b*(-k-1)+(b-t) by A7;
hence a=b*q+r;
thus thesis by A8,A10,XREAL_1:44,50;
end;
end;
end;
::$CT
theorem Th15:
a,m are_coprime implies ex x being Integer st (a*x-b) mod m = 0
proof
assume a,m are_coprime;
then a gcd m = 1 by INT_2:def 3;
then consider s,t being Integer such that
A1: 1=s*a+t*m by NAT_D:68;
take b*s;
(a*b*s-b) mod m = ((a*s-1)*b) mod m .= ((-(m*t))*b) mod m by A1
.= (0+m*((-t)*b)) mod m
.= 0 mod m by NAT_D:61
.= 0 by Th12;
hence thesis;
end;
theorem Th16:
m>0 & a,m are_coprime implies ex n being Nat st (a*n-b) mod m = 0
proof
assume that
A1: m>0 and
A2: a,m are_coprime;
consider x being Integer such that
A3: (a*x-b) mod m = 0 by A2,Th15;
consider q,n being Integer such that
A4: x=(m*q)+n and
A5: n>=0 and
n<m by A1,Th13;
A6: (a*x-b) mod m = ((a*q)*m+(a*n-b)) mod m by A4
.= (a*n-b) mod m by NAT_D:61;
n in NAT by A5,INT_1:3;
then reconsider n as Nat;
take n;
thus thesis by A3,A6;
end;
theorem
m<>0 & not (a gcd m) divides b implies not ex x being Integer st (a*x-
b) mod m = 0
proof
assume that
A1: m<>0 and
A2: not (a gcd m) divides b;
given y such that
A3: (a*y-b) mod m = 0;
(a gcd m) divides m by INT_2:21;
then
A4: ex i being Integer st m=(a gcd m)*i;
(a*y-b) mod m = 0 mod m by A3,Th12;
then (a*y-b),0 are_congruent_mod m by A1,NAT_D:64;
then (a*y-b),0 are_congruent_mod (a gcd m) by A4,INT_1:20;
then
A5: (a gcd m) divides (a*y-b-0);
(a gcd m) divides a*y by INT_2:2,21;
hence contradiction by A2,A5,Lm5;
end;
theorem
m<>0 & (a gcd m) divides b implies ex x being Integer st (a*x-b) mod m = 0
proof
assume that
A1: m<>0 and
A2: (a gcd m) divides b;
consider a1,m1 being Integer such that
A3: a = (a gcd m)*a1 and
A4: m = (a gcd m)*m1 and
A5: a1,m1 are_coprime by A1,INT_2:23;
consider b1 being Integer such that
A6: b = (a gcd m)*b1 by A2;
A7: m1<>0 by A1,A4;
consider y being Integer such that
A8: (a1*y-b1) mod m1 = 0 by A5,Th15;
take y;
(a1*y-b1) mod m1 = 0 mod m1 by A8,Th12;
then a1*y-b1,0 are_congruent_mod m1 by A7,NAT_D:64;
then (a1*y-b1)*(a gcd m), (a gcd m)*(0 qua Nat) are_congruent_mod m1*(a gcd
m) by Th10;
then (a*y-b) mod m = 0 mod m by A3,A4,A6,NAT_D:64;
hence thesis by Th12;
end;
begin
theorem Th19:
n>0 & p>0 implies p*q mod p|^n = p*(q mod p|^(n-'1))
proof
assume that
A1: n>0 and
A2: p>0;
A3: n>=0+1 by A1,NAT_1:13;
p*(q mod p|^(n-'1)) = p*(q-(q div p|^(n-'1))*p|^(n-'1)) by A2,NEWTON:63
.= p*q-(q div p|^(n-'1))*(p*p|^(n-'1))
.= p*q-(q div p|^(n-'1))*(p|^(n-'1+1)) by NEWTON:6
.= p*q-(q div p|^(n-'1))*p|^n by A3,XREAL_1:235;
then
A4: p*q=(q div p|^(n-'1))*p|^n+p*(q mod p|^(n-'1));
p*(q mod p|^(n-'1)) < p*p|^(n-'1) by A2,NAT_D:1,XREAL_1:68;
then p*(q mod p|^(n-'1)) < p|^(n-'1+1) by NEWTON:6;
then p*(q mod p|^(n-'1)) < p|^n by A3,XREAL_1:235;
hence thesis by A4,NAT_D:def 2;
end;
theorem
p*q mod p*n = p*(q mod n)
proof
per cases;
suppose
A1: n=0;
then q mod n = 0;
hence thesis by A1;
end;
suppose
A2: n>0;
then
A3: p*q = p*(n * (q div n) + (q mod n)) by NAT_D:2
.= (p*n)*(q div n) + p*(q mod n);
per cases;
suppose
p=0;
hence thesis;
end;
suppose
p>0;
then p*(q mod n) < p*n by A2,NAT_D:1,XREAL_1:68;
hence thesis by A3,NAT_D:def 2;
end;
end;
end;
theorem Th21:
n>0 & p is prime & p,q are_coprime implies not p divides (q mod p|^n)
proof
assume that
A1: n>0 and
A2: p is prime and
A3: p,q are_coprime;
n>=0+1 by A1,NAT_1:13;
then p|^1 divides p|^n by NEWTON:89;
then p divides p|^n;
then
A4: p divides p|^n*(q div p|^n) by NAT_D:9;
q=p|^n*(q div p|^n)+(q mod p|^n) by A2,NAT_D:2;
hence thesis by A2,A3,A4,Lm6,NAT_D:8;
end;
theorem Th22:
for p,q,n being Nat st n>0 holds (p - q) mod n = 0 iff p mod n = q mod n
proof
let p,q,n be Nat;
assume
A1: n>0;
thus (p - q) mod n = 0 implies p mod n = q mod n
proof
assume (p - q) mod n = 0;
then n divides (p - q) by A1,INT_1:62;
then consider s being Integer such that
A2: n * s = p - q;
per cases by XXREAL_0:1;
suppose
p > q;
then s > 0 by A2,XREAL_1:50;
then s in NAT by INT_1:3;
then reconsider s9=s as Nat;
p mod n = (n * s9 + q) mod n by A2
.= q mod n by NAT_D:21;
hence thesis;
end;
suppose
p = q;
hence thesis;
end;
suppose
A3: p < q;
A4: q - p = n * (-s) by A2;
then (-s) > 0 by A3,XREAL_1:50;
then (-s) in NAT by INT_1:3;
then reconsider s9=(-s) as Nat;
q - p = n * s9 by A4;
then q mod n = (n * s9 + p) mod n .= p mod n by NAT_D:21;
hence thesis;
end;
end;
assume
A5: p mod n = q mod n;
p = n * (p div n) + (p mod n) by A1,NAT_D:2
.= n * (p div n) + (q - n * (q div n)) by A1,A5,NEWTON:63
.= q + n * ((p div n) - (q div n));
then n divides (p - q);
hence thesis;
end;
theorem
for a,b,m being Nat st m > 0 holds a mod m = b mod m iff m divides (a- b)
proof
let a,b,m be Nat;
assume
A1: m > 0;
thus a mod m = b mod m implies m divides (a-b)
proof
assume a mod m = b mod m;
then (a - b) mod m = 0 by A1,Th22;
hence thesis by A1,INT_1:62;
end;
assume m divides (a - b);
then (a - b) mod m = 0;
hence thesis by A1,Th22;
end;
theorem
n>0 & p is prime & p,q are_coprime implies not ex x being
Integer st (p*x^2 - q) mod p|^n = 0
proof
assume that
A1: n>0 and
A2: p is prime and
A3: p,q are_coprime;
given x such that
A4: (p*x^2 - q) mod p|^n = 0;
(p*x^2) mod p|^n = q mod p|^n by A2,A4,Th22;
then p*(x^2 mod p|^(n-'1)) = q mod p|^n by A1,A2,Th19;
then p divides q mod p|^n;
hence contradiction by A1,A2,A3,Th21;
end;
theorem
n>0 & p is prime & p,q are_coprime implies not ex x being
Integer st (p*x - q) mod p|^n = 0
proof
assume that
A1: n>0 and
A2: p is prime and
A3: p,q are_coprime;
A4: p > 1 by A2,INT_2:def 4;
given x being Integer such that
A5: (p*x - q) mod p|^n = 0;
per cases;
suppose
x>=0;
then x in NAT by INT_1:3;
then reconsider x as Nat;
(p*x) mod p|^n = q mod p|^n by A2,A5,Th22;
then p*(x mod p|^(n-'1)) = q mod p|^n by A1,A2,Th19;
then p divides q mod p|^n;
hence contradiction by A1,A2,A3,Th21;
end;
suppose
x<0;
then -x in NAT by INT_1:3;
then reconsider l=-x as Nat;
A6: p divides p*l;
p|^n divides (p*x - q) by A2,A5,INT_1:62;
then p|^n divides (-1)*(p*x - q) by INT_2:2;
then consider k being Integer such that
A7: (p*l + q) = (p|^n) * k;
k>=0 by A2,A7,XREAL_1:132;
then k in NAT by INT_1:3;
then reconsider k as Nat;
(p*l + q) = (p|^n) * k by A7;
then
A8: p|^n divides (p*l + q);
p divides p|^n by A1,NAT_3:3;
then
A9: p divides (p*l + q) by A8,NAT_D:4;
reconsider p,q as Element of NAT by ORDINAL1:def 12;
p gcd q > 1 by A4,A9,A6,NAT_D:10,NEWTON:49;
hence contradiction by A3,INT_2:def 3;
end;
end;
begin
definition
let m be Integer;
func Cong(m) -> Relation of INT means
:Def1:
[x,y] in it iff x,y are_congruent_mod m;
existence
proof
defpred Z[Element of INT,Element of INT] means $1,$2 are_congruent_mod m;
consider R being Relation of INT,INT such that
A1: for x being Element of INT, y being Element of INT holds [x,y] in
R iff Z[x,y] from RELSET_1:sch 2;
take R;
let x,y;
for x,y being Integer holds [x,y] in R iff x,y are_congruent_mod m
proof
let x,y be Integer;
reconsider x,y as Element of INT by INT_1:def 2;
[x,y] in R iff Z[x,y] by A1;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
let P1,P2 be Relation of INT such that
A2: [x,y] in P1 iff x,y are_congruent_mod m and
A3: [x,y] in P2 iff x,y are_congruent_mod m;
A4: for x,y holds [x,y] in P1 iff [x,y] in P2
by A2,A3;
thus P1 c= P2
proof
let a be object;
assume
A5: a in P1;
then consider x,y being object such that
A6: a = [x,y] and
A7: x in INT & y in INT by RELSET_1:2;
reconsider x,y as Integer by A7;
[x,y] in P2 by A4,A5,A6;
hence thesis by A6;
end;
let a be object;
assume
A8: a in P2;
then consider x,y being object such that
A9: a = [x,y] and
A10: x in INT & y in INT by RELSET_1:2;
reconsider x,y as Integer by A10;
[x,y] in P1 by A4,A8,A9;
hence thesis by A9;
end;
end;
registration
let m be Integer;
cluster Cong m -> total;
coherence
proof
thus dom Cong(m) c= INT;
thus INT c= dom Cong(m)
proof
let x be object;
assume x in INT;
then reconsider x as Integer;
x,x are_congruent_mod m by INT_1:11;
then [x,x] in Cong(m) by Def1;
hence thesis by XTUPLE_0:def 12;
end;
end;
end;
Lm8: Cong(m) is Equivalence_Relation of INT
proof
A1: Cong(m) is_symmetric_in INT
proof
let x,y be object;
assume that
A2: x in INT and
A3: y in INT and
A4: [x,y] in Cong(m);
reconsider y as Integer by A3;
reconsider x as Integer by A2;
x,y are_congruent_mod m by A4,Def1;
then y,x are_congruent_mod m by INT_1:14;
hence thesis by Def1;
end;
A5: Cong(m) is_transitive_in INT
proof
let x,y,z be object;
assume that
A6: x in INT & y in INT & z in INT and
A7: [x,y] in Cong(m) & [y,z] in Cong(m);
reconsider x, y, z as Integer by A6;
x,y are_congruent_mod m & y,z are_congruent_mod m by A7,Def1;
then x,z are_congruent_mod m by INT_1:15;
hence thesis by Def1;
end;
field Cong(m) = INT by ORDERS_1:12;
hence thesis by A1,A5,RELAT_2:def 11,def 16;
end;
registration
let m be Integer;
cluster Cong m -> reflexive symmetric transitive;
coherence by Lm8;
end;
theorem Th26:
m<>0 & (a*x-b) mod m = 0 implies for y being Integer holds (a,m
are_coprime & (a*y-b) mod m = 0 implies y in Class(Cong m,x)) & (y in
Class(Cong m,x) implies (a*y-b) mod m = 0)
proof
assume that
A1: m<>0 and
A2: (a*x-b) mod m = 0;
let y be Integer;
hereby
assume that
A3: a,m are_coprime and
A4: (a*y-b) mod m = 0;
a*x-b,a*y-b are_congruent_mod m by A1,A2,A4,NAT_D:64;
then (a*x-b)+b,a*y are_congruent_mod m;
then x,y are_congruent_mod m by A3,Th9;
then [x,y] in Cong(m) by Def1;
hence y in Class(Cong(m),x) by EQREL_1:18;
end;
assume y in Class(Cong m,x);
then [x,y] in Cong(m) by EQREL_1:18;
then x,y are_congruent_mod m by Def1;
then
A5: x*a,y*a are_congruent_mod m by Th11;
(a*x-b) mod m = 0 mod m by A2,Th12;
then 0,a*x-b are_congruent_mod m by A1,NAT_D:64;
then 0+b,a*x are_congruent_mod m;
then 0+b,a*y are_congruent_mod m by A5,INT_1:15;
then 0,a*y-b are_congruent_mod m;
then (a*y-b) mod m = 0 mod m by NAT_D:64;
hence thesis by Th12;
end;
theorem
for a,b,m,x being Integer holds m<>0 & a,m are_coprime & (a*x-b
) mod m = 0 implies ex s being Integer st [x,b*s] in Cong m
proof
let a,b,m,x;
assume that
A1: m<>0 and
A2: a,m are_coprime and
A3: (a*x-b) mod m = 0;
a gcd m = 1 by A2,INT_2:def 3;
then consider r,t being Integer such that
A4: 1=r*a+t*m by NAT_D:68;
(a*x-b) mod m = 0 mod m by A3,Th12;
then a*x-b,0 are_congruent_mod m by A1,NAT_D:64;
then (a*x-b)*r,0 * r are_congruent_mod m by Th11;
then x*(a*r)-b*r,0 are_congruent_mod m;
then
A5: x*(1-t*m)-b*r,0 are_congruent_mod m by A4;
take s=r;
(x-x*t*m-b*r) mod m = ((x-b*r)+((-x)*t)*m) mod m .= (x-b*r) mod m by NAT_D:61
;
then (x-b*r) mod m = 0 mod m by A5,NAT_D:64;
then 0,x-b*r are_congruent_mod m by A1,NAT_D:64;
then 0+b*r,x are_congruent_mod m;
then x,b*s are_congruent_mod m by INT_1:14;
hence thesis by Def1;
end;
theorem
for a,m being Element of NAT st a<>0 & m>1 & a,m are_coprime
for b,x being Integer holds (a*x-b) mod m = 0 implies [x, b*(a|^(Euler m -'1))]
in Cong m
proof
let a,m be Element of NAT;
assume that
A1: a <> 0 and
A2: m > 1 and
A3: a,m are_coprime;
let b,x be Integer;
(a|^Euler m) mod m = 1 by A1,A2,A3,EULER_2:18;
then (a|^Euler m) = m * ((a|^Euler m) div m) + 1 by A2,NAT_D:2;
then m divides ((a|^Euler m)-1);
then (a|^Euler m),1 are_congruent_mod m;
then
A4: (a|^Euler m)*x,1*x are_congruent_mod m by Th11;
Euler m <> 0
proof
set X = {k where k is Element of NAT:m,k are_coprime & k >= 1 & k
<= m};
1 gcd m = 1 by NEWTON:51;
then m,1 are_coprime by INT_2:def 3;
then
A5: 1 in X by A2;
assume Euler m = 0;
hence contradiction by A5;
end;
then
A6: Euler m -'1+1 = Euler m-1+1 by NAT_1:14,XREAL_1:233
.= Euler m;
assume (a*x-b) mod m = 0;
then m divides ((a*x-b)-0) by A2,INT_1:62;
then a*x-b,0 are_congruent_mod m;
then 0,a*x-b are_congruent_mod m by INT_1:14;
then (a|^(Euler m -'1))*(0 qua Nat), (a|^(Euler m -'1))*(a*x-b)
are_congruent_mod m by Th11;
then 0,(a|^(Euler m -'1))*a*x-(a|^(Euler m -'1))*b are_congruent_mod m;
then 0,(a|^(Euler m -'1+1))*x-(a|^(Euler m -'1))*b are_congruent_mod m by
NEWTON:6;
then 0+(a|^(Euler m -'1))*b,(a|^Euler m)*x are_congruent_mod m by A6;
then (a|^(Euler m -'1))*b,x are_congruent_mod m by A4,INT_1:15;
then x, b*(a|^(Euler m -'1)) are_congruent_mod m by INT_1:14;
hence thesis by Def1;
end;
theorem :: Theorem 6.1, from Chapter 2 of Hua Loo Keng
m<>0 & (a gcd m) divides b implies ex fp being FinSequence of INT st
len fp = a gcd m & (for c st c in dom fp holds (a*(fp.c)-b) mod m = 0) & for c1
,c2 st c1 in dom fp & c2 in dom fp & c1<>c2 holds not fp.c1,fp.c2
are_congruent_mod m
proof
assume that
A1: m<>0 and
A2: (a gcd m) divides b;
set l = a gcd m;
reconsider l as Element of NAT by ORDINAL1:def 12;
consider a1,m1 being Integer such that
A3: a = l*a1 and
A4: m = l*m1 and
A5: a1,m1 are_coprime by A1,INT_2:23;
consider b1 being Integer such that
A6: b=l*b1 by A2;
consider x1 being Integer such that
A7: (a1 * x1 - b1) mod m1 = 0 by A5,Th15;
deffunc P(Nat) = x1+($1-1)*m1;
consider fp being FinSequence such that
A8: len fp = l & for c being Nat st c in dom fp holds fp.c = P(c) from
FINSEQ_1:sch 2;
for c being Nat st c in dom fp holds fp.c in INT
proof
let c be Nat;
assume c in dom fp;
then fp.c = x1+(c-1)*m1 by A8;
hence thesis by INT_1:def 2;
end;
then reconsider fp as FinSequence of INT by FINSEQ_2:12;
A9: m1 <> 0 by A1,A4;
A10: for c1,c2 st c1 in dom fp & c2 in dom fp & c1<>c2 holds not fp.c1,fp.c2
are_congruent_mod m
proof
let c1,c2;
assume that
A11: c1 in dom fp and
A12: c2 in dom fp and
A13: c1<>c2;
assume
A14: fp.c1,fp.c2 are_congruent_mod m;
fp.c1 = x1+(c1-1)*m1 & fp.c2 = x1+(c2-1)*m1 by A8,A11,A12;
then m divides (((c1-1)*m1+x1)-((c2-1)*m1+x1)) by A14;
then consider w being Integer such that
A15: (c1-c2)*m1 = l*m1*w by A4;
(c1-c2)*m1 = (l*w)*m1 by A15;
then (c1-c2) = l*w by A9,XCMPLX_1:5;
then
A16: l divides (c1-c2);
A17: c2 in Seg l by A8,A12,FINSEQ_1:def 3;
then
A18: c2>=1 by FINSEQ_1:1;
A19: c1 in Seg l by A8,A11,FINSEQ_1:def 3;
then c1<=l by FINSEQ_1:1;
then c1-c2 <= l-1 by A18,XREAL_1:13;
then
A20: c1-c2 < l by XREAL_1:147;
A21: c2<=l by A17,FINSEQ_1:1;
c1>=1 by A19,FINSEQ_1:1;
then c1-c2 >= 1-l by A21,XREAL_1:13;
then c1-c2 > -l by XREAL_1:145;
then
A22: |.c1-c2.| < l by A20,SEQ_2:1;
c1-c2<>0 by A13;
then |.l.| <= |.c1-c2.| by A16,Th6;
hence contradiction by A22,ABSVALUE:def 1;
end;
take fp;
(a1 * x1 - b1) mod m1 = 0 mod m1 by A7,Th12;
then (a1 * x1 - b1),0 are_congruent_mod m1 by A9,NAT_D:64;
then (a1 * x1 - b1)*l,0*l are_congruent_mod m1*l by Th10;
then
A23: (a*x1 - b) mod m = 0 mod m by A3,A4,A6,NAT_D:64;
for c st c in dom fp holds (a*(fp.c)-b) mod m = 0
proof
let c;
assume c in dom fp;
hence (a*(fp.c)-b) mod m = (a*(x1+(c-1)*m1)-b) mod m by A8
.= ((a*x1-b)+a1*(c-1)*m) mod m by A3,A4
.= (a*x1 - b) mod m by NAT_D:61
.= 0 by A23,Th12;
end;
hence thesis by A8,A10;
end;
begin
reserve fp,fp1 for FinSequence of NAT,
b,c,d, n for Element of NAT,
a for Nat;
theorem Th30:
for b,n st b in dom fp & len fp = n+1 holds Del(fp^<*d*>,b) = Del(fp,b)^<*d*>
proof
let b,n such that
A1: b in dom fp and
A2: len fp = n+1;
A3: len Del(fp,b) = n by A1,A2,FINSEQ_3:109;
then
A4: len (Del(fp,b)^<*d*>) = n+1 by FINSEQ_2:16;
A5: len (fp^<*d*>) = (n+1)+1 & b in dom (fp^<*d*>) by A1,A2,FINSEQ_2:16
,FINSEQ_3:22;
then
A6: len Del(fp^<*d*>,b) = len (Del(fp,b)^<*d*>) by A4,FINSEQ_3:109;
for k be Nat st 1 <= k & k <= len Del(fp^<*d*>,b) holds Del(fp^<*d*>,b).
k=(Del(fp,b)^<*d*>).k
proof
let k be Nat such that
A7: 1 <=k and
A8: k <= len Del(fp^<*d*>,b);
A9: k in dom fp by A2,A4,A6,A7,A8,FINSEQ_3:25;
per cases;
suppose
A10: k<b;
b <= n+1 by A1,A2,FINSEQ_3:25;
then k < n+1 by A10,XXREAL_0:2;
then k <= n by NAT_1:13;
then k in dom Del(fp,b) by A3,A7,FINSEQ_3:25;
then
A11: (Del(fp,b)^<*d*>).k = Del(fp,b).k by FINSEQ_1:def 7
.= fp.k by A10,FINSEQ_3:110;
set fpd = fp^<*d*>;
Del(fpd,b).k = fpd.k by A10,FINSEQ_3:110
.= fp.k by A9,FINSEQ_1:def 7;
hence thesis by A11;
end;
suppose
A12: b<=k;
then
A13: Del(fp^<*d*>,b).k = (fp^<*d*>).(k+1) by A4,A5,A6,A8,FINSEQ_3:111;
per cases by A4,A6,A8,NAT_1:8;
suppose
A14: k<=n;
then k in dom Del(fp,b) by A3,A7,FINSEQ_3:25;
then
A15: (Del(fp,b)^<*d*>).k = Del(fp,b).k by FINSEQ_1:def 7
.= fp.(k+1) by A1,A2,A12,A14,FINSEQ_3:111;
A16: k+1 >= 1 by NAT_1:11;
k+1 <= n+1 by A14,XREAL_1:6;
then (k+1) in dom fp by A2,A16,FINSEQ_3:25;
hence thesis by A13,A15,FINSEQ_1:def 7;
end;
suppose
A17: k=n+1;
then Del(fp^<*d*>,b).k = d by A2,A13,FINSEQ_1:42;
hence thesis by A3,A17,FINSEQ_1:42;
end;
end;
end;
hence thesis by A4,A5,FINSEQ_3:109;
end;
theorem Th31:
len fp>=2 & (for b,c st b in dom fp & c in dom fp & b<>c holds (
fp.b gcd fp.c)=1) implies for b st b in dom fp holds (Product Del(fp,b)) gcd (
fp.b) = 1
proof
defpred CC[FinSequence of NAT] means for b st b in dom $1 holds Product Del(
$1,b) gcd $1.b = 1;
defpred RP[FinSequence of NAT] means for b,c st b in dom $1 & c in dom $1 &
b<>c holds ($1.b gcd $1.c)=1;
defpred TH[set] means ex f being FinSequence of NAT st f = $1 &
(len f>=2 & RP[f] implies CC[f]);
A1: now
let fp,d such that
A2: TH[fp];
set k=len fp;
set fp1=fp^<*d*>;
now
assume that
A3: len fp1>=2 and
A4: RP[fp1];
A5: len fp1 = k+1 by FINSEQ_2:16;
now
per cases by A3,XXREAL_0:1;
suppose
A6: len fp1 = 2;
then 1 in dom fp1 & 2 in dom fp1 by FINSEQ_3:25;
then
A7: fp1.2 gcd fp1.1 = 1 by A4;
A8: fp1=<*fp1.1,fp1.2*> by A6,FINSEQ_1:44;
for b st b in dom fp1 holds Product Del(fp1,b) gcd fp1.b = 1
proof
let b;
assume b in dom fp1;
then
A9: b in Seg len fp1 by FINSEQ_1:def 3;
per cases by A6,A9,FINSEQ_1:2,TARSKI:def 2;
suppose
b=1;
hence Product Del(fp1,b) gcd fp1.b = Product <*fp1.2*> gcd fp1.1
by A8,WSIERP_1:19
.= 1 by A7,RVSUM_1:95;
end;
suppose
b=2;
hence Product Del(fp1,b) gcd fp1.b = Product <*fp1.1*> gcd fp1.2
by A8,WSIERP_1:19
.= 1 by A7,RVSUM_1:95;
end;
end;
hence CC[fp1];
end;
suppose
len fp1 > 2;
then
A10: k+1 > 1+1 by FINSEQ_2:16;
then k >= 1+1 by NAT_1:13;
then consider n being Nat such that
A11: k=n+1 by NAT_1:6;
A12: RP[fp]
proof
A13: dom fp c= dom fp1 by FINSEQ_1:26;
let b,c such that
A14: b in dom fp & c in dom fp and
A15: b<>c;
fp1.b=fp.b & (fp1.c)=fp.c by A14,FINSEQ_1:def 7;
hence thesis by A4,A14,A15,A13;
end;
A16: a in dom fp implies fp.a gcd d=1
proof
A17: (len fp+1) in dom fp1 by A5,FINSEQ_5:6;
A18: dom fp c= dom fp1 & fp1.(len fp+1)=d by FINSEQ_1:26,42;
assume
A19: a in dom fp;
len fp+1>len fp by NAT_1:13;
then
A20: len fp+1 <> a by A19,FINSEQ_3:25;
fp1.a=fp.a by A19,FINSEQ_1:def 7;
hence thesis by A4,A19,A18,A20,A17;
end;
reconsider n as Element of NAT by ORDINAL1:def 12;
A21: k=n+1 by A11;
for b st b in dom fp1 holds Product Del(fp1,b) gcd fp1.b = 1
proof
let b such that
A22: b in dom fp1;
A23: b>=1 by A22,FINSEQ_3:25;
A24: b<=k+1 by A5,A22,FINSEQ_3:25;
per cases by A24,NAT_1:8;
suppose
b<=k;
then
A25: b in dom fp by A23,FINSEQ_3:25;
then
Product Del(fp,b) gcd fp.b = 1 & fp.b gcd d=1 by A2,A10,A12,A16,
NAT_1:13;
then (Product Del(fp,b))*d gcd fp.b = 1 by WSIERP_1:7;
then
A26: (Product (Del(fp,b)^<*d*>)) gcd fp.b = 1 by RVSUM_1:96;
Del(fp1,b) = Del(fp,b)^<*d*> by A21,A25,Th30;
hence thesis by A25,A26,FINSEQ_1:def 7;
end;
suppose
b=k+1;
hence Product Del(fp1,b) gcd fp1.b = Product Del(fp1,k+1) gcd d
by FINSEQ_1:42
.= Product(fp) gcd d by WSIERP_1:40
.= 1 by A16,WSIERP_1:36;
end;
end;
hence CC[fp1];
end;
end;
hence CC[fp1];
end;
hence TH[fp1];
end;
A27: TH[<*>NAT]
proof
take <*>NAT;
thus thesis;
end;
for fp holds TH[fp] from FINSEQ_2:sch 2(A27,A1);
then ex f being FinSequence of NAT st f = fp &
(len f>=2 & RP[f] implies CC[f]);
hence thesis;
end;
theorem Th32:
for a st a in dom fp holds fp.a divides Product fp
proof
let a;
assume a in dom fp;
then fp.a in rng fp by FUNCT_1:3;
hence thesis by NAT_3:7;
end;
theorem
a in dom fp & p divides fp.a implies p divides Product fp
proof
assume that
A1: a in dom fp and
A2: p divides fp.a;
fp.a divides Product fp by A1,Th32;
hence thesis by A2,NAT_D:4;
end;
theorem
len fp = n+1 & a >= 1 & a <= n implies Del(fp,a).n = fp.(len fp)
proof
assume that
A1: len fp = n+1 and
A2: a >= 1 and
A3: a <= n;
n<n+1 by XREAL_1:29;
then a<n+1 by A3,XXREAL_0:2;
then a in dom fp by A1,A2,FINSEQ_3:25;
hence thesis by A1,A3,WSIERP_1:def 1;
end;
theorem Th35:
for a,b st a in dom fp & b in dom fp & a<>b & len fp >= 1 holds
fp.b divides Product Del (fp,a)
proof
let a,b;
assume that
A1: a in dom fp and
A2: b in dom fp and
A3: a<>b and
A4: len fp >= 1;
consider n being Nat such that
A5: len fp = n+1 by A4,NAT_1:6;
A6: a<=n+1 by A1,A5,FINSEQ_3:25;
A7: a>=1 by A1,FINSEQ_3:25;
A8: b>=1 by A2,FINSEQ_3:25;
A9: len Del (fp,a) + 1 = n + 1 by A1,A5,WSIERP_1:def 1;
A10: b<=n+1 by A2,A5,FINSEQ_3:25;
per cases by A6,NAT_1:8;
suppose
A11: a<=n;
per cases by A3,XXREAL_0:1;
suppose
A12: b<a;
then b<=n by A11,XXREAL_0:2;
then
A13: b in dom Del (fp,a) by A8,A9,FINSEQ_3:25;
Del (fp,a).b = fp.b by A1,A12,WSIERP_1:def 1;
hence thesis by A13,Th32;
end;
suppose
A14: a<b;
then b>=a+1 by NAT_1:13;
then b-1>=a by XREAL_1:19;
then b-'1>=a by A8,XREAL_1:233;
then
A15: Del (fp,a).(b-'1) = fp.((b-'1)+1) by A1,WSIERP_1:def 1;
b>1 by A7,A14,XXREAL_0:2;
then b-1>0 by XREAL_1:50;
then b-'1>0 by A8,XREAL_1:233;
then
A16: b-'1>=1 by Lm7;
b-1<=(n+1)-1 by A10,XREAL_1:9;
then b-'1<=n by A8,XREAL_1:233;
then b-'1 in dom Del (fp,a) by A9,A16,FINSEQ_3:25;
then Del (fp,a).(b-'1) divides Product Del (fp,a) by Th32;
hence thesis by A8,A15,XREAL_1:235;
end;
end;
suppose
A17: a=n+1;
then b<n+1 by A3,A10,XXREAL_0:1;
then b<=n by NAT_1:13;
then
A18: b in dom Del (fp,a) by A8,A9,FINSEQ_3:25;
b<a by A3,A10,A17,XXREAL_0:1;
then Del (fp,a).b = fp.b by A1,WSIERP_1:def 1;
hence thesis by A18,Th32;
end;
end;
Lm9: for i1,i2 being Integer for n being Nat st n > 0 & i1 mod n = 0 holds i1*
i2 mod n = 0
proof
let i1,i2 be Integer,n be Nat;
assume that
A1: n > 0 and
A2: i1 mod n = 0;
n divides i1 by A1,A2,INT_1:62;
then n divides i1*i2 by INT_2:2;
hence thesis;
end;
theorem Th36:
(for b being Nat st b in dom fp holds a divides fp.b) implies a
divides Sum fp
proof
defpred RP[FinSequence of NAT] means for b being Nat st b in dom $1 holds a
divides $1.b;
defpred CC[FinSequence of NAT] means a divides Sum $1;
defpred TH[set] means ex f being FinSequence of NAT st f = $1 &
(RP[f] implies CC[f]);
A1: now
let fp,d such that
A2: TH[fp];
set fp1=fp^<*d*>;
now
assume
A3: RP[fp1];
A4: RP[fp]
proof
let b be Nat such that
A5: b in dom fp;
dom fp c= dom fp1 & fp1.b = fp.b by A5,FINSEQ_1:26,def 7;
hence thesis by A3,A5;
end;
len fp1 in dom fp1 by FINSEQ_5:6;
then a divides fp1.(len fp1) by A3;
then a divides fp1.(len fp + 1) by FINSEQ_2:16;
then a divides d by FINSEQ_1:42;
then a divides (Sum fp + d ) by A2,A4,NAT_D:8;
hence CC[fp1] by RVSUM_1:74;
end;
hence TH[fp1];
end;
A6: TH[<*>NAT] by NAT_D:6,RVSUM_1:72;
for fp holds TH[fp] from FINSEQ_2:sch 2(A6,A1);
then ex f being FinSequence of NAT st f = fp & (RP[f] implies CC[f]);
hence thesis;
end;
theorem
len fp>=2 & (for b,c st b in dom fp & c in dom fp & b<>c holds (fp.b
gcd fp.c)=1) & (for b st b in dom fp holds fp.b <> 0) implies
for fp1 ex x being Integer st
for b st b in dom fp holds (x-fp1.b) mod fp.b = 0
proof
assume that
A1: len fp>=2 and
A2: for b,c st b in dom fp & c in dom fp & b<>c holds (fp.b gcd fp.c)=1 and
A3: for b st b in dom fp holds fp.b <> 0;
consider fp2 being FinSequence of NAT,q being Element of NAT such that
A4: fp=fp2^<*q*> by A1,FINSEQ_2:19;
deffunc F(Nat) = {l where l is Element of NAT: ((Product Del(fp,$1))*l - 1)
mod fp.$1 = 0};
defpred FF[Nat,Nat] means $2 in F($1);
A5: for a be Nat st a in Seg len fp ex n being Element of NAT st FF[a,n]
proof
let a be Nat;
reconsider l=fp.a as Integer;
assume a in Seg len fp;
then
A6: a in dom fp by FINSEQ_1:def 3;
then Product Del(fp,a) gcd fp.a = 1 by A1,A2,Th31;
then
A7: Product Del(fp,a),l are_coprime by INT_2:def 3;
l <> 0 by A3,A6;
then consider n being Nat such that
A8: ((Product Del(fp,a))*n-1) mod l = 0 by A7,Th16;
reconsider n as Element of NAT by ORDINAL1:def 12;
take n;
thus thesis by A8;
end;
consider s being FinSequence of NAT such that
A9: dom s = Seg len fp & for a be Nat st a in Seg len fp holds FF[a,s.a
] from FINSEQ_1:sch 5(A5);
let fp1;
set k=len fp2;
deffunc P(Nat) = Product Del(fp,$1)*(s.$1)*(fp1.$1);
consider s1 being FinSequence such that
A10: len s1=k+1 & for a be Nat st a in dom s1 holds s1.a=P(a) from
FINSEQ_1:sch 2;
for a being Nat st a in dom s1 holds s1.a in NAT
proof
let a be Nat;
assume
A11: a in dom s1;
reconsider a as Element of NAT by ORDINAL1:def 12;
s1.a = Product Del(fp,a)*(s.a)*(fp1.a) by A10,A11;
hence thesis by ORDINAL1:def 12;
end;
then reconsider s1 as FinSequence of NAT by FINSEQ_2:12;
set x = Sum s1;
take x;
A12: len fp = k + 1 by A4,FINSEQ_2:16;
A13: for a,b st a in dom fp & b in dom fp & a<>b holds fp.b divides s1.a
proof
let a,b;
assume that
A14: a in dom fp and
A15: b in dom fp & a<>b;
len fp >= 1 by A1,XXREAL_0:2;
then fp.b divides Product Del(fp,a)*((s.a)*(fp1.a)) by A14,A15,Th35,NAT_D:9
;
then
A16: fp.b divides Product Del(fp,a)*(s.a)*(fp1.a);
a in dom s1 by A12,A10,A14,FINSEQ_3:29;
hence thesis by A10,A16;
end;
A17: for b st b in dom fp holds fp.b divides Sum Del (s1,b)
proof
let b;
assume
A18: b in dom fp;
then b in Seg len s1 by A12,A10,FINSEQ_1:def 3;
then
A19: b in dom s1 by FINSEQ_1:def 3;
then
A20: len Del (s1,b) + 1 = k + 1 by A10,WSIERP_1:def 1;
for a st a in dom Del (s1,b) holds fp.b divides Del (s1,b).a
proof
let a;
assume
A21: a in dom Del (s1,b);
then
A22: a>=1 & a<=k by A20,FINSEQ_3:25;
dom Del (s1,b) c= dom s1 by WSIERP_1:39;
then a in dom s1 by A21;
then a in Seg (k+1) by A10,FINSEQ_1:def 3;
then
A23: a in dom fp by A12,FINSEQ_1:def 3;
per cases;
suppose
A24: a<b;
then Del (s1,b).a = s1.a by A19,WSIERP_1:def 1;
hence thesis by A13,A18,A23,A24;
end;
suppose
A25: a>=b;
a+1<=k+1 & a+1>1 by A22,XREAL_1:6,29;
then
A26: a+1 in dom fp by A12,FINSEQ_3:25;
Del (s1,b).a=s1.(a+1) & a+1>b by A19,A25,WSIERP_1:def 1,XREAL_1:39;
hence thesis by A13,A18,A26;
end;
end;
hence thesis by Th36;
end;
for b st b in dom fp holds (x-fp1.b) mod fp.b = 0
proof
let b;
assume
A27: b in dom fp;
then
A28: fp.b <>0 by A3;
A29: fp.b divides Sum Del (s1,b) by A17,A27;
A30: (Sum Del (s1,b)+((s1.b)-fp1.b)) mod fp.b = (s1.b - fp1.b) mod fp.b
proof
reconsider l = Sum Del (s1,b) as Integer;
A31: l mod fp.b = 0 by A29;
(Sum Del (s1,b)+((s1.b)-fp1.b)) mod fp.b = ((l mod fp.b) + (((s1.b)
-fp1.b) mod fp.b)) mod fp.b by NAT_D:66
.= ((s1.b)-fp1.b) mod fp.b by A31,NAT_D:65;
hence thesis;
end;
A32: b>=1 & b<=k+1 by A12,A27,FINSEQ_3:25;
then
A33: b in Seg (k+1);
then b in dom s1 by A10,FINSEQ_1:def 3;
then
A34: s1.b - fp1.b = Product Del(fp,b)*(s.b)*(fp1.b) - 1*fp1.b by A10
.= (Product Del(fp,b)*(s.b) - 1)*fp1.b;
s.b in F(b) by A12,A9,A33;
then
A35: ex ll being Element of NAT st ll = s.b & ((Product Del(fp,b))*ll-1)
mod fp.b = 0;
A36: s1 is FinSequence of REAL by FINSEQ_2:24,NUMBERS:19;
b in dom s1 by A10,A32,FINSEQ_3:25;
then (x-fp1.b) mod fp.b = (Sum Del (s1,b)+(s1.b)-fp1.b) mod fp.b by
WSIERP_1:20,A36
.= 0 by A28,A34,A35,A30,Lm9;
hence thesis;
end;
hence thesis;
end;
theorem Th38:
(for b,c st b in dom fp & c in dom fp & b<>c holds (fp.b gcd fp.
c)=1) & (for b st b in dom fp holds fp.b divides a) implies Product fp divides
a
proof
defpred RP[FinSequence of NAT] means (for b,c st b in dom $1 & c in dom $1 &
b<>c holds ($1.b gcd $1.c)=1) & (for b st b in dom $1 holds $1.b divides a);
defpred CC[FinSequence of NAT] means Product $1 divides a;
defpred TH[set] means ex f being FinSequence of NAT st f = $1 &
(RP[f] implies CC[f]);
A1: now
let fp,d such that
A2: TH[fp];
set fp1=fp^<*d*>;
len fp + 1 >= 0 + 1 by XREAL_1:6;
then
A3: len fp1 >= 1 by FINSEQ_2:16;
now
assume
A4: RP[fp1];
for a st a in dom fp holds fp.a gcd d=1
proof
let a;
A5: len fp1 in dom fp1 by A3,FINSEQ_3:25;
assume
A6: a in dom fp;
then a <= len fp by FINSEQ_3:25;
then a < len fp + 1 by XREAL_1:39;
then
A7: a < len fp1 by FINSEQ_2:16;
a in dom fp1 by A6,FINSEQ_2:15;
then fp1.a gcd fp1.(len fp1)=1 by A4,A7,A5;
then
A8: fp1.a gcd fp1.(len fp + 1)=1 by FINSEQ_2:16;
fp1.a = fp.a by A6,FINSEQ_1:def 7;
hence thesis by A8,FINSEQ_1:42;
end;
then Product(fp) gcd d = 1 by WSIERP_1:36;
then
A9: Product(fp),d are_coprime by INT_2:def 3;
A10: dom fp c= dom fp1 by FINSEQ_1:26;
A11: for b,c st b in dom fp & c in dom fp & b<>c holds (fp.b gcd fp.c)=1
proof
let b,c;
assume that
A12: b in dom fp & c in dom fp and
A13: b<>c;
fp1.b = fp.b & fp1.c = fp.c by A12,FINSEQ_1:def 7;
hence thesis by A4,A10,A12,A13;
end;
A14: for b st b in dom fp holds fp.b divides a
proof
let b;
assume
A15: b in dom fp;
then fp1.b = fp.b by FINSEQ_1:def 7;
hence thesis by A4,A10,A15;
end;
len fp1 in dom fp1 by FINSEQ_5:6;
then fp1.(len fp1) divides a by A4;
then fp1.(len fp + 1) divides a by FINSEQ_2:16;
then d divides a by FINSEQ_1:42;
then (Product(fp) * d) divides a by A2,A11,A14,A9,PEPIN:4;
hence CC[fp1] by RVSUM_1:96;
end;
hence TH[fp1];
end;
A16: TH[<*>NAT]
proof
take <*>NAT;
thus thesis by NAT_D:6,RVSUM_1:94;
end;
for fp holds TH[fp] from FINSEQ_2:sch 2(A16,A1);
then ex f being FinSequence of NAT st f = fp & (RP[f] implies CC[f]);
hence thesis;
end;
theorem
(for b,c st b in dom fp & c in dom fp & b<>c holds (fp.b gcd fp.c)=1)
& (for b st b in dom fp holds fp.b > 0) implies for fp1 st (for b st b in dom
fp holds (x-fp1.b) mod fp.b = 0 & (y-fp1.b) mod fp.b = 0) holds x,y
are_congruent_mod Product(fp)
proof
assume that
A1: for b,c st b in dom fp & c in dom fp & b<>c holds (fp.b gcd fp.c)=1 and
A2: for b st b in dom fp holds fp.b > 0;
let fp1 such that
A3: for b st b in dom fp holds (x-fp1.b) mod fp.b = 0 & (y-fp1.b) mod fp
.b = 0;
per cases;
suppose
x>=y;
then (x-y) in NAT by INT_1:3,XREAL_1:48;
then reconsider k=(x-y) as Nat;
for b st b in dom fp holds fp.b divides k
proof
let b such that
A4: b in dom fp;
A5: fp.b > 0 by A2,A4;
(y-fp1.b) mod fp.b = 0 by A3,A4;
then
A6: fp.b divides (y-fp1.b) by A5,INT_1:62;
(x-fp1.b) mod fp.b = 0 by A3,A4;
then fp.b divides (x-fp1.b) by A5,INT_1:62;
then fp.b divides ((x-fp1.b)-(y-fp1.b)) by A6,Lm4;
then consider i being Integer such that
A7: x-y=(fp.b)*i;
i>=0
proof
assume i<0;
then k<0 by A2,A4,A7,XREAL_1:132;
hence contradiction;
end;
then i in NAT by INT_1:3;
then reconsider i as Nat;
thus thesis by A7;
end;
then Product fp divides k by A1,Th38;
hence thesis;
end;
suppose
x<y;
then y-x>0 by XREAL_1:50;
then (y-x) in NAT by INT_1:3;
then reconsider k=y-x as Nat;
for b st b in dom fp holds fp.b divides k
proof
let b such that
A8: b in dom fp;
A9: fp.b > 0 by A2,A8;
(y-fp1.b) mod fp.b = 0 by A3,A8;
then
A10: fp.b divides (y-fp1.b) by A9,INT_1:62;
(x-fp1.b) mod fp.b = 0 by A3,A8;
then fp.b divides (x-fp1.b) by A9,INT_1:62;
then fp.b divides ((y-fp1.b)-(x-fp1.b)) by A10,Lm4;
then consider i being Integer such that
A11: y-x=(fp.b)*i;
k=(fp.b)*i by A11;
then i>=0 by A2,A8,XREAL_1:132;
then i in NAT by INT_1:3;
then reconsider i as Nat;
thus thesis by A11;
end;
then Product fp divides k by A1,Th38;
then y,x are_congruent_mod Product fp;
hence thesis by INT_1:14;
end;
end;
reserve i,m,m1,m2,m3,r,s,a,b,c,c1,c2,x,y for Integer;
Lm10: ( x divides y implies y mod x = 0) & (x<>0 & y mod x = 0 implies x
divides y)
proof
A1: x divides y implies y mod x = 0
proof
assume x divides y;
then consider i such that
A2: y = x * i;
y mod x = (x * i + 0) mod x by A2
.= 0 mod x by NAT_D:61
.= 0 by Th12;
hence thesis;
end;
x<>0 & y mod x = 0 implies x divides y
proof
assume that
A3: x<>0 and
A4: y mod x = 0;
y = (y div x) * x + (y mod x) by A3,INT_1:59
.= (y div x) * x by A4;
hence thesis;
end;
hence thesis;
end;
Lm11: x divides y implies y = (y div x) * x
proof
assume
A1: x divides y;
then
A2: y mod x = 0;
per cases;
suppose
x = 0;
hence thesis by A1;
end;
suppose
x <> 0;
hence y = (y div x) * x + (y mod x) by INT_1:59
.= (y div x) * x by A2;
end;
end;
Lm12: (x<>0 or y<>0) implies x div (x gcd y),y div (x gcd y) are_coprime
proof
assume
A1: x<>0 or y<>0;
then
A2: x gcd y <> 0 by INT_2:5;
A3: y=(y div (x gcd y))*(x gcd y) by Lm11,INT_2:21;
consider a,b being Integer such that
A4: x = (x gcd y)*a and
A5: y = (x gcd y)*b & a,b are_coprime by A1,INT_2:23;
x=(x div (x gcd y))*(x gcd y) by Lm11,INT_2:21;
then a = x div (x gcd y) by A2,A4,XCMPLX_1:5;
hence thesis by A2,A3,A5,XCMPLX_1:5;
end;
Lm13: x divides i & y divides i & x,y are_coprime implies (x*y) divides
i
proof
assume that
A1: x divides i and
A2: y divides i & x,y are_coprime;
consider m such that
A3: i = x * m by A1;
y divides m by A2,A3,INT_2:25;
then consider r such that
A4: m = y * r;
i = (x * y) * r by A3,A4;
hence thesis;
end;
theorem Th40:
m1<>0 & m2<>0 & m1,m2 are_coprime implies ex r being
Integer st (for x st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds x,(c1+m1*r
) are_congruent_mod (m1*m2)) & (m1*r - (c2-c1)) mod m2 = 0
proof
assume that
A1: m1<>0 and
A2: m2<>0 and
A3: m1,m2 are_coprime;
consider r being Integer such that
A4: (m1*r-(c2-c1)) mod m2 = 0 by A3,Th15;
take r;
for x st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds x,(c1+m1*r)
are_congruent_mod (m1*m2)
proof
let x;
assume that
A5: (x - c1) mod m1 = 0 and
A6: (x - c2) mod m2 = 0;
set y = (x - c1) div m1;
A7: x - c1 = ((x - c1) div m1) * m1 + ((x - c1) mod m1) by A1,INT_1:59
.= ((x - c1) div m1) * m1 by A5;
then (x - c2) mod m2 = (m1 * y - (c2 -c1)) mod m2;
then y in Class(Cong(m2),r) by A2,A3,A4,A6,Th26;
then [r,y] in Cong(m2) by EQREL_1:18;
then r,y are_congruent_mod m2 by Def1;
then y,r are_congruent_mod m2 by INT_1:14;
then m2 divides (y - r);
then consider t being Integer such that
A8: y - r = m2 * t;
x = c1 + y * m1 by A7
.= c1 + (r + m2 * t)* m1 by A8
.= (c1 + r * m1) + (m1 * m2) * t;
then (m1 * m2) divides (x - (c1 + r * m1));
hence thesis;
end;
hence thesis by A4;
end;
theorem Th41:
m1 <> 0 & m2 <> 0 & not (m1 gcd m2) divides (c1-c2) implies not
ex x st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0
proof
assume that
A1: m1 <> 0 and
A2: m2 <> 0 and
A3: not (m1 gcd m2) divides (c1-c2);
A4: (m1 gcd m2) divides m2 by INT_2:21;
given x such that
A5: (x - c1) mod m1 = 0 and
A6: (x - c2) mod m2 = 0;
m2 divides (x-c2) by A2,A6,Lm10;
then
A7: (m1 gcd m2) divides (x-c2) by A4,INT_2:9;
A8: (m1 gcd m2) divides m1 by INT_2:21;
m1 divides (x-c1) by A1,A5,Lm10;
then (m1 gcd m2) divides (x-c1) by A8,INT_2:9;
then (m1 gcd m2) divides ((x-c2)-(x-c1)) by A7,Lm4;
hence contradiction by A3;
end;
theorem Th42:
m1<>0 & m2<>0 & (m1 gcd m2) divides (c2-c1) implies ex r st (for
x st (x-c1) mod m1 = 0 & (x-c2) mod m2 = 0 holds x,(c1+m1*r) are_congruent_mod
(m1 lcm m2)) & ((m1 div (m1 gcd m2))*r - ((c2-c1) div (m1 gcd m2))) mod (m2 div
(m1 gcd m2)) = 0
proof
assume that
A1: m1<>0 and
A2: m2<>0 and
A3: (m1 gcd m2) divides (c2-c1);
set d = m1 gcd m2;
set d1 = m1 div d;
set d2 = m2 div d;
set d3 = (c2 - c1) div d;
A4: d1,d2 are_coprime by A1,Lm12;
then consider r such that
A5: (d1 * r - d3) mod d2 = 0 by Th15;
take r;
A6: m1 = (m1 div (m1 gcd m2))*(m1 gcd m2) by Lm11,INT_2:21;
A7: m2 = (m2 div (m1 gcd m2))*(m1 gcd m2) by Lm11,INT_2:21;
A8: d <> 0 by A1,INT_2:5;
for x st (x-c1) mod m1 = 0 & (x-c2) mod m2 = 0 holds x,(c1+m1*r)
are_congruent_mod (m1 lcm m2)
proof
let x;
assume that
A9: (x-c1) mod m1 = 0 and
A10: (x-c2) mod m2 = 0;
set y = (x-c1) div m1;
A11: x-c1 = ((x-c1) div m1) * m1 + ((x-c1) mod m1) by A1,INT_1:59
.= ((x-c1) div m1) * m1 by A9;
then x - (m1 * r + c1) = m1 * (((x-c1) div m1) - r);
then
A12: m1 divides (x - (m1 * r + c1));
(x-c2) mod m2 = (m1 * y -(c2 - c1)) mod m2 by A11
.= (d * d1 * y - d * d3) mod (d * d2) by A3,A6,A7,Lm11;
then (d2 * d) divides (((d1 * y) - d3) * d) by A2,A7,A10,Lm10;
then d2 divides (d1 * y - d3) by A8,Th7;
then
A13: (d1 * y - d3) mod d2 = 0;
d2 <> 0 by A2,A7;
then r in Class(Cong(d2),y) by A4,A5,A13,Th26;
then [y,r] in Cong(d2) by EQREL_1:18;
then y,r are_congruent_mod d2 by Def1;
then d2 divides (y - r);
then consider w being Integer such that
A14: y - r = d2*w;
x = c1 + y * m1 by A11
.= c1 + (d2 * w + r) * m1 by A14
.= (m1 * r + c1) + w * d1 * m2 by A6,A7;
then m2 divides (x - (m1 * r + c1));
then (m1 lcm m2) divides (x - (m1 * r + c1)) by A12,INT_2:19;
hence thesis;
end;
hence thesis by A5;
end;
theorem
m1<>0 & m2<>0 & (a gcd m1) divides c1 & (b gcd m2) divides c2 & m1,m2
are_coprime implies ex w,r,s being Integer st (for x st (a*x-c1) mod m1
= 0 & (b*x-c2) mod m2 = 0 holds x,(r + (m1 div (a gcd m1))*w) are_congruent_mod
((m1 div (a gcd m1))*(m2 div (b gcd m2)))) & ((a div (a gcd m1))*r-(c1 div (a
gcd m1))) mod (m1 div (a gcd m1)) =0 & ((b div (b gcd m2))*s-(c2 div (b gcd m2)
)) mod (m2 div (b gcd m2)) = 0 & ((m1 div (a gcd m1))*w - (s-r)) mod ((m2 div (
b gcd m2))) = 0
proof
assume that
A1: m1<>0 and
A2: m2<>0 and
A3: (a gcd m1) divides c1 and
A4: (b gcd m2) divides c2 and
A5: m1,m2 are_coprime;
set d2 = b gcd m2;
A6: d2 <> 0 by A2,INT_2:5;
set d1 = a gcd m1;
A7: d1 <> 0 by A1,INT_2:5;
A8: (a div d1),(m1 div d1) are_coprime by A1,Lm12;
then consider r such that
A9: ((a div d1)*r - (c1 div d1)) mod (m1 div d1) = 0 by Th15;
A10: c2 = (c2 div d2)*d2 by A4,Lm11;
A11: b = (b div d2)*d2 by Lm11,INT_2:21;
A12: m2 = (m2 div d2)*d2 by Lm11,INT_2:21;
then
A13: (m2 div d2) divides m2;
A14: m2 div d2 <> 0 by A2,A12;
A15: c1 = (c1 div d1)*d1 by A3,Lm11;
A16: a = (a div d1)*d1 by Lm11,INT_2:21;
A17: (b div d2),(m2 div d2) are_coprime by A2,Lm12;
then consider s being Integer such that
A18: ((b div d2)*s - (c2 div d2)) mod (m2 div d2) = 0 by Th15;
A19: m1 = (m1 div d1)*d1 by Lm11,INT_2:21;
then
A20: (m1 div d1) divides m1;
A21: (m1 div d1),(m2 div d2) are_coprime
proof
reconsider e = (m1 div d1) gcd (m2 div d2) as Element of NAT by
ORDINAL1:def 12;
assume not (m1 div d1),(m2 div d2) are_coprime;
then
A22: (m1 div d1) gcd (m2 div d2) <> 1 by INT_2:def 3;
e divides (m2 div d2) by INT_2:21;
then
A23: e divides m2 by A13,INT_2:9;
e divides (m1 div d1) by INT_2:21;
then e divides m1 by A20,INT_2:9;
then e divides (m1 gcd m2) by A23,INT_2:22;
then e divides 1 by A5,INT_2:def 3;
hence contradiction by A22,WSIERP_1:15;
end;
then consider w being Integer such that
A24: ((m1 div d1)*w - (s-r)) mod (m2 div d2) = 0 by Th15;
take w,r,s;
A25: m1 div d1 <> 0 by A1,A19;
for x st (a*x-c1) mod m1 = 0 & (b*x-c2) mod m2 = 0 holds x,(r + (m1 div
(a gcd m1))*w) are_congruent_mod ((m1 div (a gcd m1))*(m2 div (b gcd m2)))
proof
let x;
assume that
A26: (a*x-c1) mod m1 = 0 and
A27: (b*x-c2) mod m2 = 0;
(m1 div d1)*d1 divides ((a div d1)*x - (c1 div d1))*d1 by A1,A19,A15,A16
,A26,Lm10;
then (m1 div d1) divides ((a div d1)*x - (c1 div d1)) by A7,Th7;
then ((a div d1)*x - (c1 div d1)) mod (m1 div d1) = 0;
then r in Class(Cong(m1 div d1),x) by A8,A9,A25,Th26;
then [x,r] in Cong(m1 div d1) by EQREL_1:18;
then x,r are_congruent_mod (m1 div d1) by Def1;
then
A28: (m1 div d1) divides (x-r);
(m2 div d2)*d2 divides ((b div d2)*x - (c2 div d2))*d2 by A2,A12,A10,A11
,A27,Lm10;
then (m2 div d2) divides ((b div d2)*x - (c2 div d2)) by A6,Th7;
then ((b div d2)*x - (c2 div d2)) mod (m2 div d2) = 0;
then s in Class(Cong(m2 div d2),x) by A17,A18,A14,Th26;
then [x,s] in Cong(m2 div d2) by EQREL_1:18;
then x,s are_congruent_mod (m2 div d2) by Def1;
then
A29: (m2 div d2) divides (x-s);
(m2 div d2) divides ((m1 div d1)*w - (s-r)) by A14,A24,Lm10;
then
A30: (m2 div d2) divides ((x-s) - (((m1 div d1)*w + r) - s)) by A29,Lm4;
(m1 div d1) divides (m1 div d1)*w;
then (m1 div d1) divides ((x - r) - (m1 div d1)*w) by A28,Lm4;
then
(m1 div d1)* (m2 div d2) divides (x - (r + (m1 div d1)*w)) by A21,A30,Lm13;
hence thesis;
end;
hence thesis by A9,A18,A24;
end;
theorem
m1 <> 0 & m2 <> 0 & m3 <> 0 & m1,m2 are_coprime & m1,m3
are_coprime & m2,m3 are_coprime implies ex r,s st for x st (x-a)
mod m1=0 & (x-b) mod m2=0 & (x-c) mod m3=0 holds x,(a+m1*r+m1*m2*s)
are_congruent_mod (m1*m2*m3) & (m1*r-(b-a)) mod m2 = 0 & (m1*m2*s-(c-a-m1*r))
mod m3 = 0
proof
assume that
A1: m1 <> 0 & m2 <> 0 and
A2: m3 <> 0 and
A3: m1,m2 are_coprime and
A4: m1,m3 are_coprime & m2,m3 are_coprime;
consider r such that
A5: for x st (x-a) mod m1 = 0 & (x-b) mod m2 = 0 holds x,(a+m1*r)
are_congruent_mod (m1*m2) and
A6: (m1*r-(b-a)) mod m2=0 by A1,A3,Th40;
m1*m2 <> 0 by A1,XCMPLX_1:6;
then consider s such that
A7: ( for x st (x-(a+m1*r)) mod m1*m2 = 0 & (x-c) mod m3 = 0 holds x,(a+
m1*r+ m1*m2 *s) are_congruent_mod m1*m2*m3)& ((m1*m2)*s - (c-(a+m1*r))) mod m3
= 0 by A2,A4,Th40,INT_2:26;
take r,s;
for x st (x-a) mod m1=0 & (x-b) mod m2=0 & (x-c) mod m3=0 holds x,(a+m1*
r+m1*m2*s) are_congruent_mod (m1*m2*m3) & (m1*r-(b-a)) mod m2 = 0 & (m1*m2*s-(c
-a-m1*r)) mod m3 = 0
proof
let x;
assume that
A8: (x-a) mod m1=0 & (x-b) mod m2=0 and
A9: (x-c) mod m3=0;
x,(a+m1*r) are_congruent_mod (m1*m2) by A5,A8;
then m1*m2 divides (x - (a+m1*r));
then (x - (a+m1*r)) mod m1*m2 = 0;
hence thesis by A6,A7,A9;
end;
hence thesis;
end;
theorem
m1 <> 0 & m2 <> 0 & m3 <> 0 & (not (m1 gcd m2) divides (a - b) or not
(m1 gcd m3) divides (a - c) or not (m2 gcd m3) divides (b - c)) implies not ex
x st (x-a) mod m1 = 0 & (x-b) mod m2 = 0 & (x-c) mod m3 = 0 by Th41;
theorem Th46:
for n1,n2,n3 being non zero Nat holds (n1 gcd n3) lcm
(n2 gcd n3) = (n1 lcm n2) gcd n3
proof
let n1,n2,n3 be non zero Nat;
set d1 = n1 gcd n3;
set d2 = n2 gcd n3;
set M = n1 lcm n2;
reconsider d = M gcd n3 as non zero Nat by INT_2:5;
reconsider M as non zero Nat by INT_2:4;
d1 divides n3 & d2 divides n3 by NAT_D:def 5;
then
A1: (d1 lcm d2) divides n3 by NAT_D:def 4;
d2 divides n2 & n2 divides M by NAT_D:def 4,def 5;
then
A2: d2 divides M by NAT_D:4;
A3: for p being Nat st p in support pfexp d holds (ppf d).p
divides n1 or (ppf d).p divides n2
proof
let p be Nat;
assume that
A4: p in support pfexp d and
A5: not (ppf d).p divides n1 and
A6: not (ppf d).p divides n2;
A7: not p|^(p |-count d) divides n2 by A4,A6,NAT_3:def 9;
A8: p is Prime by A4,NAT_3:34;
A9: not p|^(p |-count d) divides n1 by A4,A5,NAT_3:def 9;
A10: p |-count d > p |-count M
proof
A11: p |-count M = (pfexp M).p by A8,NAT_3:def 8
.= (max(pfexp n1,pfexp n2)).p by NAT_3:54;
per cases;
suppose
(pfexp n1).p <= (pfexp n2).p;
then p |-count M = (pfexp n2).p by A11,NAT_3:def 4
.= p |-count n2 by A8,NAT_3:def 8;
hence thesis by A7,A8,MOEBIUS1:9;
end;
suppose
(pfexp n1).p > (pfexp n2).p;
then p |-count M = (pfexp n1).p by A11,NAT_3:def 4
.= p |-count n1 by A8,NAT_3:def 8;
hence thesis by A9,A8,MOEBIUS1:9;
end;
end;
d divides M by NAT_D:def 5;
hence contradiction by A8,A10,NAT_3:30;
end;
A12: for p being Nat st p in support pfexp d holds (ppf d).p
divides (d1 lcm d2)
proof
A13: d2 divides (d1 lcm d2) by NAT_D:def 4;
let p be Nat;
A14: d1 divides (d1 lcm d2) by NAT_D:def 4;
assume
A15: p in support pfexp d;
then
A16: p is Prime by NAT_3:34;
d divides n3 by NAT_D:def 5;
then (p |-count d) <= (p |-count n3) by A16,NAT_3:30;
then p |^ (p |-count d) divides p |^ (p |-count n3) by NEWTON:89;
then
A17: (ppf d).p divides p|^(p |-count n3) by A15,NAT_3:def 9;
p<>1 by A16,INT_2:def 4;
then p|^(p |-count n3) divides n3 by NAT_3:def 7;
then
A18: (ppf d).p divides n3 by A17,NAT_D:4;
per cases by A3,A15;
suppose
(ppf d).p divides n1;
then (ppf d).p divides d1 by A18,NAT_D:def 5;
hence thesis by A14,NAT_D:4;
end;
suppose
(ppf d).p divides n2;
then (ppf d).p divides d2 by A18,NAT_D:def 5;
hence thesis by A13,NAT_D:4;
end;
end;
Product ppf d divides (d1 lcm d2)
proof
set g = ppf d;
set K = canFS(support g);
consider f being FinSequence of COMPLEX such that
A19: Product g = Product f and
A20: f = g*K by NAT_3:def 5;
rng f c= NAT by A20,VALUED_0:def 6;
then reconsider f as FinSequence of NAT by FINSEQ_1:def 4;
A21: rng K = support g by FUNCT_2:def 3;
then rng K c= NAT by XBOOLE_1:1;
then reconsider K as FinSequence of NAT by FINSEQ_1:def 4;
A22: for m,n being Element of NAT st m in dom f & n in dom f & m<>n holds
(f.m gcd f.n)=1
proof
let m,n be Element of NAT;
assume that
A23: m in dom f and
A24: n in dom f and
A25: m<>n;
A26: m in dom K by A20,A23,FUNCT_1:11;
then K.m in support g by A21,FUNCT_1:3;
then
A27: K.m in support pfexp d by NAT_3:def 9;
then
A28: K.m is prime by NAT_3:34;
A29: n in dom K by A20,A24,FUNCT_1:11;
then K.n in support g by A21,FUNCT_1:3;
then
A30: K.n in support pfexp d by NAT_3:def 9;
then
A31: K.n is prime by NAT_3:34;
f.n = g.(K.n) by A20,A24,FUNCT_1:12;
then
A32: f.n = (K.n)|^((K.n) |-count d) by A30,NAT_3:def 9;
f.m = g.(K.m) by A20,A23,FUNCT_1:12;
then
A33: f.m = (K.m)|^((K.m) |-count d) by A27,NAT_3:def 9;
K.m <> K.n by A25,A26,A29,FUNCT_1:def 4;
then
A34: K.n,((K.m)|^((K.m) |-count d)) are_coprime by A28,A31,EULER_2:17
,INT_2:30;
A35: K.n > 0 by A30,NAT_3:34;
K.m > 0 by A27,NAT_3:34;
then ((K.n)|^((K.n) |-count d)),((K.m)|^((K.m) |-count d))
are_coprime by A35,A34,EULER_2:17;
hence thesis by A33,A32,INT_2:def 3;
end;
for m being Element of NAT st m in dom f holds f.m divides (d1 lcm d2 )
proof
let m be Element of NAT;
assume
A36: m in dom f;
then m in dom K by A20,FUNCT_1:11;
then K.m in support g by A21,FUNCT_1:3;
then K.m in support pfexp d by NAT_3:def 9;
then g.(K.m) divides (d1 lcm d2) by A12;
hence thesis by A20,A36,FUNCT_1:12;
end;
hence thesis by A19,A22,Th38;
end;
then
A37: d divides (d1 lcm d2) by NAT_3:61;
d1 divides n1 & n1 divides M by NAT_D:def 4,def 5;
then d1 divides M by NAT_D:4;
then (d1 lcm d2) divides M by A2,NAT_D:def 4;
then (d1 lcm d2) divides d by A1,NAT_D:def 5;
hence thesis by A37,NAT_D:5;
end;
theorem
for n1,n2,n3 being non zero Nat st (n1 gcd n2) divides (a-b
) holds ex r,s st for x st (x-a) mod n1=0 & (x-b) mod n2=0 & (x-c) mod n3=0
holds x,((a+n1*r)+(n1 lcm n2)*s) are_congruent_mod ((n1 lcm n2) lcm n3) & ((n1
div (n1 gcd n2))*r-((b-a) div (n1 gcd n2))) mod (n2 div (n1 gcd n2))=0 & (((n1
lcm n2) div ((n1 lcm n2) gcd n3))*s-((c-(a+n1*r)) div ((n1 lcm n2) gcd n3)))
mod (n3 div ((n1 lcm n2) gcd n3))=0
proof
let n1,n2,n3 be non zero Nat;
set d1 = (n1 gcd n2);
set d2 = (n1 gcd n3);
set d3 = (n2 gcd n3);
set dd1 = n1 gcd n2;
set K = n1 lcm n2;
A1: n2 divides (n1 lcm n2) by NAT_D:def 4;
assume (n1 gcd n2) divides (a-b);
then d1 divides -(a-b) by INT_2:10;
then consider r such that
A2: for x st (x-a) mod n1=0 & (x-b) mod n2=0 holds x,(a+n1*r)
are_congruent_mod K and
A3: ((n1 div dd1)*r - ((b-a) div dd1)) mod (n2 div dd1) = 0 by Th42;
take r;
set y = a + n1*r;
A4: (K div (K gcd n3)),(n3 div (K gcd n3)) are_coprime by Lm12;
then consider s such that
A5: ( (K div (K gcd n3))*s - ((c-y) div (K gcd n3))) mod (n3 div (K gcd
n3)) = 0 by Th15;
take s;
A6: n1 divides (n1 lcm n2) by NAT_D:def 4;
A7: for x st (x - a) mod n1 = 0 & (x - b) mod n2 = 0 & (x - c) mod n3 = 0
holds ((n1 lcm n2) gcd n3) divides (y-c)
proof
let x;
assume that
A8: (x - a) mod n1 = 0 & (x - b) mod n2 = 0 and
A9: (x - c) mod n3 = 0;
A10: n3 divides (x - c) by A9,Lm10;
x,y are_congruent_mod K by A2,A8;
then K divides (x - y);
then
A11: K divides -(x-y) by INT_2:10;
then n1 divides (y - x) by A6,INT_2:9;
then consider t1 being Integer such that
A12: (y-x) = n1 * t1;
d3 divides n3 by NAT_D:def 5;
then
A13: d3 divides (x - c) by A10,INT_2:9;
d2 divides n3 by NAT_D:def 5;
then
A14: d2 divides (x - c) by A10,INT_2:9;
n2 divides (y - x) by A1,A11,INT_2:9;
then consider t2 being Integer such that
A15: (y-x) = n2 * t2;
d3 divides n2 by NAT_D:def 5;
then
A16: d3 divides n2 * t2 by INT_2:2;
y - c = (x - c) + n2 * t2 by A15;
then
A17: d3 divides (y - c) by A16,A13,WSIERP_1:4;
d2 divides n1 by NAT_D:def 5;
then
A18: d2 divides n1 * t1 by INT_2:2;
y - c = (x - c) + n1 * t1 by A12;
then d2 divides (y - c) by A18,A14,WSIERP_1:4;
then (d2 lcm d3) divides (y - c) by A17,INT_2:19;
hence thesis by Th46;
end;
for x st (x-a) mod n1=0 & (x-b) mod n2=0 & (x-c) mod n3=0 holds x,(y +
(n1 lcm n2)*s) are_congruent_mod ((n1 lcm n2) lcm n3)
proof
A19: K <> 0 by INT_2:4;
let x;
assume that
A20: (x-a) mod n1=0 & (x-b) mod n2=0 and
A21: (x-c) mod n3=0;
((n1 lcm n2) gcd n3) divides (y-c) by A7,A20,A21;
then (K gcd n3) divides -(y-c) by INT_2:10;
then consider w being Integer such that
A22: for x st (x-y) mod K = 0 & (x-c) mod n3 = 0 holds x,(y + K*w)
are_congruent_mod (K lcm n3) and
A23: ((K div (K gcd n3))*w - ((c-y) div (K gcd n3))) mod (n3 div (K
gcd n3)) = 0 by A19,Th42;
A24: n3 = (n3 div (K gcd n3)) * (K gcd n3) by Lm11,INT_2:21;
then n3 div (K gcd n3) <> 0;
then w in Class(Cong(n3 div (K gcd n3)),s) by A4,A5,A23,Th26;
then [s,w] in Cong(n3 div (K gcd n3)) by EQREL_1:18;
then s,w are_congruent_mod (n3 div (K gcd n3)) by Def1;
then
A25: K*s,K*w are_congruent_mod K*(n3 div (K gcd n3)) by Th10;
K*(n3 div (K gcd n3)) = (K div (K gcd n3))*(K gcd n3)*(n3 div (K gcd
n3)) by Lm11,INT_2:21
.= n3*(K div (K gcd n3)) by A24;
then K*s,K*w are_congruent_mod n3 by A25,INT_1:20;
then
A26: n3 divides (K*s - K*w);
K divides K*(s - w);
then (K lcm n3) divides ((K*s + y) - (K*w + y)) by A26,INT_2:19;
then (K*s + y),(K*w + y) are_congruent_mod (K lcm n3);
then
A27: (K*w + y),(K*s + y) are_congruent_mod (K lcm n3) by INT_1:14;
x,y are_congruent_mod K by A2,A20;
then K divides (x - y);
then (x - y) mod K = 0;
then x,(K*w + y) are_congruent_mod (K lcm n3) by A21,A22;
hence thesis by A27,INT_1:15;
end;
hence thesis by A3,A5;
end;
begin :: CRS
reserve
a,b,c,m for Element of NAT;
definition
let m be Nat, X be set;
pred X is_CRS_of m means
ex fp being FinSequence of INT st X = rng fp & len fp = m &
for b being Nat st b in dom fp holds fp.b in Class(Cong m, b-'1);
end;
theorem
{ a where a is Nat: a < m } is_CRS_of m
proof
deffunc F(Nat) = $1-'1;
consider fp being FinSequence such that
A1: len fp=m & for a be Nat st a in dom fp holds fp.a=F(a) from FINSEQ_1
:sch 2;
for a being Nat st a in dom fp holds fp.a in INT
proof
let a be Nat;
assume a in dom fp;
then fp.a=F(a) by A1;
hence thesis by INT_1:def 2;
end;
then reconsider fp as FinSequence of INT by FINSEQ_2:12;
A2: { a where a is Nat: a < m } = rng fp
proof
set A = { a where a is Nat: a < m };
A3: rng fp c= A
proof
let b be object;
assume b in rng fp;
then consider k being object such that
A4: k in dom fp and
A5: b = fp.k by FUNCT_1:def 3;
reconsider k as Element of NAT by A4;
A6: k in Seg m by A1,A4,FINSEQ_1:def 3;
then k<=m by FINSEQ_1:1;
then
A7: k-1<m by XREAL_1:147;
k>=1 by A6,FINSEQ_1:1;
then
A8: k-'1<m by A7,XREAL_1:233;
reconsider b as Integer by A5;
b = k-'1 by A1,A4,A5;
hence thesis by A8;
end;
A c= rng fp
proof
let b be object;
assume b in A;
then consider k being Nat such that
A9: k = b and
A10: k < m;
k+1>=1 & k+1<=m by A10,NAT_1:11,13;
then
A11: k+1 in dom fp by A1,FINSEQ_3:25;
then fp.(k+1) = (k+1)-'1 by A1
.= k by NAT_D:34;
hence thesis by A9,A11,FUNCT_1:def 3;
end;
hence thesis by A3;
end;
for a be Nat st a in dom fp holds fp.a in Class(Cong(m),a-'1)
proof
let a be Nat;
(a-'1),(a-'1) are_congruent_mod m by INT_1:11;
then
A12: [a-'1,a-'1] in Cong(m) by Def1;
assume a in dom fp;
then fp.a = a-'1 by A1;
hence thesis by A12,EQREL_1:18;
end;
hence thesis by A1,A2;
end;
theorem Th49:
for X being finite set st X is_CRS_of m holds card X = m & for x
,y being Integer st x in X & y in X & x<>y holds not [x,y] in Cong m
proof
let X be finite set;
assume X is_CRS_of m;
then consider fp being FinSequence of INT such that
A1: X = rng fp and
A2: len fp = m and
A3: for b be Nat st b in dom fp holds fp.b in Class(Cong(m),b-'1);
A4: for x,y being Integer st x in X & y in X & x<>y holds not [x,y] in Cong (m)
proof
let x,y be Integer;
assume that
A5: x in X and
A6: y in X and
A7: x<>y;
consider a being object such that
A8: a in dom fp and
A9: x = fp.a by A1,A5,FUNCT_1:def 3;
reconsider a as Element of NAT by A8;
x in Class(Cong(m),a-'1) by A3,A8,A9;
then [a-'1,x] in Cong(m) by EQREL_1:18;
then
A10: (a-'1),x are_congruent_mod m by Def1;
consider b being object such that
A11: b in dom fp and
A12: y = fp.b by A1,A6,FUNCT_1:def 3;
reconsider b as Element of NAT by A11;
A13: b in Seg m by A2,A11,FINSEQ_1:def 3;
then
A14: b>=1 by FINSEQ_1:1;
y in Class(Cong(m),b-'1) by A3,A11,A12;
then [b-'1,y] in Cong(m) by EQREL_1:18;
then (b-'1),y are_congruent_mod m by Def1;
then
A15: y,(b-'1) are_congruent_mod m by INT_1:14;
assume [x,y] in Cong(m);
then x,y are_congruent_mod m by Def1;
then x,(b-'1) are_congruent_mod m by A15,INT_1:15;
then (a-'1),(b-'1) are_congruent_mod m by A10,INT_1:15;
then
A16: m divides ((a-'1)-(b-'1));
A17: a in Seg m by A2,A8,FINSEQ_1:def 3;
then
A18: a>=1 by FINSEQ_1:1;
b<=m by A13,FINSEQ_1:1;
then a-b >= 1-m by A18,XREAL_1:13;
then
A19: a-b > -m by XREAL_1:145;
a<=m by A17,FINSEQ_1:1;
then a-b <= m-1 by A14,XREAL_1:13;
then a-b < m by XREAL_1:147;
then |.a-b.| < m by A19,SEQ_2:1;
then
A20: |.a-b.| < |.m.| by ABSVALUE:def 1;
A21: (a-'1)-(b-'1) = (a-1)-(b-'1) by A18,XREAL_1:233
.=(a-1)-(b-1) by A14,XREAL_1:233
.= (a-b);
now
assume a<>b;
then (a-b)<>0;
hence contradiction by A16,A21,A20,Th6;
end;
hence contradiction by A7,A9,A12;
end;
for a,b being object st a in dom fp & b in dom fp & fp.a = fp.b holds a = b
proof
let a,b be object;
assume that
A22: a in dom fp and
A23: b in dom fp and
A24: fp.a = fp.b;
reconsider a,b as Element of NAT by A22,A23;
A25: b in Seg m by A2,A23,FINSEQ_1:def 3;
then
A26: b>=1 by FINSEQ_1:1;
reconsider l=fp.a,ll=fp.b as Element of INT by A22,A23,FINSEQ_2:11;
fp.b in Class(Cong(m),b-'1) by A3,A23;
then [b-'1,fp.b] in Cong(m) by EQREL_1:18;
then (b-'1),ll are_congruent_mod m by Def1;
then
A27: l,(b-'1) are_congruent_mod m by A24,INT_1:14;
A28: a in Seg m by A2,A22,FINSEQ_1:def 3;
then
A29: a>=1 by FINSEQ_1:1;
then
A30: (a-'1)-(b-'1) = (a-1)-(b-'1) by XREAL_1:233
.=(a-1)-(b-1) by A26,XREAL_1:233
.= (a-b);
b<=m by A25,FINSEQ_1:1;
then a-b >= 1-m by A29,XREAL_1:13;
then
A31: a-b > -m by XREAL_1:145;
a<=m by A28,FINSEQ_1:1;
then a-b <= m-1 by A26,XREAL_1:13;
then a-b < m by XREAL_1:147;
then |.a-b.| < m by A31,SEQ_2:1;
then
A32: |.a-b.| < |.m.| by ABSVALUE:def 1;
fp.a in Class(Cong(m),a-'1) by A3,A22;
then [a-'1,fp.a] in Cong(m) by EQREL_1:18;
then (a-'1),l are_congruent_mod m by Def1;
then (a-'1),(b-'1) are_congruent_mod m by A27,INT_1:15;
then
A33: m divides (a-b) by A30;
now
assume a<>b;
then (a-b)<>0;
hence contradiction by A33,A32,Th6;
end;
hence thesis;
end;
then fp is one-to-one;
hence thesis by A1,A2,A4,FINSEQ_4:62;
end;
theorem Th50:
{} is_CRS_of m iff m = 0
proof
set fp=<*>INT;
thus {} is_CRS_of m implies m = 0 by Th49,CARD_1:27;
assume m = 0;
then
A1: len fp = m;
{} = rng fp & for b be Nat st b in dom fp holds fp.b in Class(Cong(m),b -'1);
hence thesis by A1;
end;
theorem Th51:
for X being finite set st card X = m holds ex fp being
FinSequence st len fp = m & (for a st a in dom fp holds fp.a in X) & fp is
one-to-one
proof
defpred P[Nat] means for X being finite set holds card X = $1 implies ex fp
being FinSequence st len fp = $1 & (for a st a in dom fp holds fp.a in X) & fp
is one-to-one;
let X be finite set;
A1: for m being Nat st P[m] holds P[m + 1]
proof
let m be Nat such that
A2: P[m];
let X be finite set;
assume
A3: card X = m + 1;
then consider x being object such that
A4: x in X by CARD_1:27,XBOOLE_0:def 1;
set Y = X\{x};
card Y = card X - card {x} by A4,EULER_1:4
.= (m+1) - 1 by A3,CARD_1:30
.= m;
then consider fp1 being FinSequence such that
A5: len fp1 = m and
A6: for a st a in dom fp1 holds fp1.a in Y and
A7: fp1 is one-to-one by A2;
set fp = fp1^<*x*>;
A8: len fp = m + 1 by A5,FINSEQ_2:16;
for a,b being object st a in dom fp & b in dom fp & a<>b
holds fp.a <> fp.b
proof
let a,b be object;
assume that
A9: a in dom fp and
A10: b in dom fp and
A11: a<>b;
A12: a in Seg (m+1) by A8,A9,FINSEQ_1:def 3;
A13: b in Seg (m+1) by A8,A10,FINSEQ_1:def 3;
reconsider a,b as Element of NAT by A9,A10;
per cases by A12,FINSEQ_2:7;
suppose
A14: a in Seg m;
per cases by A13,FINSEQ_2:7;
suppose
b in Seg m;
then
A15: b in dom fp1 by A5,FINSEQ_1:def 3;
then
A16: fp.b = fp1.b by FINSEQ_1:def 7;
A17: a in dom fp1 by A5,A14,FINSEQ_1:def 3;
then fp.a = fp1.a by FINSEQ_1:def 7;
hence thesis by A7,A11,A17,A15,A16;
end;
suppose
A18: b = m + 1;
a in dom fp1 by A5,A14,FINSEQ_1:def 3;
then fp1.a in Y & fp.a = fp1.a by A6,FINSEQ_1:def 7;
then
A19: not fp.a in {x} by XBOOLE_0:def 5;
fp.b = x by A5,A18,FINSEQ_1:42;
hence thesis by A19,TARSKI:def 1;
end;
end;
suppose
A20: a = m + 1;
then b in Seg m by A11,A13,FINSEQ_2:7;
then b in dom fp1 by A5,FINSEQ_1:def 3;
then fp1.b in Y & fp.b = fp1.b by A6,FINSEQ_1:def 7;
then not fp.b in {x} by XBOOLE_0:def 5;
then fp.b <> x by TARSKI:def 1;
hence thesis by A5,A20,FINSEQ_1:42;
end;
end;
then
A21: for a,b being object st a in dom fp & b in dom fp & fp.a = fp.b
holds a = b;
take fp;
for a being object st a in dom fp holds fp.a in X
proof
let a be object;
assume a in dom fp;
then
A22: a in Seg (m+1) by A8,FINSEQ_1:def 3;
per cases by A22,FINSEQ_2:7;
suppose
a in Seg m;
then
A23: a in dom fp1 by A5,FINSEQ_1:def 3;
then fp.a = fp1.a by FINSEQ_1:def 7;
then fp.a in Y by A6,A23;
hence thesis;
end;
suppose
a = m + 1;
hence thesis by A4,A5,FINSEQ_1:42;
end;
end;
hence thesis by A5,A21,FINSEQ_2:16;
end;
A24: P[0]
proof
set fp = <*>NAT;
let X be finite set;
assume card X = 0;
take fp;
thus len fp = 0;
thus thesis;
end;
for m being Nat holds P[m] from NAT_1:sch 2(A24,A1);
hence thesis;
end;
theorem Th52:
for X being finite Subset of INT st card X = m & (for x,y being
Integer st x in X & y in X & x<>y holds not [x,y] in Cong m) holds X is_CRS_of
m
proof
let X be finite Subset of INT;
assume that
A1: card X = m and
A2: for x,y being Integer st x in X & y in X & x<>y holds not [x,y] in Cong(m);
per cases;
suppose
X is empty;
hence thesis by A1,Th50;
end;
suppose
X is non empty;
then reconsider X as non empty finite Subset of INT;
defpred P[Nat,set] means $2 in Class(Cong(m),$1-'1);
A3: X <> {};
A4: for a be Nat st a in Seg m ex y being Element of X st P[a,y]
proof
set Y = Segm m;
let a be Nat such that
A5: a in Seg m;
a<=m by A5,FINSEQ_1:1;
then
A6: a-1<m by XREAL_1:147;
consider fp being FinSequence such that
A7: len fp = m and
A8: for b st b in dom fp holds fp.b in X and
A9: fp is one-to-one by A1,Th51;
for b being Nat st b in dom fp holds fp.b in X by A8;
then reconsider fp as FinSequence of X by FINSEQ_2:12;
defpred PP[Nat,set] means fp.$1 in Class(Cong(m),$2);
A10: for c st c in Seg m ex r being Element of Y st PP[c,r]
proof
let c;
assume c in Seg m;
consider q,r being Integer such that
A11: fp.c = m * q + r and
A12: r >= 0 and
A13: r < m by A1,Th13;
fp.c mod m = r mod m by A11,NAT_D:61;
then r,fp.c are_congruent_mod m by A1,NAT_D:64;
then
A14: [r,fp.c] in Cong(m) by Def1;
reconsider r as Element of NAT by A12,INT_1:3;
reconsider r as Element of Y by A13,NAT_1:44;
take r;
thus thesis by A14,EQREL_1:18;
end;
reconsider Y as non empty set by A1,A3;
A15: for c be Nat st c in Seg m ex r being Element of Y st PP[c,r] by A10;
consider fr being FinSequence of Y such that
A16: dom fr = Seg m & for c be Nat st c in Seg m holds PP[c,fr.c]
from FINSEQ_1:sch 5(A15);
for x1,x2 being object st x1 in dom fr & x2 in dom fr & fr.x1 = fr.x2
holds x1 = x2
proof
let x1,x2 be object;
assume that
A17: x1 in dom fr and
A18: x2 in dom fr and
A19: fr.x1 = fr.x2;
fp.x1 in Class(Cong(m),fr.x1) & fp.x2 in Class(Cong(m),fr.x1) by A16
,A17,A18,A19;
then
A20: [fp.x1,fp.x2] in Cong(m) by EQREL_1:22;
assume
A21: x1 <> x2;
reconsider x1,x2 as Element of NAT by A17,A18;
A22: x1 in dom fp by A7,A16,A17,FINSEQ_1:def 3;
then
A23: fp.x1 in X by FINSEQ_2:11;
A24: x2 in dom fp by A7,A16,A18,FINSEQ_1:def 3;
then
A25: fp.x2 in X by FINSEQ_2:11;
fp.x1 <> fp.x2 by A9,A21,A22,A24;
hence contradiction by A2,A20,A23,A25;
end;
then fr is one-to-one;
then
A26: card rng fr = len fr by FINSEQ_4:62
.= m by A16,FINSEQ_1:def 3;
reconsider Y as finite set;
a>=1 by A5,FINSEQ_1:1;
then a-'1<m by A6,XREAL_1:233;
then
A27: a-'1 in Y by NAT_1:44;
card Y = m;
then rng fr = Y by A26,CARD_2:102;
then consider w being object such that
A28: w in dom fr and
A29: fr.w = a-'1 by A27,FUNCT_1:def 3;
reconsider w as Element of NAT by A28;
w in dom fp by A7,A16,A28,FINSEQ_1:def 3;
then reconsider y = fp.w as Element of X by FINSEQ_2:11;
take y;
thus thesis by A16,A28,A29;
end;
consider fp being FinSequence of X such that
A30: dom fp = Seg m & for a be Nat st a in Seg m holds P[a,fp.a] from
FINSEQ_1:sch 5(A4);
A31: rng fp c= X by FINSEQ_1:def 4;
A32: len fp = m by A30,FINSEQ_1:def 3;
for a,b being object st a in dom fp & b in dom fp & fp.a = fp.b
holds a = b
proof
let a,b be object;
assume that
A33: a in dom fp and
A34: b in dom fp and
A35: fp.a = fp.b;
reconsider a,b as Element of NAT by A33,A34;
A36: b>=1 by A30,A34,FINSEQ_1:1;
A37: a>=1 by A30,A33,FINSEQ_1:1;
then
A38: (a-'1)-(b-'1) = (a-1)-(b-'1) by XREAL_1:233
.= (a-1)-(b-1) by A36,XREAL_1:233
.= a-b;
reconsider l=fp.a,ll=fp.b as Element of INT by A33,A34,FINSEQ_2:11;
fp.b in Class(Cong(m),b-'1) by A30,A34;
then [b-'1,fp.b] in Cong(m) by EQREL_1:18;
then (b-'1),ll are_congruent_mod m by Def1;
then
A39: l,(b-'1) are_congruent_mod m by A35,INT_1:14;
b<=m by A30,A34,FINSEQ_1:1;
then a-b >= 1-m by A37,XREAL_1:13;
then
A40: a-b > -m by XREAL_1:145;
a<=m by A30,A33,FINSEQ_1:1;
then a-b <= m-1 by A36,XREAL_1:13;
then a-b < m by XREAL_1:147;
then |.a-b.| < m by A40,SEQ_2:1;
then
A41: |.a-b.| < |.m.| by ABSVALUE:def 1;
fp.a in Class(Cong(m),a-'1) by A30,A33;
then [a-'1,fp.a] in Cong(m) by EQREL_1:18;
then (a-'1),l are_congruent_mod m by Def1;
then (a-'1),(b-'1) are_congruent_mod m by A39,INT_1:15;
then
A42: m divides (a-b) by A38;
now
assume a<>b;
then a-b<>0;
hence contradiction by A42,A41,Th6;
end;
hence thesis;
end;
then fp is one-to-one;
then card X = card(rng fp) by A1,A32,FINSEQ_4:62;
then X = rng fp by A31,CARD_2:102;
hence thesis by A30,A32;
end;
end;
reserve a for Integer;
theorem
for X being finite Subset of INT st X is_CRS_of m holds (a ++ X) is_CRS_of m
proof
let X be finite Subset of INT;
assume
A1: X is_CRS_of m;
then card X = m by Th49;
then
A2: card (a ++ X) = m by Th2;
A3: for i,j being Integer st i in a++X & j in a++X & i<>j holds not [i,j] in
Cong(m)
proof
let i,j be Integer;
assume that
A4: i in a++X and
A5: j in a++X and
A6: i<>j;
consider u being Complex such that
A7: i=a+u and
A8: u in X by A4,MEMBER_1:143;
consider w being Complex such that
A9: j=a+w and
A10: w in X by A5,MEMBER_1:143;
reconsider u9=u, w9=w as Integer by A8,A10;
assume [i,j] in Cong(m);
then i,j are_congruent_mod m by Def1;
then m divides ((a+u9)-(a+w9)) by A7,A9;
then m divides (u9-w9);
then
A11: u9,w9 are_congruent_mod m;
not [u9,w9] in Cong(m) by A1,A6,A8,A7,A10,A9,Th49;
hence contradiction by A11,Def1;
end;
a ++ X is Subset of INT by Lm1;
hence thesis by A2,A3,Th52;
end;
theorem
for X being finite Subset of INT st a,m are_coprime & X
is_CRS_of m holds (a ** X) is_CRS_of m
proof
let X be finite Subset of INT;
assume that
A1: a,m are_coprime and
A2: X is_CRS_of m;
A3: card X = m by A2,Th49;
A4: a ** X c= INT by Lm2;
per cases;
suppose
A5: a = 0;
then a gcd m = |.m.| by WSIERP_1:8
.= m by ABSVALUE:def 1;
then
A6: m = 1 by A1,INT_2:def 3;
then ex x being object st X = {x} by A3,CARD_2:42;
then
A7: a ** X = {0} by A5,Th4;
A8: for x,y being Integer st x in a**X & y in a**X & x<>y holds not [x,y]
in Cong(m)
proof
let x,y be Integer;
assume that
A9: x in a**X and
A10: y in a**X & x<>y;
assume [x,y] in Cong(m);
x = 0 by A7,A9,TARSKI:def 1;
hence contradiction by A7,A10,TARSKI:def 1;
end;
card (a ** X) = m by A6,A7,CARD_2:42;
hence thesis by A4,A8,Th52;
end;
suppose
A11: a <> 0;
A12: for x,y being Integer st x in a**X & y in a**X & x<>y holds not [x,y]
in Cong(m)
proof
let x,y be Integer;
assume that
A13: x in a**X and
A14: y in a**X and
A15: x<>y;
consider y1 being Integer such that
A16: y1 in X and
A17: y = a * y1 by A14,Lm3;
consider x1 being Integer such that
A18: x1 in X and
A19: x = a * x1 by A13,Lm3;
not [x1,y1] in Cong(m) by A2,A15,A18,A19,A16,A17,Th49;
then
A20: not x1,y1 are_congruent_mod m by Def1;
assume [x,y] in Cong(m);
then a*x1,a*y1 are_congruent_mod m by A19,A17,Def1;
hence contradiction by A1,A20,Th9;
end;
card (a ** X) = m by A3,A11,Th5;
hence thesis by A4,A12,Th52;
end;
end;