:: Divisibility of Natural Numbers
::  by Grzegorz Bancerek
::
:: Received January 3, 2007
:: Copyright (c) 2007-2012 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;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, FINSET_1,
      NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_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, XBOOLE_0, CARD_1,
      ZFMISC_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 theorems ORDINAL1, XCMPLX_1, XREAL_1, XXREAL_0, NAT_1, INT_1, INT_2, ABSVALUE,
      XREAL_0, CARD_1, ZFMISC_1, COMPLEX1, XCMPLX_0, TARSKI;
 schemes NAT_1;

begin

reserve p,k,l,m,n,s,h,i,j,t for Nat;

:: Exact division and rest of division

Lm1: now
  let k,l;
  k div l in NAT by INT_1:3,55;
  hence k div l is Nat;
end;

Lm2: now
  let k,l;
  k mod l in NAT by INT_1:3,57;
  hence k mod l is Nat;
end;

definition
  let k,l be Nat;
  redefine func k div l -> Nat means       :: the exact division
  :Def1:
  ( ex t being Nat st k = l * it + t & t < l ) or it = 0 & l = 0;
  compatibility
  proof
    let r be Nat;
    per cases;
    suppose l = 0;
      hence thesis by INT_1:48;
    end;
    suppose
A1:   l > 0;
      then
A2:   k = l * (k div l) + (k mod l) by INT_1:59;
A3:   k mod l is Nat by Lm2;
      hence r = k div l implies
      (ex t being Nat st k = l * r + t & t < l) or r = 0 & l = 0
      by A1,A2,INT_1:58;
      assume
A4:   ( ex t being Nat st k = l * r + t & t < l ) or r = 0 & l = 0;
A5:   k mod l < l by A1,INT_1:58;
      k div l is Nat by Lm1;
      hence thesis by A2,A3,A4,A5,NAT_1:18;
    end;
  end;
  coherence by Lm1;
end;

definition
  let k,l be Nat;
  redefine func k mod l -> Nat means         :: the rest of division
  :Def2:
  ( ex t being Nat st k = l * t + it & it < l ) or it = 0 & l = 0;
  compatibility
  proof
    let r be Nat;
    per cases;
    suppose l = 0;
      hence thesis by INT_1:def 10;
    end;
    suppose
A1:   l > 0;
      then
A2:   k = l * (k div l) + (k mod l) by INT_1:59;
      hence r = k mod l implies
      ( ex t being Nat st k = l * t + r & r < l ) or r = 0 & l = 0
      by A1,INT_1:58;
      assume
A3:   ( ex t being Nat st k = l * t + r & r < l ) or r = 0 & l = 0;
A4:   k mod l < l by A1,INT_1:58;
      k mod l is Nat by Lm2;
      hence thesis by A2,A3,A4,NAT_1:18;
    end;
  end;
  coherence by Lm2;
end;

definition
  let k,l be Nat;
  redefine func k div l -> Element of NAT;
  coherence
  proof
    k div l is Nat;
    hence thesis by ORDINAL1:def 12;
  end;
  redefine func k mod l -> Element of NAT;
  coherence
  proof
    k mod l is Nat;
    hence thesis by ORDINAL1:def 12;
  end;
end;

theorem Th1:
  0 < i implies j mod i < i
proof
  assume 0 < i;
  then ex t being Nat st j = i * t + (j mod i) & j mod i < i by Def2;
  hence thesis;
end;

theorem
  0 < i implies j = i * (j div i) + (j mod i) by INT_1:59;

:: The divisibility relation

definition
  let k,l be Nat;
  redefine pred k divides l means
  :Def3:
  ex t being Nat st l = k * t;
  compatibility
  proof
    hereby
      assume
A1:   k divides l;
      thus ex t being Nat st l = k * t
      proof
        consider t being Integer such that
A2:     l = k * t by A1,INT_1:def 3;
        per cases;
        suppose 0 < l;
          then 0 <= t by A2;
          then reconsider t as Element of NAT by INT_1:3;
          take t;
          thus l = k * t by A2;
        end;
        suppose
A3:       l = 0;
          take 0;
          thus l = k*0 by A3;
        end;
      end;
    end;
    assume ex t being Nat st l = k * t;
    hence thesis by INT_1:def 3;
  end;
  reflexivity
  proof
    let i;
    i = i * 1;
    hence thesis;
  end;
end;

theorem Th3:
  j divides i iff i = j * (i div j)
proof
  thus j divides i implies i = j * (i div j)
  proof
    assume j divides i;
    then consider k being Nat such that
A1: i = j * k by Def3;
A2: i = j * k + 0 by A1;
    now
      assume
A3:   j <> 0;
      then
A4:   i = j * (i div j) + (i mod j) by INT_1:59;
      i mod j < j by A3,Th1;
      hence thesis by A2,A4,NAT_1:18;
    end;
    hence thesis by A1;
  end;
  assume i = j * (i div j);
  hence thesis by Def3;
end;

theorem
  i divides j & j divides h implies i divides h
proof
  assume that
A1: i divides j and
A2: j divides h;
A3: j = i * (j div i) by A1,Th3;
  h = j * (h div j) by A2,Th3;
  then h = i * ((j div i)*(h div j)) by A3;
  hence thesis by Def3;
end;

theorem Th5:
  i divides j & j divides i implies i = j
proof
  assume that
A1: i divides j and
A2: j divides i;
A3: j = i * (j div i) by A1,Th3;
  i = j * (i div j) by A2,Th3;
  then
A4: i*1 = i * (j div i) * (i div j) by A3
    .= i * ((j div i) * (i div j));
A5: i = 0 implies i = j by A3;
  (j div i) * (i div j) = 1 implies i = j
  proof
    assume (j div i) * (i div j) = 1;
    then j div i = 1 by NAT_1:15;
    hence thesis by A3;
  end;
  hence thesis by A4,A5,XCMPLX_1:5;
end;

theorem Th6:
  i divides 0 & 1 divides i
proof
  0 = i * 0;
  hence i divides 0 by Def3;
  i = i * 1;
  hence thesis by Def3;
end;

theorem
  0 < j & i divides j implies i <= j
proof
  assume that
A1: 0 < j and
A2: i divides j;
A3: j = i * (j div i) by A2,Th3;
  then j div i <> 0 by A1;
  then consider m such that
A4: j div i = m + 1 by NAT_1:6;
  i * (m + 1) = i + i * m;
  hence thesis by A3,A4,NAT_1:11;
end;

theorem Th8:
  i divides j & i divides h implies i divides j+h
proof
  assume that
A1: i divides j and
A2: i divides h;
A3: j = i * (j div i) by A1,Th3;
  h = i * (h div i) by A2,Th3;
  then j + h = i * ((j div i) + (h div i)) by A3;
  hence thesis by Def3;
end;

theorem Th9:
  i divides j implies i divides j * h
proof
  assume i divides j;
  then consider l being Nat such that
