:: Modular Integer Arithmetic :: by Christoph Schwarzweller :: :: Received May 13, 2008 :: Copyright (c) 2008-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, FINSEQ_1, RELAT_1, TARSKI, VALUED_0, ORDINAL1, RFINSEQ, XXREAL_0, ARYTM_1, SUBSET_1, FUNCT_1, ARYTM_3, INT_1, ORDINAL4, XBOOLE_0, NAT_1, VALUED_1, CARD_3, BINOP_2, SETWISEO, BINOP_1, SETWOP_2, CARD_1, FINSOP_1, PARTFUN1, COMPLEX1, INT_2, PARTFUN3, INT_6, REAL_1; notations TARSKI, XBOOLE_0, SUBSET_1, INT_1, INT_2, ORDINAL1, NUMBERS, RELAT_1, PARTFUN1, PARTFUN3, XXREAL_0, XREAL_0, FUNCT_1, VALUED_0, VALUED_1, BINOP_2, SETWISEO, RFINSEQ, BINOP_1, FINSEQ_1, SETWOP_2, RVSUM_1, XCMPLX_0, NAT_1, FINSOP_1; constructors FINSOP_1, RFINSEQ, INT_2, BINOP_2, REAL_1, SETWISEO, SETWOP_2, PARTFUN3, XXREAL_0, RVSUM_1, BINOP_1, RELSET_1; registrations NUMBERS, XREAL_0, NAT_1, INT_1, RELAT_1, FINSEQ_1, RVSUM_1, XBOOLE_0, MEMBERED, BINOP_2, ORDINAL1, XXREAL_0, VALUED_0, VALUED_1, FUNCT_1, CARD_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin registration let f be complex-valued FinSequence, n be Nat; cluster f|n -> complex-valued; end; registration let f be INT-valued FinSequence, n be Nat; cluster f|n -> INT-valued; end; registration let f be INT-valued FinSequence, n be Nat; cluster f/^n -> INT-valued; end; registration let i be Integer; cluster <*i*> -> INT-valued; end; registration let f,g be INT-valued FinSequence; cluster f ^ g -> INT-valued; end; theorem :: INT_6:1 for f1,f2 being complex-valued FinSequence holds len(f1 + f2) = min(len f1, len f2); theorem :: INT_6:2 for f1, f2 being complex-valued FinSequence holds len(f1 - f2) = min(len f1, len f2); theorem :: INT_6:3 for f1,f2 being complex-valued FinSequence holds len(f1 (#) f2) = min(len f1, len f2); theorem :: INT_6:4 for m1,m2 being complex-valued FinSequence st len m1 = len m2 for k being Nat st k <= len m1 holds (m1(#)m2)|k = (m1|k) (#) (m2|k); registration let F be INT-valued FinSequence; cluster Sum F -> integer; cluster Product F -> integer; end; theorem :: INT_6:5 for f being complex-valued FinSequence, i being Nat st i+1 <= len f holds f|i ^ <*f.(i+1)*> = f|(i+1); theorem :: INT_6:6 for f being complex-valued FinSequence st ex i being Nat st i in dom f & f.i = 0 holds Product(f) = 0; theorem :: INT_6:7 for n,a,b being Integer holds (a - b) mod n = ((a mod n) - (b mod n)) mod n; theorem :: INT_6:8 for i,j,k being Integer st i divides j holds k*i divides k*j; theorem :: INT_6:9 for m being INT-valued FinSequence, i being Nat st i in dom m & m.i <> 0 holds Product(m) / m.i is Integer; theorem :: INT_6:10 for m being INT-valued FinSequence, i being Nat st i in dom m ex z being Integer st z * m.i = Product(m); theorem :: INT_6:11 for m being INT-valued FinSequence, i,j being Nat st i in dom m & j in dom m & j <> i & m.j <> 0 holds Product(m) / (m.i * m.j) is Integer; theorem :: INT_6:12 for m being INT-valued FinSequence, i,j being Nat st i in dom m & j in dom m & j <> i & m.j <> 0 ex z being Integer st z * m.i = Product(m) / m.j; begin :: More on Greatest Common Divisors theorem :: INT_6:13 for i being Integer holds |.i.| divides i & i divides |.i.|; theorem :: INT_6:14 for i,j being Integer holds i gcd j = i gcd |.j.|; theorem :: INT_6:15 for i,j being Integer st i,j are_coprime holds i lcm j = |.i * j.|; theorem :: INT_6:16 for i,j,k being Integer holds (i*j) gcd (i*k) = |.i.| * (j gcd k); theorem :: INT_6:17 for i,j being Integer holds (i * j) gcd i = |.i.|; theorem :: INT_6:18 for i,j,k being Integer holds i gcd (j gcd k) = (i gcd j) gcd k; theorem :: INT_6:19 for i,j,k being Integer st i,j are_coprime holds i gcd (j * k) = i gcd k; theorem :: INT_6:20 for i,j being Integer st i,j are_coprime holds i * j divides i lcm j; theorem :: INT_6:21 for x,y,i,j being Integer st i,j are_coprime holds x,y are_congruent_mod i & x,y are_congruent_mod j implies x,y are_congruent_mod i*j ; theorem :: INT_6:22 for i,j being Integer st i,j are_coprime holds ex s being Integer st s*i,1 are_congruent_mod j; begin :: Chinese Remainder Sequences notation let f be INT-valued FinSequence; antonym f is multiplicative-trivial for f is non-empty; end; definition let f be INT-valued FinSequence; redefine attr f is multiplicative-trivial means :: INT_6:def 1 ex i being Nat st i in dom f & f.i = 0; end; registration cluster multiplicative-trivial for INT-valued FinSequence; cluster non multiplicative-trivial for INT-valued FinSequence; cluster non empty positive-yielding for INT-valued FinSequence; end; theorem :: INT_6:23 for m being multiplicative-trivial INT-valued FinSequence holds Product(m) = 0; definition let f be INT-valued FinSequence; attr f is Chinese_Remainder means :: INT_6:def 2 for i,j being Nat st i in dom f & j in dom f & i <> j holds f.i, f.j are_coprime; end; registration cluster non empty positive-yielding Chinese_Remainder for INT-valued FinSequence; end; definition mode CR_Sequence is non empty positive-yielding Chinese_Remainder INT-valued FinSequence; end; registration cluster -> non multiplicative-trivial for CR_Sequence; end; registration cluster multiplicative-trivial -> non empty for INT-valued FinSequence; end; theorem :: INT_6:24 for f being CR_Sequence, m being Nat st 0 < m & m <= len f holds f|m is CR_Sequence; registration let m be CR_Sequence; cluster Product(m) -> positive natural; end; theorem :: INT_6:25 for m being CR_Sequence, i being Nat st i in dom m for mm being Integer st mm = Product(m) / m.i holds mm, m.i are_coprime; begin :: Integer Arithmetic based on CRT definition let u be Integer, m be INT-valued FinSequence; func mod(u,m) -> FinSequence means :: INT_6:def 3 len it = len m & for i being Nat st i in dom it holds it.i = u mod m.i; end; registration let u be Integer, m be INT-valued FinSequence; cluster mod(u,m) -> INT-valued; end; definition let m be CR_Sequence; mode CR_coefficients of m -> FinSequence means :: INT_6:def 4 len it = len m & for i being Nat st i in dom it holds ex s being Integer, mm being Integer st mm = Product(m) / m.i & s * mm, 1 are_congruent_mod m.i & it.i = s * ( Product(m) / m.i); end; registration let m be CR_Sequence; cluster -> INT-valued for CR_coefficients of m; end; theorem :: INT_6:26 for m being CR_Sequence, c being CR_coefficients of m, i being Nat st i in dom c holds c.i,1 are_congruent_mod m.i; theorem :: INT_6:27 for m being CR_Sequence, c being CR_coefficients of m, i,j being Nat st i in dom c & j in dom c & i <> j holds c.i,0 are_congruent_mod m.j; theorem :: INT_6:28 for m being CR_Sequence, c1,c2 being CR_coefficients of m, i being Nat st i in dom c1 holds c1.i,c2.i are_congruent_mod m.i; theorem :: INT_6:29 for u being INT-valued FinSequence, m being CR_Sequence st len m = len u for c being CR_coefficients of m, i being Nat st i in dom m holds Sum(u(#)c),u.i are_congruent_mod m.i; theorem :: INT_6:30 for u being INT-valued FinSequence, m being CR_Sequence st len m = len u for c1,c2 being CR_coefficients of m holds Sum(u(#)c1),Sum(u(#)c2 ) are_congruent_mod Product(m); definition let u be INT-valued FinSequence, m be CR_Sequence such that len m = len u; func to_int(u,m) -> Integer means :: INT_6:def 5 for c being CR_coefficients of m holds it = Sum(u(#)c) mod Product(m); end; theorem :: INT_6:31 for u being INT-valued FinSequence, m being CR_Sequence st len m = len u holds 0 <= to_int(u,m) & to_int(u,m) < Product(m); theorem :: INT_6:32 for u being Integer, m being CR_Sequence, i being Nat st i in dom m holds u, mod(u,m).i are_congruent_mod m.i; theorem :: INT_6:33 for u,v being Integer, m being CR_Sequence, i being Nat st i in dom m holds (mod(u,m) + mod(v,m)).i, u + v are_congruent_mod m.i; theorem :: INT_6:34 for u,v being Integer, m being CR_Sequence, i being Nat st i in dom m holds (mod(u,m) (#) mod(v,m)).i, u * v are_congruent_mod m.i; theorem :: INT_6:35 for u,v being Integer, m being CR_Sequence, i being Nat st i in dom m holds to_int(mod(u,m) + mod(v,m),m), u + v are_congruent_mod m.i; theorem :: INT_6:36 for u,v being Integer, m being CR_Sequence, i being Nat st i in dom m holds to_int(mod(u,m) - mod(v,m),m), u - v are_congruent_mod m.i; theorem :: INT_6:37 for u,v being Integer, m being CR_Sequence, i being Nat st i in dom m holds to_int(mod(u,m) (#) mod(v,m),m), u * v are_congruent_mod m.i; theorem :: INT_6:38 for u,v being Integer, m being CR_Sequence st 0 <= u + v & u + v < Product(m) holds to_int(mod(u,m) + mod(v,m), m) = u + v; theorem :: INT_6:39 for u,v being Integer, m being CR_Sequence st 0 <= u - v & u - v < Product(m) holds to_int(mod(u,m) - mod(v,m), m) = u - v; theorem :: INT_6:40 for u,v being Integer, m being CR_Sequence st 0 <= u * v & u * v < Product(m) holds to_int(mod(u,m) (#) mod(v,m), m) = u * v; begin :: Chinese Remainder Theorem Revisited theorem :: INT_6:41 for u being INT-valued FinSequence, m being CR_Sequence st len u = len m ex z being Integer st 0 <= z & z < Product(m) & for i being Nat st i in dom u holds z,u.i are_congruent_mod m.i; theorem :: INT_6:42 for u being INT-valued FinSequence, m being CR_Sequence for z1,z2 being Integer st 0 <= z1 & z1 < Product(m) & (for i being Nat st i in dom m holds z1,u.i are_congruent_mod m.i) & 0 <= z2 & z2 < Product(m) & (for i being Nat st i in dom m holds z2,u.i are_congruent_mod m.i) holds z1 = z2;