:: Divisibility of Natural Numbers
::  by Grzegorz Bancerek
::
:: Received January 3, 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, NAT_1, INT_1, RELAT_1, ARYTM_3, CARD_1, XXREAL_0,
      SUBSET_1, ARYTM_1, INT_2, COMPLEX1, ZFMISC_1, XBOOLE_0, FINSET_1,
      ORDINAL1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, FINSET_1,
      NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, INT_1, NAT_1, INT_2;
 constructors XXREAL_0, NAT_1, INT_2, REAL_1, FINSET_1, CARD_1;
 registrations XXREAL_0, XREAL_0, NAT_1, INT_1, ORDINAL1, CARD_1;
 requirements REAL, NUMERALS, SUBSET, ARITHM;


begin

reserve a,b,p,k,l,m,n,s,h,i,j,t,i1,i2 for natural Number;

definition
  let k,l be natural Number;
  redefine func k div l -> Nat means
:: NAT_D:def 1       :: the exact division

  ( ex t being Nat st k = l * it + t & t < l ) or it = 0 & l = 0;
end;

definition
  let k,l be natural Number;
  redefine func k mod l -> Nat means
:: NAT_D:def 2         :: the rest of division

  ( ex t being Nat st k = l * t + it & it < l ) or it = 0 & l = 0;
end;

definition
  let k,l be Nat;
  redefine func k div l -> Element of NAT;
  redefine func k mod l -> Element of NAT;
end;

theorem :: NAT_D:1
  0 < i implies j mod i < i;

theorem :: NAT_D:2
  0 < i implies j = i * (j div i) + (j mod i);

:: The divisibility relation

definition
  let k,l be natural Number;
  redefine pred k divides l means
:: NAT_D:def 3
  ex t being Nat st l = k * t;
  reflexivity;
end;

theorem :: NAT_D:3
  j divides i iff i = j * (i div j);

theorem :: NAT_D:4
  i divides j & j divides h implies i divides h;

theorem :: NAT_D:5
  i divides j & j divides i implies i = j;

theorem :: NAT_D:6
  i divides 0 & 1 divides i;

theorem :: NAT_D:7
  0 < j & i divides j implies i <= j;

theorem :: NAT_D:8
  i divides j & i divides h implies i divides j+h;

theorem :: NAT_D:9
  i divides j implies i divides j * h;

theorem :: NAT_D:10
  i divides j & i divides j + h implies i divides h;

theorem :: NAT_D:11
  i divides j & i divides h implies i divides j mod h;

:: The least common multiple and the greatest common divisor

definition
  let k,n be natural Number;
  redefine func k lcm n means
:: NAT_D:def 4

  k divides it & n divides it &
  for m being Nat st k divides m & n divides m holds it divides m;
end;

definition
  let k,n be Nat;
  redefine func k lcm n -> Element of NAT;
end;

definition
  let k,n be natural Number;
  redefine func k gcd n means
:: NAT_D:def 5

  it divides k & it divides n &
  for m being Nat st m divides k & m divides n holds m divides it;
end;

definition
  let k,n be Nat;
  redefine func k gcd n -> Element of NAT;
end;

::$N Correctness of Euclid's Algorithm
::$N Greatest Common Divisor Algorithm
scheme :: NAT_D:sch 1
 Euklides { Q(Nat)->Nat, a,b()->Nat } :
  ex n being Nat st Q(n) = a() gcd b() & Q(n + 1) = 0
provided
 0 < b() & b() < a() and
 Q(0) = a() & Q(1) = b() and
 for n being Nat holds Q(n + 2) = Q(n) mod Q(n + 1);

theorem :: NAT_D:12
  n mod 2 = 0 or n mod 2 = 1;

theorem :: NAT_D:13
  (k * n) mod k = 0;

theorem :: NAT_D:14
  k > 1 implies 1 mod k = 1;

theorem :: NAT_D:15
  k mod n = 0 & l = k - m * n implies l mod n = 0;

theorem :: NAT_D:16
  n <> 0 & k mod n = 0 & l < n implies k + l mod n = l;

theorem :: NAT_D:17
  k mod n = 0 implies k + l mod n = l mod n;

theorem :: NAT_D:18
  k <> 0 implies (k * n) div k = n;

theorem :: NAT_D:19
  k mod n = 0 implies (k + l) div n = (k div n) + (l div n);

begin :: Addenda

::$CT

:: from GR_CY_1, 2005.11.16, A.T.

theorem :: NAT_D:21
  m mod n = (n*k + m) mod n;

theorem :: NAT_D:22
  (p+s) mod n = ((p mod n)+s) mod n;

theorem :: NAT_D:23
  (p+s) mod n = (p + ( s mod n)) mod n;

theorem :: NAT_D:24
  k < n implies k mod n = k;

theorem :: NAT_D:25
  n mod n = 0;

theorem :: NAT_D:26
  0 = 0 mod n;

:: from JORDAN4

theorem :: NAT_D:27
  i < j implies i div j = 0;

:: Moved from SCMP_GCD by AK on 28.12.2006

theorem :: NAT_D:28
  m > 0 implies n gcd m = m gcd (n mod m);

:: from AMI_3, 2007.06.14, A.T.

scheme :: NAT_D:sch 2
 INDI{ k,n() -> Element of NAT, P[set] }: P[n()]
provided
 P[0] and
 k() > 0 and
 for i,j being Nat st P[k()*i] & j <> 0 & j <= k() holds P[k()*i+j];