A1: j = i * l by Def3;
  i * l * h = i * (l * h);
  hence thesis by A1,Def3;
end;

theorem Th10:
  i divides j & i divides j + h implies i divides h
proof
  assume that
A1: i divides j and
A2: i divides j + h;
  consider t being Nat such that
A3: j + h = i * t by A2,Def3;
  consider u being Nat such that
A4: j = i * u by A1,Def3;
  now
    assume
A5: i <> 0;
    then
A6: h = i * (h div i) + (h mod i) by INT_1:59;
A7: j + (i * (h div i) + (h mod i)) = i * (u + (h div i)) + (h mod i) by A4;
A8: h mod i < i by A5,Th1;
    j + h = i * t + 0 by A3;
    then h mod i = 0 by A6,A7,A8,NAT_1:18;
    hence thesis by A6,Th3;
  end;
  hence thesis by A3;
end;

theorem Th11:
  i divides j & i divides h implies i divides j mod h
proof
  assume that
A1: i divides j and
A2: i divides h;
A3: now
    assume h = 0;
    then j mod h = 0 by Def2;
    hence thesis by Th6;
  end;
  now
    assume h <> 0;
    then
A4: j = h * (j div h) + (j mod h) by INT_1:59;
    i divides h * (j div h) by A2,Th9;
    hence thesis by A1,A4,Th10;
  end;
  hence thesis by A3;
end;

:: The least common multiple and the greatest common divisor

definition
  let k,n be Nat;
  redefine func k lcm n means
  :Def4:
  k divides it & n divides it &
  for m being Nat st k divides m & n divides m holds it divides m;
  compatibility
  proof
    let IT be Nat;
    thus IT = k lcm n implies k divides IT & n divides IT &
    for m being Nat st k divides m & n divides m holds IT divides m
    by INT_2:def 1;
    assume that
A1: k divides IT and
A2: n divides IT and
A3: for m being Nat st k divides m & n divides m holds IT divides m;
    for m being Integer st k divides m & n divides m holds IT divides m
    proof
      let m be Integer;
      m in INT by INT_1:def 2;
      then consider i being Element of NAT such that
A4:   m = i or m = -i by INT_1:def 1;
      assume that
A5:   k divides m and
A6:   n divides m;
A7:   k divides i by A4,A5,INT_2:10;
      n divides i by A4,A6,INT_2:10;
      then IT divides i by A3,A7;
      hence thesis by A4,INT_2:10;
    end;
    hence thesis by A1,A2,INT_2:def 1;
  end;
end;

definition
  let k,n be Nat;
  redefine func k lcm n -> Element of NAT;
  coherence by ORDINAL1:def 12;
end;

definition
  let k,n be Nat;
  redefine func k gcd n means
  :Def5:
  it divides k & it divides n &
  for m being Nat st m divides k & m divides n holds m divides it;
  compatibility
  proof
    let IT be Nat;
    thus IT = k gcd n implies IT divides k & IT divides n &
    for m being Nat st m divides k & m divides n holds m divides IT
    by INT_2:def 2;
    assume that
A1: IT divides k and
A2: IT divides n and
A3: for m being Nat st m divides k & m divides n holds m divides IT;
    for m being Integer st m divides k & m divides n holds m divides IT
    proof
      let m be Integer;
      m in INT by INT_1:def 2;
      then consider i being Element of NAT such that
A4:   m = i or m = -i by INT_1:def 1;
      assume that
A5:   m divides k and
A6:   m divides n;
A7:   i divides k by A4,A5,INT_2:10;
      i divides n by A4,A6,INT_2:10;
      then i divides IT by A3,A7;
      hence thesis by A4,INT_2:10;
    end;
    hence thesis by A1,A2,INT_2:def 2;
  end;
end;

definition
  let k,n be Nat;
  redefine func k gcd n -> Element of NAT;
  coherence by ORDINAL1:def 12;
end;

::$N Correctness of Euclide Algorithm
::$N Greatest Common Divisor Algorithm
scheme Euklides { Q(Nat)->Nat, a,b()->Nat } :
  ex n being Element of NAT st Q(n) = a() gcd b() & Q(n + 1) = 0
provided
A1: 0 < b() & b() < a() and
A2: Q(0) = a() & Q(1) = b() and
A3: for n being Element of NAT holds Q(n + 2) = Q(n) mod Q(n + 1)
proof
  defpred P[Nat] means ex n being Element of NAT st $1 = Q(n);
A4: ex k being Nat st P[k] by A2;
A5: for k being Nat st k <> 0 & P[k] ex n being Nat st n < k & P[n]
  proof
    let k be Nat;
    assume that
A6: k <> 0 and
A7: ex n being Element of NAT st k = Q(n);
    consider n being Element of NAT such that
A8: k = Q(n) by A7;
    reconsider Q = Q(n+1) as Element of NAT by ORDINAL1:def 12;
A9: n = 0 implies Q < k by A1,A2,A8;
    now
      given m such that
A10:  n = m + 1;
      reconsider m1=m as Element of NAT by ORDINAL1:def 12;
      Q(m1 + 2) = Q(m1) mod Q(m1 + 1) by A3;
      hence Q(n + 1) < k by A6,A8,A10,Th1;
      take m = n + 1;
      thus Q(n + 1) =Q(m);
    end;
    hence thesis by A9,NAT_1:6;
  end;
A11: P[0] from NAT_1:sch 7(A4,A5);
  defpred Q[Nat] means 0 = Q($1);
A12: ex n being Nat st Q[n] by A11;
  consider k being Nat such that
A13: Q[k] & for n being Nat st Q[n] holds k <= n from NAT_1:sch 5(A12);
  consider n such that
A14: k = n + 1 by A1,A2,A13,NAT_1:6;
  reconsider n as Element of NAT by ORDINAL1:def 12;
  take n;
  defpred PP[Nat] means Q(n) divides Q($1) & Q(n) divides Q($1 + 1);
  PP[n] by A13,A14,Th6;
  then
A15: ex k being Nat st PP[k];
A16: for k being Nat st k <> 0 & PP[k] ex m being Nat st m < k & PP[m]
  proof
    let l be Nat;
    assume that
A17: l <> 0 and
A18: Q(n) divides Q(l) and
A19: Q(n) divides Q(l + 1);
    consider m such that
A20: l = m + 1 by A17,NAT_1:6;
    reconsider m as Element of NAT by ORDINAL1:def 12;
    take m;
A21: m <= m + 1 by NAT_1:11;
    m <> m + 1;
    hence m < l by A20,A21,XXREAL_0:1;
A22: now
      assume
A23:  Q(m + 1) = 0;
      now
        assume
A24:    m + 1 <> k;
        k <= m + 1 by A13,A23;
        then k < m + 1 by A24,XXREAL_0:1;
        then
A25:    k <= m by NAT_1:13;
        defpred Q[Nat] means k <= $1 implies Q($1) = 0;
