:: Linear Congruence Relation and Complete Residue Systems
:: by Xiquan Liang , Li Yan and Junjie Zhao
::
:: Received August 28, 2007
:: Copyright (c) 2007-2016 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;
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 :: INT_4:1
for X being real-membered set, a being Real holds X, a ++
X are_equipotent;
registration
let X be finite real-membered set, a be Real;
cluster a ++ X -> finite;
end;
theorem :: INT_4:2
for X being real-membered set, a being Real holds card X =
card (a ++ X);
theorem :: INT_4:3
for X being real-membered set, a being Real st a <> 0
holds X, a ** X are_equipotent;
theorem :: INT_4:4
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});
registration
let X be finite real-membered set, a be Real;
cluster a ** X -> finite;
end;
theorem :: INT_4:5
for X being real-membered set, a being Real st a <> 0
holds card X = card (a ** X);
begin
theorem :: INT_4:6
i divides i1 & i1<>0 implies |.i.|<=|.i1.|;
theorem :: INT_4:7
for i3 st i3 <> 0 holds i1 divides i2 iff i1*i3 divides i2*i3;
theorem :: INT_4:8
for a,b,m being Nat for n being Element of NAT st a mod m = b mod m
holds (a|^n) mod m = (b|^n) mod m;
theorem :: INT_4:9
i1*i,i2*i are_congruent_mod i3 & i,i3 are_coprime implies
i1,i2 are_congruent_mod i3;
theorem :: INT_4:10
i1,i2 are_congruent_mod i3 implies i1*k,i2*k are_congruent_mod i3*k;
theorem :: INT_4:11
i1,i2 are_congruent_mod i implies i1*i3,i2*i3 are_congruent_mod i;
theorem :: INT_4:12
for i being Integer holds 0 = 0 mod i;
theorem :: INT_4:13
for b st b>0 for a ex q,r being Integer st a=(b*q)+r & r>=0 & r< b;
theorem :: INT_4:14
i1,i2 are_congruent_mod i3 implies i1 gcd i3 = i2 gcd i3;
theorem :: INT_4:15
a,m are_coprime implies ex x being Integer st (a*x-b) mod m = 0;
theorem :: INT_4:16
m>0 & a,m are_coprime implies ex n being Nat st (a*n-b) mod m = 0;
theorem :: INT_4:17
m<>0 & not (a gcd m) divides b implies not ex x being Integer st (a*x-
b) mod m = 0;
theorem :: INT_4:18
m<>0 & (a gcd m) divides b implies ex x being Integer st (a*x-b) mod m = 0;
begin
theorem :: INT_4:19
n>0 & p>0 implies p*q mod p|^n = p*(q mod p|^(n-'1));
theorem :: INT_4:20
p*q mod p*n = p*(q mod n);
theorem :: INT_4:21
n>0 & p is prime & p,q are_coprime implies not p divides (q mod p|^n);
theorem :: INT_4:22
for p,q,n being Nat st n>0 holds (p - q) mod n = 0 iff p mod n = q mod n;
theorem :: INT_4:23
for a,b,m being Nat st m > 0 holds a mod m = b mod m iff m divides (a- b);
theorem :: INT_4:24
n>0 & p is prime & p,q are_coprime implies not ex x being
Integer st (p*x^2 - q) mod p|^n = 0;
theorem :: INT_4:25
n>0 & p is prime & p,q are_coprime implies not ex x being
Integer st (p*x - q) mod p|^n = 0;
begin
definition
let m be Integer;
func Cong(m) -> Relation of INT means
:: INT_4:def 1
[x,y] in it iff x,y are_congruent_mod m;
end;
registration
let m be Integer;
cluster Cong m -> total;
end;
registration
let m be Integer;
cluster Cong m -> reflexive symmetric transitive;
end;
theorem :: INT_4:26
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);
theorem :: INT_4:27
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;
theorem :: INT_4:28
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;
theorem :: INT_4:29 :: 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;
begin
reserve fp,fp1 for FinSequence of NAT,
b,c,d, n for Element of NAT,
a for Nat;
theorem :: INT_4:30
for b,n st b in dom fp & len fp = n+1 holds Del(fp^<*d*>,b) = Del(fp,b)^<*d*>
;
theorem :: INT_4:31
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;
theorem :: INT_4:32
for a st a in dom fp holds fp.a divides Product fp;
theorem :: INT_4:33
a in dom fp & p divides fp.a implies p divides Product fp;
theorem :: INT_4:34
len fp = n+1 & a >= 1 & a <= n implies Del(fp,a).n = fp.(len fp);
theorem :: INT_4:35
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);
theorem :: INT_4:36
(for b being Nat st b in dom fp holds a divides fp.b) implies a
divides Sum fp;
theorem :: INT_4:37
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;
theorem :: INT_4:38
(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;
theorem :: INT_4:39
(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);
reserve i,m,m1,m2,m3,r,s,a,b,c,c1,c2,x,y for Integer;
theorem :: INT_4:40
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;
theorem :: INT_4:41
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;
theorem :: INT_4:42
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;
theorem :: INT_4:43
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;
theorem :: INT_4:44
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;
theorem :: INT_4:45
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;
theorem :: INT_4:46
for n1,n2,n3 being non zero Nat holds (n1 gcd n3) lcm
(n2 gcd n3) = (n1 lcm n2) gcd n3;
theorem :: INT_4:47
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;
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
:: INT_4:def 2
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 :: INT_4:48
{ a where a is Nat: a < m } is_CRS_of m;
theorem :: INT_4:49
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;
theorem :: INT_4:50
{} is_CRS_of m iff m = 0;
theorem :: INT_4:51
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;
theorem :: INT_4:52
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;
reserve a for Integer;
theorem :: INT_4:53
for X being finite Subset of INT st X is_CRS_of m holds (a ++ X) is_CRS_of m;
theorem :: INT_4:54
for X being finite Subset of INT st a,m are_coprime & X
is_CRS_of m holds (a ** X) is_CRS_of m;