:: Linear Congruence Relation and Complete Residue Systems :: by Xiquan Liang , Li Yan and Junjie Zhao :: :: Received August 28, 2007 :: Copyright (c) 2007-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, 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; ::$CT 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; ::$CT 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;