A26:    Q[0] by A13;
A27:    for m st Q[m] holds Q[m+1]
        proof
          let m such that
A28:      k <= m implies Q(m) = 0 and
A29:      k <= m + 1;
          now
            assume k <> m + 1;
            then
A30:        k < m + 1 by A29,XXREAL_0:1;
            then consider l such that
A31:        m = l + 1 by A1,A2,A28,NAT_1:6,13;
            reconsider l as Element of NAT by ORDINAL1:def 12;
            Q(l + 2) = Q(l) mod Q(l + 1) by A3;
            hence thesis by A28,A30,A31,Def2,NAT_1:13;
          end;
          hence thesis by A13;
        end;
        for m holds Q[m] from NAT_1:sch 2(A26,A27);
        then Q(m) = 0 by A25;
        hence Q(n) divides Q(m) by Th6;
      end;
      hence Q(n) divides Q(m) by A14;
    end;
    now
      assume
A32:  Q(m + 1) <> 0;
      Q(m + 2) = Q(m) mod Q(m + 1) by A3;
      then
A33:  Q(m) = Q(m + 1) * (Q(m) div Q(m + 1)) + Q(m + 2) by A32,INT_1:59;
      Q(n) divides Q(m + 1) * (Q(m) div Q(m + 1)) by A18,A20,Th9;
      hence Q(n) divides Q(m) by A19,A20,A33,Th8;
    end;
    hence Q(n) divides Q(m) by A22;
    thus Q(n) divides Q(m + 1) by A18,A20;
  end;
  now
    PP[0] from NAT_1:sch 7(A15,A16);
    hence Q(n) divides a() & Q(n) divides b() by A2;
    let m;
    defpred P1[Nat] means m divides Q($1) & m divides Q($1 + 1);
    assume that
A34: m divides a() and
A35: m divides b();
A36: P1[0] by A2,A34,A35;
A37: for k be Element of NAT st P1[k] holds P1[k+1]
    proof
      let k be Element of NAT;
      assume that
A38:  m divides Q(k) and
A39:  m divides Q(k + 1);
      thus m divides Q(k + 1) by A39;
      Q(k + 2) = Q(k) mod Q(k + 1) by A3;
      hence m divides Q(k + 1 + 1) by A38,A39,Th11;
    end;
    for k be Element of NAT holds P1[k] from NAT_1:sch 1(A36,A37);
    hence m divides Q(n);
  end;
  hence Q(n) = a() gcd b() by Def5;
  thus thesis by A13,A14;
end;

theorem
  n mod 2 = 0 or n mod 2 = 1
proof
  assume
A1: n mod 2 <> 0;
A2: 2 = 1 + 1;
  n mod 2 < 2 by Th1;
  then
A3: n mod 2 <= 1 by A2,NAT_1:13;
  n mod 2 >= 1 by A1,NAT_1:14;
  hence thesis by A3,XXREAL_0:1;
end;

theorem
  (k * n) mod k = 0
proof
  per cases;
  suppose k = 0;
    hence thesis by Def2;
  end;
  suppose
A1: k <> 0;
    k * n = k * n + 0;
    hence thesis by A1,Def2;
  end;
end;

theorem
  k > 1 implies 1 mod k = 1
proof
  assume
A1: k > 1;
  1 = k * 0 + 1;
  hence thesis by A1,Def2;
end;

theorem
  k mod n = 0 & l = k - m * n implies l mod n = 0
proof
  assume that
A1: k mod n = 0 and
A2: l = k - m * n;
  per cases;
  suppose n = 0;
    hence thesis by A1,A2;
  end;
  suppose n <> 0;
    then consider t being Nat such that
A3: k = n * t + 0 and
A4: 0 < n by A1,Def2;
A5: l = n * (t - m) + 0 by A2,A3;
    now
      assume t < m + 0;
      then t - m < 0 by XREAL_1:19;
      then l < n * 0 by A4,A5,XREAL_1:68;
      hence contradiction;
    end;
    then t - m is Element of NAT by NAT_1:21;
    hence thesis by A4,A5,Def2;
  end;
end;

theorem
  n <> 0 & k mod n = 0 & l < n implies k + l mod n = l
proof
  assume that
A1: n <> 0 and
A2: k mod n = 0 and
A3: l < n;
  ex t being Nat st k = n * t + 0 & 0 < n by A1,A2,Def2;
  hence thesis by A3,Def2;
end;

theorem
  k mod n = 0 implies k + l mod n = l mod n
proof
  assume that
A1: k mod n = 0;
  per cases;
  suppose
A2: n = 0;
    hence k + l mod n = 0 by Def2
      .= l mod n by A2,Def2;
  end;
  suppose
A3: n <> 0;
    then consider m being Nat such that
A4: k = n * m + 0 and 0 < n by A1,Def2;
    consider t being Nat such that
A5: l = n * t + (l mod n) and
A6: l mod n < n by A3,Def2;
    k + l = n * (m + t) + (l mod n) by A4,A5;
    hence thesis by A6,Def2;
  end;
end;

theorem
  k <> 0 implies (k * n) div k = n
proof
  assume
A1: k <> 0;
  k * n = k * n + 0;
  hence thesis by A1,Def1;
end;

theorem
  k mod n = 0 implies (k + l) div n = (k div n) + (l div n)
proof
  assume
A1: k mod n = 0;
  per cases;
  suppose
A2: n <> 0;
    then
A3: k = n * (k div n) + 0 by A1,INT_1:59;
A4: ex t being Nat st l = n * t + (l mod n) & l mod n < n by A2,Def2;
    l = n * (l div n) + (l mod n) by A2,INT_1:59;
    then k + l = n * ((k div n) + (l div n)) + (l mod n) by A3;
    hence thesis by A4,Def1;
  end;
  suppose
A5: n = 0;
    then
A6: (k + l) div n = 0 by Def1;
    k div n = 0 by A5,Def1;
    hence thesis by A5,A6,Def1;
  end;
end;

begin :: Addenda
:: from AMI_5, 2005.11.16, A.T.

theorem
  k <> 0 implies m * k div k = m
proof
  assume k <> 0;
  then m*k = k * m + 0 & 0 < k or m = 0 & k = 0;
  hence thesis by Def1;
end;

:: from GR_CY_1, 2005.11.16, A.T.

theorem Th21:
  m mod n = (n*k + m) mod n
proof
  per cases;
  suppose
A1: n > 0;
    m mod n = t implies (n*k + m) mod n = t
    proof
      assume m mod n = t;
      then consider q being Nat such that
A2:   m = n * q + t and
A3:   t < n by A1,Def2;
      ex p st n*k + m = n*p + t & t < n
      proof
        reconsider p = k+q as Element of NAT by ORDINAL1:def 12;
        take p;
        thus thesis by A2,A3;
      end;
      hence thesis by Def2;
    end;
    hence thesis;
  end;
  suppose n = 0;
    hence thesis;
  end;
