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