:: moved from INT_2, 2007.11.7, A.T,

theorem :: NAT_D:29
  i*j = (i lcm j)*(i gcd j);

:: from from SCMP_GCD, 2007.07.26, A.T.

theorem :: NAT_D:30
  for i,j being Integer st i>=0 & j>0 holds i gcd j= j gcd (i mod j);

:: ???, 2007.07.26, A.T.

theorem :: NAT_D:31
  i lcm i = i;

theorem :: NAT_D:32
  i gcd i = i;

:: from SCMPDS_9. 2008.05.06, A.T.

theorem :: NAT_D:33
  i < j & i <> 0 implies i/j is not integer;

:: from BINARITH, 2008.08.18, A.T.

definition
  let i,j be Nat;
  redefine func i -' j -> Element of NAT;
end;

theorem :: NAT_D:34
  i + j -' j = i;

theorem :: NAT_D:35
  a -' b <= a;

theorem :: NAT_D:36
  n-'i=0 implies n<=i;

theorem :: NAT_D:37
  i<=j implies j+k-'i=j+k-i;

theorem :: NAT_D:38
  i<=j implies j+k-'i=j-'i+k;

theorem :: NAT_D:39
  i-'i1>=1 or i-i1>=1 implies i-'i1=i-i1;

theorem :: NAT_D:40
  n-'0=n;

theorem :: NAT_D:41
  i1<=i2 implies n-'i2<=n-'i1;

theorem :: NAT_D:42
  i1<=i2 implies i1-'n<=i2-'n;

theorem :: NAT_D:43
  i-'i1>=1 or i-i1>=1 implies i-'i1+i1=i;

theorem :: NAT_D:44
  i1<=i2 implies i1-'1<=i2;

theorem :: NAT_D:45
  i-'2=i-'1-'1;

theorem :: NAT_D:46
  i1+1<=i2 implies i1-'1<i2 & i1-'2<i2 & i1<=i2;

theorem :: NAT_D:47
  i1+2<=i2 or i1+1+1<=i2 implies i1+1<i2 & i1+1-'1<i2 & i1+1-'2<i2 & i1+1<=i2 &
  i1-'1+1<i2 & i1-'1+1-'1<i2 & i1<i2 & i1-'1<i2 & i1-'2<i2 & i1<=i2;

theorem :: NAT_D:48
  i1<=i2 or i1<=i2-'1 implies
  i1<i2+1 & i1<=i2+1 & i1<i2+1+1 & i1<=i2+1+1 & i1<i2+2 & i1<=i2+2;

theorem :: NAT_D:49
  i1<i2 or i1+1<=i2 implies i1<=i2-'1;

theorem :: NAT_D:50
  i>=i1 implies i>=i1-'i2;

theorem :: NAT_D:51
  1<=i & 1<=i1-'i implies i1-'i<i1;

theorem :: NAT_D:52
  i-'k <= j implies i <= j + k;

theorem :: NAT_D:53
  i <= j + k implies i-'k <= j;

theorem :: NAT_D:54
  i <= j -' k & k <= j implies i + k <= j;

theorem :: NAT_D:55
  j + k <= i implies k <= i -' j;

theorem :: NAT_D:56
  k <= i & i < j implies i -' k < j -' k;

theorem :: NAT_D:57
  i < j & k < j implies i -' k < j -' k;

:: form JCT_MISC, 2008.08.21, A.T.

theorem :: NAT_D:58
  i <= j implies j-'(j-'i) = i;

:: from LEXBFS, 2008.08.23, A.T.

theorem :: NAT_D:59
  n < k implies k -' (n+1) + 1 = k -' n;

theorem :: NAT_D:60
  for A being finite set holds A is trivial iff card A < 2;

:: from INT_3, 2011.04.28, A.T.

theorem :: NAT_D:61
  for n,a,k being Integer holds (n <> 0 implies (a + n * k) div n =
  (a div n) + k) & (a + n * k) mod n = a mod n;

theorem :: NAT_D:62
  for n being natural Number st n > 0 for a being Integer holds
  a mod n >= 0 & a mod n < n;

theorem :: NAT_D:63
  for n,a being Integer holds (0 <= a & a < n implies a mod n = a)
  & (0 > a & a >= -n implies a mod n = n + a);

theorem :: NAT_D:64
  for n,a,b being Integer holds (n <> 0 & a mod n = b mod n
implies a,b are_congruent_mod n) & (a,b are_congruent_mod n implies a mod n = b
  mod n);

theorem :: NAT_D:65
  for n being natural Number, a being Integer holds (a mod n) mod n = a mod n;

theorem :: NAT_D:66
  for n,a,b being Integer holds (a + b) mod n = ((a mod n) + (b mod n)) mod n;

theorem :: NAT_D:67
  for n,a,b being Integer holds (a * b) mod n = ((a mod n) * (b mod n)) mod n;

::$N Bezout's identity
::$N Bezout's lemma

theorem :: NAT_D:68
  for a,b being Integer ex s,t being Integer st a gcd b = s * a + t * b;

:: from RADIX_1, 2011.07.31, A.T.

theorem :: NAT_D:69
  n mod k = k - 1 implies (n+1) mod k = 0;

theorem :: NAT_D:70
  n mod k < k - 1 implies (n+1) mod k = (n mod k) + 1;

theorem :: NAT_D:71
  for i being Integer, n being Nat holds (i*n) mod n = 0;

theorem :: NAT_D:72 :: NAT_D:43
  m-n >= 0 implies m-'n+n = m;