end;

theorem Th22:
  (p+s) mod n = ((p mod n)+s) mod n
proof
  per cases;
  suppose n > 0;
    then (p + s) mod n = (n*(p div n) + (p mod n) + s) mod n by INT_1:59
      .=(n*(p div n) + ((p mod n) + s)) mod n
      .=((p mod n) + s) mod n by Th21;
    hence thesis;
  end;
  suppose
A1: n = 0;
    hence (p+s) mod n = 0 by Def2
      .= ((p mod n)+s) mod n by A1,Def2;
  end;
end;

theorem
  (p+s) mod n = (p + ( s mod n)) mod n by Th22;

theorem Th24:
  k < n implies k mod n = k
proof
  assume
A1: k<n;
  k=n*0 + k;
  hence thesis by A1,Def2;
end;

theorem Th25:
  n mod n = 0
proof
  per cases;
  suppose
A1: n>0;
    n=n*1+0;
    hence thesis by A1,Def2;
  end;
  suppose n = 0;
    hence thesis by Def2;
  end;
end;

theorem
  0 = 0 mod n
proof
  n = 0 or n > 0;
  hence thesis by Def2,Th24;
end;

:: from JORDAN4

theorem Th27:
  i < j implies i div j = 0
proof
  assume
A1: i<j;
  per cases by Def1;
  suppose ex j1 being Nat st i=j*(i div j)+j1 & j1<j;
    then consider j1 being Nat such that
A2: i=j*(i div j)+j1 and j1<j;
    assume i div j<>0;
    then consider k such that
A3: i div j = k+1 by NAT_1:6;
    i = j + (j*k+j1) by A2,A3;
    hence contradiction by A1,NAT_1:11;
  end;
  suppose i div j=0 & j=0;
    hence thesis;
  end;
end;

:: Moved from SCMP_GCD by AK on 28.12.2006

theorem Th28:
  m > 0 implies n gcd m = m gcd (n mod m)
proof
  set r=n mod m, x=n gcd m, y=m gcd r;
  assume m>0;
  then consider t be Nat such that
A1: n = m * t + r and r < m by Def2;
  reconsider t as Element of NAT by ORDINAL1:def 12;
A2: x divides n by Def5;
A3: x divides m by Def5;
  then x divides r by A2,Th11;
  then
A4: x divides y by A3,Def5;
A5: y divides m by Def5;
A6: y divides r by Def5;
  y divides m*t by A5,Th9;
  then y divides n by A1,A6,Th8;
  then y divides x by A5,Def5;
  hence thesis by A4,Th5;
end;

:: from AMI_3, 2007.06.14, A.T.

scheme INDI{ k,n() -> Element of NAT, P[set] }: P[n()]
provided
A1: P[0] and
A2: k() > 0 and
A3: for i,j st P[k()*i] & j <> 0 & j <= k() holds P[k()*i+j]
proof
  defpred R[Nat] means P[k()*$1];
A4: R[0] by A1;
A5: now
    let i;
    assume
A6: R[i];
    k()*(i+1) = k()*i + k();
    hence R[i+1] by A2,A3,A6;
  end;
A7: for i holds R[i] from NAT_1:sch 2(A4,A5);
  per cases;
  suppose n() mod k() = 0;
    then n() = k() * (n() div k()) + 0 by A2,INT_1:59;
    hence thesis by A7;
  end;
  suppose
A8: n() mod k() <> 0;
A9: n() = k() * (n() div k()) + (n() mod k()) by A2,INT_1:59;
    n() mod k() <= k() by A2,Th1;
    hence thesis by A3,A7,A8,A9;
  end;
end;

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

theorem
  i*j = (i lcm j)*(i gcd j)
proof
A1: i<>0 & j<>0 implies i*j = (i lcm j)*(i gcd j)
  proof
    assume that
A2: i<>0 and
A3: j<>0;
A4: i divides i implies i divides i*j by Th9;
    j divides j implies j divides j*i by Th9;
    then (i lcm j) divides i*j by A4,Def4;
    then consider c being Nat such that
A5: i*j = (i lcm j)*c by Def3;
A6: i divides (i lcm j) by Def4;
A7: j divides (i lcm j) by Def4;
    consider d being Nat such that
A8: (i lcm j) = i*d by A6,Def3;
    consider e being Nat such that
A9: (i lcm j) = j*e by A7,Def3;
    i*j = i*(c*d) by A5,A8;
    then
A10: j = c*d by A2,XCMPLX_1:5;
    i*j = j*(c*e) by A5,A9;
    then i = c*e by A3,XCMPLX_1:5;
    then
A11: c divides i by Def3;
A12: c divides j by A10,Def3;
    for f being Nat holds f divides i & f divides j implies f divides c
    proof
      let f be Nat;
      assume that
A13:  f divides i and
A14:  f divides j;
      consider g being Nat such that
A15:  i = f*g by A13,Def3;
      consider h being Nat such that
A16:  j = f*h by A14,Def3;
A17:  j*g = g*h*f by A16;
      i*h = g*h*f by A15;
      then
A18:  i divides g*h*f by Def3;
      j divides g*h*f by A17,Def3;
      then (i lcm j) divides g*h*f by A18,Def4;
      then consider z being Nat such that
A19:  g*h*f = (i lcm j)*z by Def3;
A20:  c*(i lcm j) = (g*(h*f))*f by A5,A15,A16
        .= (i lcm j)*z*f by A19
        .= (z*f)*(i lcm j);
      (i lcm j) <> 0 by A2,A3,INT_2:4;
      then c = f*z by A20,XCMPLX_1:5;
      hence thesis by Def3;
    end;
    hence thesis by A5,A11,A12,Def5;
  end;
  i = 0 or j = 0 implies i*j = (i lcm j)*(i gcd j)
  proof
    assume
A21: i = 0 or j = 0;
    then i*j = 0*(i gcd j) .= (i lcm j)*(i gcd j) by A21,INT_2:4;
    hence thesis;
  end;
  hence thesis by A1;
end;

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

theorem
  for i,j being Integer st i>=0 & j>0 holds i gcd j= j gcd (i mod j)
proof
  let i,j be Integer;
  assume that
A1: i>=0 and
A2: j>0;
A3: abs(j)> 0 by A2,ABSVALUE:def 1;
  thus i gcd j = abs(i) gcd abs(j) by INT_2:34
    .=abs(j) gcd (abs(i) mod abs(j)) by A3,Th28
    .=abs(j) gcd abs(abs(i) mod abs(j)) by ABSVALUE:def 1
    .=j gcd (abs(i) mod abs(j)) by INT_2:34
    .=j gcd (i mod j) by A1,A2,INT_2:32;
end;

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

theorem
  i lcm i = i
proof
  for m being Nat st i divides m & i divides m holds i divides m;
  hence thesis by Def4;
end;

theorem
  i gcd i = i
