:: Modular Integer Arithmetic
:: by Christoph Schwarzweller
::
:: Received May 13, 2008
:: Copyright (c) 2008-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, 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;