:: The Chinese Remainder Theorem :: by Andrzej Kondracki :: :: Received December 30, 1997 :: Copyright (c) 1997-2018 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, NAT_1, INT_1, RAT_1, NEWTON, RELAT_1, ARYTM_1, ARYTM_3, XXREAL_0, CARD_1, PREPOWER, INT_2, COMPLEX1, SUBSET_1, FINSEQ_1, FUNCT_1, XBOOLE_0, ORDINAL4, TARSKI, CARD_3, FINSEQ_3, REAL_1, SQUARE_1, ORDINAL1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, RELAT_1, NUMBERS, XCMPLX_0, XREAL_0, INT_1, REAL_1, NAT_1, NAT_D, RAT_1, INT_2, XXREAL_0, VALUED_0, PREPOWER, SQUARE_1, FUNCT_1, FINSEQ_1, FINSEQ_3, RVSUM_1, FINSEQ_4, NEWTON, TREES_4; constructors REAL_1, SQUARE_1, NAT_1, NAT_D, BINOP_2, FINSEQ_3, FINSEQ_4, FINSOP_1, RVSUM_1, NEWTON, PREPOWER, TREES_4, RELSET_1, NUMBERS; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, INT_1, RAT_1, FINSEQ_1, NEWTON, VALUED_0, CARD_1, RVSUM_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: PRELIMINARIES reserve x,y,z for Real, a,b,c,d,e,f,g,h for Nat, k,l,m,n,m1,n1,m2,n2 for Integer, q for Rational; theorem :: WSIERP_1:1 x|^2=x*x & (-x)|^2=x|^2; theorem :: WSIERP_1:2 for a being Nat holds (-x)|^(2*a)=x|^(2*a) & (-x)|^(2*a+1)=-(x|^( 2*a+1)); theorem :: WSIERP_1:3 x>=0 & y>=0 & d>0 & x|^d=y|^d implies x=y; registration let k be Integer, a be natural Number; cluster k |^ a -> integer; end; theorem :: WSIERP_1:4 k divides m & k divides n implies k divides m+n; theorem :: WSIERP_1:5 k divides m & k divides n implies k divides m*m1+n*n1; theorem :: WSIERP_1:6 m gcd n = 1 & k gcd n = 1 implies m*k gcd n = 1; theorem :: WSIERP_1:7 a gcd b=1 & c gcd b=1 implies a*c gcd b=1; theorem :: WSIERP_1:8 0 gcd m = |.m.| & 1 gcd m = 1; theorem :: WSIERP_1:9 1,k are_coprime; theorem :: WSIERP_1:10 k,l are_coprime implies k|^a,l are_coprime; theorem :: WSIERP_1:11 k,l are_coprime implies k|^a,l|^b are_coprime; theorem :: WSIERP_1:12 k gcd l = 1 implies k gcd l|^b = 1 & k|^a gcd l|^b = 1; theorem :: WSIERP_1:13 |.m.| divides k iff m divides k; theorem :: WSIERP_1:14 a divides b implies (a|^c) divides (b|^c); theorem :: WSIERP_1:15 a divides 1 implies a=1; theorem :: WSIERP_1:16 d divides a & a gcd b = 1 implies d gcd b = 1; theorem :: WSIERP_1:17 k<>0 implies (k divides l iff l/k is Integer); theorem :: WSIERP_1:18 a<=b-c implies a<=b & c <=b; reserve fs,fs1,fs2,fs3 for FinSequence; reserve D for non empty set, v,v1,v2,v3 for object, fp for FinSequence of NAT, fr,fr1,fr2 for FinSequence of INT, ft for FinSequence of REAL; registration let fr; cluster Product fr -> integer; end; definition let fp; redefine func Sum(fp) -> Element of NAT; end; definition let fp; redefine func Product fp -> Element of NAT; end; definition let a be Nat,fs; redefine func Del (fs,a) means :: WSIERP_1:def 1 it = fs if not a in dom fs otherwise len it + 1 = len fs & for b holds (b=a implies it.b = fs.(b+1)); end; definition let D; let a be Nat; let fs be FinSequence of D; redefine func Del(fs,a) -> FinSequence of D; end; definition let D; let D1 be non empty Subset of D; let a be Nat; let fs be FinSequence of D1; redefine func Del(fs,a) -> FinSequence of D1; end; theorem :: WSIERP_1:19 Del(<*v1*>,1) = {} & Del(<*v1,v2*>,1) = <*v2*> & Del(<*v1,v2*>,2) = <* v1 *> & Del(<*v1,v2,v3*>,1) = <*v2,v3*> & Del(<*v1,v2,v3*>,2) = <*v1,v3*> & Del (<*v1,v2,v3*>,3) = <*v1,v2*>; theorem :: WSIERP_1:20 a in dom ft implies Sum Del(ft,a)+(ft.a)=Sum(ft); theorem :: WSIERP_1:21 a in dom fp implies Product(fp)/fp.a is Element of NAT; theorem :: WSIERP_1:22 numerator(q),denominator(q) are_coprime; theorem :: WSIERP_1:23 q=k/a & a<>0 & k,a are_coprime implies k=numerator(q) & a= denominator(q); theorem :: WSIERP_1:24 (ex q st a=q|^b) implies ex k st a=k|^b; theorem :: WSIERP_1:25 (ex q st a=q|^d) implies ex b st a=b|^d; theorem :: WSIERP_1:26 e>0 & (a|^e) divides (b|^e) implies a divides b; theorem :: WSIERP_1:27 ex m,n st a gcd b = a*m+b*n; theorem :: WSIERP_1:28 ex m1,n1 st m gcd n = m*m1+n*n1; theorem :: WSIERP_1:29 m divides n*k & m gcd n=1 implies m divides k; theorem :: WSIERP_1:30 for a,b,c being Nat holds a gcd b=1 & a divides b*c implies a divides c; theorem :: WSIERP_1:31 a<>0 & b<>0 implies ex c,d st a gcd b=a*c-b*d; theorem :: WSIERP_1:32 f>0 & g>0 & (f gcd g)=1 & a|^f=b|^g implies ex e st a=e|^g & b=e|^f; reserve x,y,t for Integer; theorem :: WSIERP_1:33 (ex x,y st m*x+n*y=k) iff (m gcd n) divides k; theorem :: WSIERP_1:34 m<>0 & n<>0 & m*m1+n*n1=k implies for x,y st m*x+n*y=k ex t st x=m1+t* (n/(m gcd n)) & y=n1-t*(m/(m gcd n)); theorem :: WSIERP_1:35 a gcd b=1 & a*b=c|^d implies ex e,f st a=e|^d & b=f|^d; :: Chinese remainder theorem ::\$N Chinese Remainder Theorem theorem :: WSIERP_1:36 for d holds (for a st a in dom fp holds fp.a gcd d=1) implies Product(fp) gcd d = 1; theorem :: WSIERP_1: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) implies for fr st len fr=len fp holds ex fr1 st (len fr1=len fp & for b st b in dom fp holds (fp.b)*(fr1.b)+(fr.b)=(fp.1)*(fr1.1)+(fr.1)); ::\$N Thue Theorem theorem :: WSIERP_1:38 a<>0 & a gcd k=1 implies ex b,e st 0<>b & 0<>e & b<=sqrt a & e<=sqrt a & (a divides (k*b+e) or a divides (k*b-e)); theorem :: WSIERP_1:39 dom Del(fs,a) c= dom fs; theorem :: WSIERP_1:40 Del (<*v*>^fs, 1) = fs & Del (fs^<*v*>, len fs + 1) = fs; begin :: Addenda :: from JORDAN1D, 2007.07.27, A.T. reserve n for Nat; theorem :: WSIERP_1:41 n > 0 & k mod n <> 0 implies - (k div n) = (-k) div n + 1; theorem :: WSIERP_1:42 k mod n = 0 implies - (k div n) = (-k) div n; reserve i1,i2,i3 for Integer; theorem :: WSIERP_1:43 ::: INT_4:14 i1,i2 are_congruent_mod i3 implies i1 gcd i3 = i2 gcd i3;