proof
  for m being Nat st m divides i & m divides i holds m divides i;
  hence thesis by Def5;
end;

:: from SCMPDS_9. 2008.05.06, A.T.

theorem
  for i, j being Nat st i < j & i <> 0 holds i/j is not integer
proof
  let i, j be Nat such that
A1: i < j and
A2: i <> 0;
  assume i/j is integer;
  then reconsider r = i/j as Integer;
  r = [\ r /] by INT_1:25
    .= i qua Integer div j by INT_1:def 9;
  hence thesis by A1,A2,Th27,XCMPLX_1:50;
end;

:: from BINARITH, 2008.08.18, A.T.

definition
  let i,j be Nat;
  redefine func i -' j -> Element of NAT;
  coherence
  proof
    i -' j = i - j & 0 <= i -' j or i -' j = 0 by XREAL_0:def 2;
    hence thesis by INT_1:3;
  end;
end;

theorem Th34:
  for i,j being Nat holds i + j -' j = i
proof
  let i, j be Nat;
  i + j - j >= 0;
  hence thesis by XREAL_0:def 2;
end;

reserve a,b for Nat;

theorem Th35:
  a -' b <= a
proof
  a-b <= a-0 by XREAL_1:230;
  hence thesis by XREAL_0:def 2;
end;

reserve n,i,j,k for Nat;

theorem Th36:
  n-'i=0 implies n<=i
proof
  assume
A1: n-'i=0;
  assume i<n;
  then i+1<=n by NAT_1:13;
  then i+1-i<=n-i by XREAL_1:9;
  hence contradiction by A1,XREAL_0:def 2;
end;

theorem
  i<=j implies j+k-'i=j+k-i by NAT_1:12,XREAL_1:233;

theorem
  i<=j implies j+k-'i=j-'i+k
proof
  assume
A1: i<=j;
  hence j+k-'i=j+k-i by NAT_1:12,XREAL_1:233
    .=j-i+k
    .=j-'i+k by A1,XREAL_1:233;
end;

reserve i,j,k,i1,i2,n for Nat;

theorem Th39:
  i-'i1>=1 or i-i1>=1 implies i-'i1=i-i1
proof
  assume
A1: i-'i1>=1 or i-i1>=1;
  per cases by A1;
  suppose i-'i1>=1;
    hence thesis by XREAL_0:def 2;
  end;
  suppose i-i1>=1;
    hence thesis by XREAL_0:def 2;
  end;
end;

theorem
  n-'0=n
proof
  n-'0=n-0 by XREAL_0:def 2
    .=n;
  hence thesis;
end;

theorem
  i1<=i2 implies n-'i2<=n-'i1
proof
  assume
A1: i1<=i2;
  per cases;
  suppose
A2: i2<=n;
    then
A3: n-'i1=n-i1 by A1,XREAL_1:233,XXREAL_0:2;
    n-'i2=n-i2 by A2,XREAL_1:233;
    hence thesis by A1,A3,XREAL_1:10;
  end;
  suppose i2>n;
    then n-i2<0 by XREAL_1:49;
    hence thesis by XREAL_0:def 2;
  end;
end;

theorem Th42:
  i1<=i2 implies i1-'n<=i2-'n
proof
  assume
A1: i1<=i2;
  per cases;
  suppose i1-n>=0;
    then
A2: i1-'n=i1-n by XREAL_0:def 2;
    i1-n<=i2-n by A1,XREAL_1:9;
    hence thesis by A2,XREAL_0:def 2;
  end;
  suppose i1-n<0;
    hence thesis by XREAL_0:def 2;
  end;
end;

theorem Th43:
  i-'i1>=1 or i-i1>=1 implies i-'i1+i1=i
proof
  assume i-'i1>=1 or i-i1>=1;
  then i-'i1+i1=i-i1+i1 by Th39
    .=i;
  hence thesis;
end;

theorem
  i1<=i2 implies i1-'1<=i2
proof
  assume
A1: i1<=i2;
  per cases;
  suppose i1-1>=0;
    then i1-'1=i1-1 by XREAL_0:def 2;
    then i1-'1<=i1-1+1 by NAT_1:12;
    hence thesis by A1,XXREAL_0:2;
  end;
  suppose i1-1<0;
    hence thesis by XREAL_0:def 2;
  end;
end;

theorem Th45:
  i-'2=i-'1-'1
proof
  per cases;
  suppose
A1: i>=2;
    then 1<=i by XXREAL_0:2;
    then i-1>=0 by XREAL_1:48;
    then
A2: i-'1=i-1 by XREAL_0:def 2;
    i-1>=1+1-1 by A1,XREAL_1:9;
    then i-1-1>=1-1 by XREAL_1:9;
    then i-'1-'1 =i-2 by A2,XREAL_0:def 2;
    hence thesis by XREAL_0:def 2;
  end;
  suppose
A3: i<2;
    then i-2<2-2 by XREAL_1:9;
    then
A4: i-'2=0 by XREAL_0:def 2;
A5: i+1-1<=1+1-1 by A3,NAT_1:13;
    now per cases;
      case 1<=i;
        then i=1 by A5,XXREAL_0:1;
        then i-'1-'1=0-'1 by XREAL_1:232;
        hence thesis by A4,Th35;
      end;
      case i<1;
        then i-1<1-1 by XREAL_1:9;
        then i-'1-'1=0-'1 by XREAL_0:def 2;
        hence thesis by A4,Th35;
      end;
    end;
    hence thesis;
  end;
end;

theorem Th46:
  i1+1<=i2 implies i1-'1<i2 & i1-'2<i2 & i1<=i2
proof
  assume
A1: i1+1<=i2;
  then
A2: i1<i2 by NAT_1:13;
  i1-'1<=i1 by Th35;
  hence
A3: i1-'1<i2 by A2,XXREAL_0:2;
A4: i1-'1-'1=i1-'2 by Th45;
  i1-'1-'1<=i1-'1 by Th35;
  hence i1-'2<i2 by A3,A4,XXREAL_0:2;
  thus thesis by A1,NAT_1:13;
end;

theorem
  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
proof
  assume i1+2<=i2 or i1+1+1<=i2;
  then i1+1+1<=i2;
  hence
A1: i1+1<i2 & i1+1-'1<i2 & i1+1-'2<i2 & i1+1<=i2 by Th46,NAT_1:13;
  i1-'1<=i1 by Th35;
  then i1-'1+1<=i1+1 by XREAL_1:6;
  then
A2: i1-'1+1<i2 by A1,XXREAL_0:2;
  i1-'1+1-'1<=i1-'1+1 by Th35;
  hence i1-'1+1<i2 & i1-'1+1-'1<i2 by A2,XXREAL_0:2;
  thus thesis by A1,Th46,NAT_1:13;
end;

theorem
  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
proof
  assume
A1: i1<=i2 or i1<=i2-'1;
A2: now
    assume i1<=i2;
    then
A3: i1<i2+1 by NAT_1:13;
    i2+1+1=i2+(1+1);
    hence thesis by A3,NAT_1:13;
  end;
  now
    assume
A4: i1<=i2-'1;
    i2-'1<=i2 by Th35;
    hence thesis by A2,A4,XXREAL_0:2;
  end;
  hence thesis by A1,A2;
end;

theorem
  i1<i2 or i1+1<=i2 implies i1<=i2-'1
proof
  assume
A1: i1<i2 or i1+1<=i2;
  per cases by A1;
  suppose
A2: i1<i2;
    then i1+1<=i2 by NAT_1:13;
    then
A3: i1+1-1<=i2-1 by XREAL_1:9;
    0+1<=i2 by A2,NAT_1:13;
    hence thesis by A3,XREAL_1:233;
  end;
  suppose
A4: i1+1<=i2;
    then
A5: i1+1-1<=i2-1 by XREAL_1:9;
    0+1<=i2 by A4,NAT_1:13;
    hence thesis by A5,XREAL_1:233;
  end;
end;

theorem Th50:
  i>=i1 implies i>=i1-'i2
proof
  assume
A1: i>=i1;
  i1>=i1-'i2 by Th35;
  hence thesis by A1,XXREAL_0:2;
end;

theorem
  1<=i & 1<=i1-'i implies i1-'i<i1
proof
  assume that
A1: 1<=i and
A2: 1<=i1-'i;
  i1-i=(i1-'i)+i-i by A2,Th43
    .=i1-'i;
  hence thesis by A1,XREAL_1:231;
end;

theorem Th52:
  i-'k <= j implies i <= j + k
proof
  assume
A1: i-'k <= j;
  per cases;
  suppose
A2: i >= k;
    i-'k +k <= j + k by A1,XREAL_1:6;
    hence thesis by A2,XREAL_1:235;
  end;
  suppose
A3: i <= k;
    k <= j + k by NAT_1:11;
    hence thesis by A3,XXREAL_0:2;
  end;
end;

theorem
  i <= j + k implies i-'k <= j
proof
  assume i <= j + k;
  then i -' k <= j + k -' k by Th42;
  hence thesis by Th34;
end;

theorem
  i <= j -' k & k <= j implies i + k <= j
proof
  assume that
A1: i <= j -' k and
A2: j >= k;
  i + k <= j -' k + k by A1,XREAL_1:6;
  hence thesis by A2,XREAL_1:235;
end;

theorem
  j + k <= i implies k <= i -' j
proof
  assume
A1: j + k <= i;
  per cases by A1,XXREAL_0:1;
  suppose j + k = i;
    hence thesis by Th34;
  end;
  suppose j + k < i;
    hence thesis by Th52;
  end;
end;

theorem
  k <= i & i < j implies i -' k < j -' k
proof
  assume that
A1: k <= i and
A2: i < j;
  i -' k + k = i by A1,XREAL_1:235;
  then i -' k + k < j -' k + k by A1,A2,XREAL_1:235,XXREAL_0:2;
  hence thesis by XREAL_1:6;
end;

theorem
  i < j & k < j implies i -' k < j -' k
proof
  assume that
A1: i < j and
A2: k < j;
  per cases;
  suppose k <= i;
    then
A3: i -' k = i - k by XREAL_1:233;
    j -' k = j - k by A2,XREAL_1:233;
    hence thesis by A1,A3,XREAL_1:9;
  end;
  suppose k > i;
    then i - k < 0 by XREAL_1:49;
    then
A4: i -' k = 0 by XREAL_0:def 2;
    j -' k <> 0 by A2,Th36;
    hence thesis by A4;
  end;
end;

:: form JCT_MISC, 2008.08.21, A.T.

theorem
  i <= j implies j-'(j-'i) = i
proof
  assume
A1: i <= j;
  j-'(j-'i) + (j-'i) = j by Th50,XREAL_1:235
    .= i + (j-'i) by A1,XREAL_1:235;
  hence thesis;
end;

:: from LEXBFS, 2008.08.23, A.T.

theorem
  for n,k being Nat st n < k holds k -' (n+1) + 1 = k -' n
proof
  let n,k be Nat such that
A1: n < k;
A2: k -' n = k - n by A1,XREAL_1:233;
  n+1 <= k by A1,NAT_1:13;
  then k -' (n+1) = k - (n+1) by XREAL_1:233;
  hence thesis by A2;
end;

theorem
  for A being finite set holds A is trivial iff card A < 2
proof
  let A be finite set;
  hereby
    assume
A1:  A is trivial;
    per cases;
    suppose
      A is empty;
      hence card A < 2;
    end;
    suppose
      A is non empty;
      then ex x being set st A = {x} by A1,ZFMISC_1:131;
      then card A = 1 by CARD_1:30;
      hence card A < 2;
    end;
  end;
  assume
A2: card A < 2;
  per cases by A2,NAT_1:23;
  suppose card A = 0;
    hence thesis;
  end;
  suppose card A = 1;
    then A is 1-element by CARD_1:def 7;
   hence thesis;
  end;
end;

:: from INT_3, 2011.04.28, A.T.

theorem Th61:
  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
proof
  let n,a,k be Integer;
  thus
A1: now
    assume
A2: n <> 0;
    thus (a + n * k) div n = [\ (a + n * k)/n /] by INT_1:def 9
      .= [\ (a + n * k) * n" /] by XCMPLX_0:def 9
      .= [\ a * n" + (n * n") * k /]
      .= [\ a * n" + 1 * k /] by A2,XCMPLX_0:def 7
      .= [\ a * n" /] + k by INT_1:28
      .= [\ a/n /] + k by XCMPLX_0:def 9
      .= (a div n) + k by INT_1:def 9;
  end;
  per cases;
  suppose
A3: n <> 0;
    hence (a + n * k) mod n = (a + n * k) - ((a div n) + k) * n by A1,
INT_1:def 10
      .= a - (a div n) * n
      .= a mod n by A3,INT_1:def 10;
  end;
  suppose
    n = 0;
    hence thesis;
  end;
end;

theorem Th62:
  for n being Nat st n > 0 for a being Integer holds a
  mod n >= 0 & a mod n < n
proof
  let n be Nat;
  assume
A1: n > 0;
  let a be Integer;
  now
    a div n = [\ a/n /] by INT_1:def 9;
    then a div n <= a/n by INT_1:def 6;
    then (a div n) * n <= a/n * n by XREAL_1:64;
    then (a div n) * n <= (a * n") * n by XCMPLX_0:def 9;
    then (a div n) * n <= a * (n" * n);
    then (a div n) * n <= a * 1 by A1,XCMPLX_0:def 7;
    then (a div n) * n - (a div n) * n <= a - (a div n) * n by XREAL_1:9;
    hence 0 <= a mod n by INT_1:def 10;
    assume a mod n >= n;
    then a - (a div n) * n >= n by A1,INT_1:def 10;
    then (a + -(a div n) * n) + (a div n) * n >= n + (a div n) * n by XREAL_1:6
;
    then a - n >= (n + (a div n) * n) - n by XREAL_1:9;
    then (a - n) * n" >= ((a div n) * n) * n" by XREAL_1:64;
    then (a - n) * n" >= (a div n) * (n * n");
    then a * n" - n * n" >= (a div n) * 1 by A1,XCMPLX_0:def 7;
    then a * n" - 1 >= (a div n) by A1,XCMPLX_0:def 7;
    then
A2: a/n - 1 >= (a div n) by XCMPLX_0:def 9;
    a div n = [\ a/n /] by INT_1:def 9;
    hence contradiction by A2,INT_1:def 6;
  end;
  hence thesis;
end;

theorem Th63:
  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)
proof
  let n,a be Integer;
  per cases;
  suppose
    n = 0;
    hence thesis;
  end;
  suppose
A1: n <> 0;
    hereby
      assume that
A2:   0 <= a and
A3:   a < n;
      reconsider aa = a as Element of NAT by A2,INT_1:3;
      reconsider nn = n as Element of NAT by A2,A3,INT_1:3;
      consider t being Nat such that
A4:   aa = nn * t + (aa mod nn) and
      (aa mod nn) < nn by A1,Def2;
      t = 0
      proof
        assume t <> 0;
        then t >= 1 + 0 by INT_1:7;
        then
A5:     t * n >= 1 * n by A2,A3,XREAL_1:64;
        nn * t + (aa mod nn) >= nn * t by NAT_1:11;
        hence thesis by A3,A4,A5,XXREAL_0:2;
      end;
      hence a mod n = a by A4;
    end;
    assume that
A6: 0 > a and
A7: a >= -n;
A8: n >= 0 by A6,A7;
A9: a/n - 1 < -1
    proof
      assume a/n - 1 >= -1;
      then (a/n - 1) + 1 >= -1 + 1 by XREAL_1:6;
      then a * n" >= 0 by XCMPLX_0:def 9;
      then (a * n") * n >= 0 * n by A8;
      then a * (n" * n) >= 0;
      then a * 1 >= 0 by A1,XCMPLX_0:def 7;
      hence thesis by A6;
    end;
    a * n" >= (-n) * n" by A7,A8,XREAL_1:64;
    then a /n >= -(n * n") by XCMPLX_0:def 9;
    then -1 <= a/n by A1,XCMPLX_0:def 7;
    then [\ a/n /] = -1 by A9,INT_1:def 6;
    then
A10: a div n = -1 by INT_1:def 9;
    a mod n = a - (a div n) * n by A1,INT_1:def 10;
    hence thesis by A10;
  end;
end;

theorem Th64:
  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)
proof
  let n,a,b be Integer;
  hereby
    assume
A1: n <> 0;
    assume a mod n = b mod n;
    then a - (a div n) * n = b mod n by A1,INT_1:def 10;
    then a - (a div n) * n = b - (b div n) * n by A1,INT_1:def 10;
    then a - b = (-(b div n) + (a div n)) * n;
    then n divides (a-b) by INT_1:def 3;
    hence a,b are_congruent_mod n by INT_2:15;
  end;
  assume a,b are_congruent_mod n;
  then n divides (a-b) by INT_2:15;
  then consider k being Integer such that
A2: n * k = a - b by INT_1:def 3;
  a = n * k + b by A2;
  hence thesis by Th61;
end;

theorem
  for n being Nat for a being Integer holds (a mod n)
  mod n = a mod n
proof
  let n be Nat;
  let a be Integer;
  per cases;
  suppose
A1: n = 0;
    hence (a mod n) mod n = 0 by INT_1:def 10
      .= a mod n by A1,INT_1:def 10;
  end;
  suppose
    n <> 0;
    then a mod n >= 0 & a mod n < n by Th62;
    hence thesis by Th63;
  end;
end;

theorem
  for n,a,b being Integer holds (a + b) mod n = ((a mod n) + (b mod n)) mod n
proof
  let n,a,b be Integer;
  per cases;
  suppose
A1: n = 0;
    hence (a + b) mod n = 0 by INT_1:def 10
      .= ((a mod n) + (b mod n)) mod n by A1,INT_1:def 10;
  end;
  suppose
    n <> 0;
    then
    a mod n + (a div n) * n = (a - (a div n) * n) + (a div n) * n & b mod
    n + (b div n) * n = (b - (b div n) * n) + (b div n) * n by INT_1:def 10;
    then (a + b) - ((a mod n) + (b mod n)) = ((a div n) + (b div n)) * n;
    then n divides (a + b) - ((a mod n) + (b mod n)) by INT_1:def 3;
    then a+b,(a mod n)+(b mod n) are_congruent_mod n by INT_2:15;
    hence thesis by Th64;
  end;
end;

theorem
  for n,a,b being Integer holds (a * b) mod n = ((a mod n) * (b mod n)) mod n
proof
  let n,a,b be Integer;
  per cases;
  suppose
A1: n = 0;
    hence (a * b) mod n = 0 by INT_1:def 10
      .= ((a mod n) * (b mod n)) mod n by A1,INT_1:def 10;
  end;
  suppose
    n <> 0;
    then
    a mod n + (a div n) * n = (a - (a div n) * n) + (a div n) * n & b mod
    n + (b div n) * n = (b - (b div n) * n) + (b div n) * n by INT_1:def 10;
    then (a * b) - ((a mod n) * (b mod n)) = (((a mod n) * (b div n)) + (((a
    div n) * (b mod n)) + (((a div n) * n) * (b div n)))) * n;
    then n divides ((a * b) - ((a mod n) * (b mod n))) by INT_1:def 3;
    then (a*b),((a mod n)*(b mod n)) are_congruent_mod n by INT_2:15;
    hence thesis by Th64;
  end;
end;

theorem
  for a,b being Integer ex s,t being Integer st a gcd b = s * a + t * b
proof
  let a,b be Integer;
A1: for a,b being Integer st a > 0 & b > 0 holds ex s,t being Integer st (a
  gcd b) = (s * a + t * b)
  proof
    let a,b be Integer;
    assume that
A2: a > 0 and
A3: b > 0;
    reconsider a,b as Element of NAT by A2,A3,INT_1:3;
    set M = {z where z is Element of NAT : ex s,t being Integer st z = s * a +
    t * b};
    defpred P[Nat] means ($1 in M & $1 <> 0);
    a = 1 * a + 0 * b;
    then
A4: a in M;
    then
A5: ex k being Nat st P[k] by A2;
    consider g being Nat such that
A6: P[g] & for n being Nat st P[n] holds g <= n from NAT_1:sch 5(A5);
    set G = {zz where zz is Element of NAT : ex s being Element of NAT st zz =
    s * g};
    ex z being Element of NAT st z = g & ex s,t being Integer st z = s * a
    + t * b by A6;
    then consider s,t being Integer such that
A7: g = s * a + t * b;
A8: for x being set holds x in M implies x in G
    proof
      let x be set;
      assume x in M;
      then consider x9 being Element of NAT such that
A9:   x9 = x and
A10:  ex u,v being Integer st x9 = u * a + v * b;
      consider u,v being Integer such that
A11:  x = u * a + v * b by A9,A10;
      consider r being Nat such that
A12:  x9 = g * (x9 div g) + r and
A13:  r < g by A6,Def1;
A14:  r in NAT by ORDINAL1:def 12;
      r = x9 - g * (x9 div g) by A12
        .= a * (u + -(s * (x9 div g))) + b * (v + -(t * (x9 div g)))
         by A7,A9,A11;
      then r in M by A14;
      then r = 0 by A6,A13;
      hence thesis by A9,A12;
    end;
    for x being set holds x in G implies x in M
    proof
      let x be set;
      assume x in G;
      then
A15:  ex x9 being Element of NAT st x9 = x & ex u being Element of NAT st
      x9 = u * g;
      then consider u being Integer such that
A16:  x = u * g;
      x = (u * s) * a + (u * t) * b by A7,A16;
      hence thesis by A15;
    end;
    then
A17: G = M by A8,TARSKI:1;
A18: abs(b) = b by ABSVALUE:def 1;
A19: abs(a) = a by ABSVALUE:def 1;
A20: for m being Nat st m divides abs(a) & m divides abs(b) holds m divides g
    proof
      ex g9 being Element of NAT st g9 = g & ex s,t being Integer st g9 =
      s * a + t * b by A6;
      then consider s,t being Integer such that
A21:  g = s * a + t * b;
      let m be Nat;
      assume that
A22:  m divides abs(a) and
A23:  m divides abs(b);
      consider u being Nat such that
A24:  a = m * u by A19,A22,Def3;
      consider v being Nat such that
A25:  b = m * v by A18,A23,Def3;
A26:  g = m * (s * u + t * v) by A24,A25,A21;
      then s * u + t * v >= 0 by A6;
      then s * u + t * v is Element of NAT by INT_1:3;
      hence thesis by A26,Def3;
    end;
    b = 0 * a + 1 * b;
    then b in M;
    then
    ex b9 being Element of NAT st b9 = b & ex t being Element of NAT st b9
    = t * g by A17;
    then
A27: g divides abs(b) by A18,Def3;
    ex a9 being Element of NAT st a9 = a & ex s being Element of NAT st a9
    = s * g by A4,A17;
    then g divides abs(a) by A19,Def3;
    then g = abs(a) gcd abs(b) by A27,A20,Def5
      .= a gcd b by INT_2:34;
    hence thesis by A7;
  end;
  now
    per cases;
    case
A28:  a = 0 or b = 0;
A29:  for a,b being Integer holds a = 0 implies a gcd b = abs(b)
      proof
        let a,b be Integer;
        assume a = 0;
        then abs(a) = 0 by ABSVALUE:def 1;
        then
A30:    abs(b) divides abs(a) by Th6;
        a gcd b = abs(a) gcd abs(b) & for m being Nat st m divides abs(a)
        & m divides abs(b) holds m divides abs(b) by INT_2:34;
        hence thesis by A30,Def5;
      end;
      now
        per cases by A28;
        case
          a = 0;
          then
A31:      a gcd b = abs(b) by A29;
          now
            per cases;
            case
              b >= 0;
              hence a gcd b = 0 * a + 1 * b by A31,ABSVALUE:def 1;
            end;
            case
              b < 0;
              hence a gcd b = -(b * 1) by A31,ABSVALUE:def 1
                .= 0 * a + (-1) * b;
            end;
          end;
          hence thesis;
        end;
        case
          b = 0;
          then
A32:      a gcd b = abs(a) by A29;
          now
            per cases;
            case
              a >= 0;
              hence a gcd b = 1 * a + 0 * b by A32,ABSVALUE:def 1;
            end;
            case
              a < 0;
              hence a gcd b = -(a * 1) by A32,ABSVALUE:def 1
                .= 0 * b + (-1) * a;
            end;
          end;
          hence thesis;
        end;
      end;
      hence thesis;
    end;
    case
A33:  a <> 0 & b <> 0;
      now
        per cases;
        case
          a >= 0 & b >= 0;
          hence thesis by A1,A33;
        end;
        case
A34:      a < 0 & b >= 0;
          then -a > 0 by XREAL_1:58;
          then consider s,t being Integer such that
A35:      -a gcd b = s * -a + t * b by A1,A33,A34;
A36:      a gcd b = abs(a) gcd abs(b) by INT_2:34
            .= abs((-a)) gcd abs(b) by COMPLEX1:52
            .= -a gcd b by INT_2:34;
          s * -a + t * b = (-s) * a + t * b;
          hence thesis by A35,A36;
        end;
        case
A37:      a >= 0 & b < 0;
          then -b > 0 by XREAL_1:58;
          then consider s,t being Integer such that
A38:      a gcd -b = s * a + t * -b by A1,A33,A37;
A39:      a gcd b = abs(a) gcd abs(b) by INT_2:34
            .= abs(a) gcd abs((-b)) by COMPLEX1:52
            .= a gcd -b by INT_2:34;
          s * a + t * -b = s * a + (-t) * b;
          hence thesis by A38,A39;
        end;
        case
          a < 0 & b < 0;
          then -a > 0 & -b > 0 by XREAL_1:58;
          then consider s,t being Integer such that
A40:      -a gcd -b = s * -a + t * -b by A1;
A41:      a gcd b = abs(a) gcd abs(b) by INT_2:34
            .= abs(a) gcd abs((-b)) by COMPLEX1:52
            .= abs((-a)) gcd abs((-b)) by COMPLEX1:52
            .= -a gcd -b by INT_2:34;
          s * -a + t * -b = (-s) * a + (-t) * b;
          hence thesis by A40,A41;
        end;
      end;
      hence thesis;
    end;
  end;
  hence thesis;
end;

:: from RADIX_1, 2011.07.31, A.T.

theorem
  n mod k = k - 1 implies (n+1) mod k = 0
proof
  per cases;
  suppose
    k <> 0;
    then k >= 1 by NAT_1:14;
    then reconsider K = k - 1 as Element of NAT by INT_1:3,XREAL_1:48;
A1: K + 1 = k - 0;
    assume n mod k = k-1;
    then (n+1) mod k = k mod k by A1,Th22;
    hence thesis by Th25;
  end;
  suppose
    k=0;
    hence thesis;
  end;
end;

theorem
  n mod k < k - 1 implies (n+1) mod k = (n mod k) + 1
proof
  assume n mod k < k - 1;
  then
A1: (n mod k) + 1 < k by XREAL_1:20;
  (n+1) mod k = ((n mod k)+1) mod k by Th22;
  hence thesis by A1,Th24;
end;