• Abstract
• Full article

:: Integers
::  by Micha{\l} J. Trybulec
::
:: Received February 7, 1990
:: Copyright (c) 1990 Association of Mizar Users

environ

 vocabularies ARYTM, ARYTM_1, ORDINAL2, NAT_1, ARYTM_3, RELAT_1, INT_1, BOOLE,
      COMPLEX1, ARYTM_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ARYTM_2, ARYTM_1,
      NUMBERS, ARYTM_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, XXREAL_0;
 constructors FUNCT_4, ARYTM_1, ARYTM_0, XXREAL_0, XREAL_0, REAL_1, NAT_1;
 registrations XREAL_0, ARYTM_3, REAL_1, ORDINAL2, NUMBERS, ZFMISC_1, XBOOLE_0,
      XCMPLX_0, NAT_1, XXREAL_0, ORDINAL1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

begin

 reserve X,x,y,z for set,
         k,l,n,n1,n2 for Element of NAT,
         r for real number;

definition
  redefine func INT means
:: INT_1:def 1
    x in it iff ex k st x = k or x = - k;
end;

definition let i be number;
  attr i is integer means
:: INT_1:def 2
    i in INT;
end;

registration
  cluster integer Real;
  cluster integer number;
  cluster -> integer Element of INT;
end;

definition
  mode Integer is integer number;
end;

canceled 6;

theorem :: INT_1:7
  for k being natural number st r = k or r = -k holds r is Integer;

theorem :: INT_1:8
  r is Integer implies ex k st r = k or r = - k;

:: Relations between sets INT, NAT and REAL ( and their elements )

registration
  cluster -> integer Element of NAT;
  cluster natural -> integer number;
end;

registration
  cluster integer -> real number;
end;

 reserve i,i0,i1,i2,i3,i4,i5,i7,i8,i9,j for Integer;

:: Now we are ready to redefine some functions
:: Redefinition of functions "+", "*" and "-"

registration
  let i1,i2 be Integer;
  cluster i1 + i2 -> integer;
  cluster i1 * i2 -> integer;
end;

registration
  let i0 be Integer;
  cluster - i0 -> integer;
end;

registration
  let i1,i2 be Integer;
  cluster i1 - i2 -> integer;
end;

:: More redefinitions

registration
  let n be Element of NAT;
  cluster - n -> integer;
  let i1 be Integer;
  cluster i1 + n -> integer;
  cluster i1 * n -> integer;
  cluster i1 - n -> integer;
end;

registration let n1,n2;
  cluster n1 - n2 -> integer;
end;

:: Some basic theorems about integers

canceled 7;

theorem :: INT_1:16
  0 <= i0 implies i0 in NAT;

theorem :: INT_1:17
  r is Integer implies r + 1 is Integer & r - 1 is Integer;

theorem :: INT_1:18
  i2 <= i1 implies i1 - i2 in NAT;

theorem :: INT_1:19
  i1 + k = i2 implies i1 <= i2;

theorem :: INT_1:20
  i0 < i1 implies i0 + 1 <= i1;

theorem :: INT_1:21
  i1 < 0 implies i1 <= - 1;

theorem :: INT_1:22
  i1 * i2 = 1 iff (i1 = 1 & i2 = 1) or (i1 = - 1 & i2 = - 1);

theorem :: INT_1:23
  i1 * i2 = - 1 iff (i1 = - 1 & i2 = 1) or (i1 = 1 & i2 = - 1);

scheme :: INT_1:sch 1
 SepInt { P[Integer] } :
 ex X being Subset of INT st
  for x being Integer holds x in X iff P[x];

scheme :: INT_1:sch 2
 IntIndUp { F() -> Integer, P[Integer] } :
 for i0 st F() <= i0 holds P[i0] provided
 P[F()] and
 for i2 st F() <= i2 holds P[i2] implies P[i2 + 1];

scheme :: INT_1:sch 3
 IntIndDown { F() -> Integer, P[Integer] } :
 for i0 st i0 <= F() holds P[i0] provided
   P[F()] and
   for i2 st i2 <= F() holds P[i2] implies P[i2 - 1];

scheme :: INT_1:sch 4
 IntIndFull { F() -> Integer, P[Integer] } :
 for i0 holds P[i0] provided
   P[F()] and
   for i2 holds P[i2] implies P[i2 - 1] & P[i2 + 1];

scheme :: INT_1:sch 5
 IntMin { F() -> Integer, P[Integer] } :
 ex i0 st P[i0] & for i1 st P[i1] holds i0 <= i1 provided
 for i1 st P[i1] holds F() <= i1 and
 ex i1 st P[i1];

scheme :: INT_1:sch 6
 IntMax { F() -> Integer, P[Integer] } :
 ex i0 st P[i0] & for i1 st P[i1] holds i1 <= i0 provided
 for i1 st P[i1] holds i1 <= F() and
 ex i1 st P[i1];

:: abs and sgn functions with integers

:: registration let r;
::   cluster sgn r -> integer;
::    coherence
::     proof
::      r < 0 or 0 < r or r = 0;
::      hence thesis by ABSVALUE:def 2;
::     end;
:: end;

definition let i1,i2,i3 be Integer;
  pred i1,i2 are_congruent_mod i3 means
:: INT_1:def 3
    ex i4 st i3 * i4 = i1 - i2;
end;

canceled 8;

theorem :: INT_1:32
  i1,i1 are_congruent_mod i2;

theorem :: INT_1:33
  i1,0 are_congruent_mod i1 & 0,i1 are_congruent_mod i1;

theorem :: INT_1:34
  i1,i2 are_congruent_mod 1;

theorem :: INT_1:35
  i1,i2 are_congruent_mod i3 implies i2,i1 are_congruent_mod i3;

theorem :: INT_1:36
  i1,i2 are_congruent_mod i5 & i2,i3 are_congruent_mod i5
             implies i1,i3 are_congruent_mod i5;

theorem :: INT_1:37
  i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5
      implies (i1 + i3),(i2 + i4) are_congruent_mod i5;

theorem :: INT_1:38
  i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5
            implies (i1 - i3),(i2 - i4) are_congruent_mod i5;

theorem :: INT_1:39
  i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5
          implies (i1 * i3),(i2 * i4) are_congruent_mod i5;

theorem :: INT_1:40
  (i1 + i2),i3 are_congruent_mod i5 iff i1, (i3 - i2) are_congruent_mod i5;

theorem :: INT_1:41
  i4 * i5 = i3
   implies (i1,i2 are_congruent_mod i3 implies i1,i2 are_congruent_mod i4);

theorem :: INT_1:42
  i1,i2 are_congruent_mod i5 iff (i1 + i5),i2 are_congruent_mod i5;

theorem :: INT_1:43
  i1,i2 are_congruent_mod i5 iff (i1 - i5),i2 are_congruent_mod i5;

theorem :: INT_1:44
  (i1 <= r & r - 1 < i1) & (i2 <= r & r - 1 < i2) implies i1 = i2;

theorem :: INT_1:45
  (r <= i1 & i1 < r + 1) & (r <= i2 & i2 < r + 1) implies i1 = i2;

reserve r1,p,p1,g,g1,g2 for real number,
        Y for Subset of REAL;

definition
  let r be real number;
  func [\ r /] -> Integer means
:: INT_1:def 4
  it <= r & r - 1 < it;
end;

canceled;

theorem :: INT_1:47
  [\ r /] = r iff r is integer;

theorem :: INT_1:48
  [\ r /] < r iff r is not integer;

canceled;

theorem :: INT_1:50
  [\ r /] - 1 < r & [\ r /] < r + 1;

theorem :: INT_1:51
  [\ r /] + i0 = [\ r + i0 /];

theorem :: INT_1:52
  r < [\ r /] + 1;

definition
  let r be real number;
  func [/ r \] -> Integer means
:: INT_1:def 5
  r <= it & it < r + 1;
end;

canceled;

theorem :: INT_1:54
  [/ r \] = r iff r is integer;

theorem :: INT_1:55
  r < [/ r \] iff r is not integer;

canceled;

theorem :: INT_1:57
  r - 1 < [/ r \] & r < [/ r \] + 1;

theorem :: INT_1:58
  [/ r \] + i0 = [/ r + i0 \];

theorem :: INT_1:59
  [\ r /] = [/ r \] iff r is integer;

theorem :: INT_1:60
  [\ r /] < [/ r \] iff r is not integer;

theorem :: INT_1:61
  [\ r /] <= [/ r \];

theorem :: INT_1:62
  [\ ([/ r \]) /] = [/ r \];

theorem :: INT_1:63
  [\ ([\ r /]) /] = [\ r /];

theorem :: INT_1:64
  [/ ([/ r \]) \] = [/ r \];

theorem :: INT_1:65
  [/ ([\ r /]) \] = [\ r /];

theorem :: INT_1:66
  [\ r /] = [/ r \] iff not [\ r /] + 1 = [/ r \];

definition
  let r be real number;
  func frac r equals
:: INT_1:def 6
     r - [\ r /];
end;

registration
  let r be real number;
  cluster frac r -> real;
end;

definition
  let r be real number;
  redefine func frac r -> Real;
end;

canceled;

theorem :: INT_1:68
  r = [\ r /] + frac r;

theorem :: INT_1:69
  frac r < 1 & 0 <= frac r;

theorem :: INT_1:70
  [\ frac r /] = 0;

theorem :: INT_1:71
  frac r = 0 iff r is integer;

theorem :: INT_1:72
  0 < frac r iff r is not integer;

:: Functions div and mod

definition
  let i1,i2 be Integer;
  func i1 div i2 -> Integer equals
:: INT_1:def 7
    [\ i1 / i2 /];
end;

definition
  let i1,i2 be Integer;
  func i1 mod i2 -> Integer equals
:: INT_1:def 8
      i1 - (i1 div i2) * i2 if i2 <> 0
            otherwise 0;
end;

:: The divisibility relation

definition
  let i1,i2 be Integer;
  pred i1 divides i2 means
:: INT_1:def 9
    ex i3 st i2 = i1 * i3;
  reflexivity;
end;

canceled;

theorem :: INT_1:74
  for r being real number st r <> 0 holds [\ r / r /] = 1;

theorem :: INT_1:75
  for i being Integer holds i div 0 = 0;

theorem :: INT_1:76
  for i being Integer st i <> 0 holds i div i = 1;

theorem :: INT_1:77
  for i being Integer holds i mod i = 0;

begin :: Addenda

:: from FSM_1

theorem :: INT_1:78
  k < i implies ex j being Element of NAT st j = i-k & 1 <= j;

:: from SCMFSA_7, 2005.02.05, A.T.

theorem :: INT_1:79
 for a,b being Integer st a < b holds a <= b - 1;

:: from UNIFORM1, 2005.08.22, A.T.

theorem :: INT_1:80
for r being real number st r>=0 holds
[/ r \]>=0 & [\ r /]>=0 & [/ r \] is Element of NAT &
 [\ r /] is Element of NAT;

:: from SCMFSA9A, 2005.11.16, A.T.

theorem :: INT_1:81
  for i being Integer, r being real number st i <= r holds i <= [\ r /];

theorem :: INT_1:82
 for m,n being natural number holds 0 <= m qua Integer div n;

:: from SCMFSA9A, 2006.03.14, A.T.

theorem :: INT_1:83
 0 < i & 1 < j implies i div j < i;

:: from NEWTON, 2007.01.02, AK

theorem :: INT_1:84
  i2 >= 0 implies i1 mod i2 >= 0;

theorem :: INT_1:85
  i2 > 0 implies i1 mod i2 < i2;

theorem :: INT_1:86
  i2 <> 0 implies i1 = (i1 div i2) * i2 + (i1 mod i2);

:: Integers
::  by Micha{\l} J. Trybulec
::
:: Received February 7, 1990
:: Copyright (c) 1990 Association of Mizar Users

environ

 vocabularies ARYTM, ARYTM_1, ORDINAL2, NAT_1, ARYTM_3, RELAT_1, INT_1, BOOLE,
      COMPLEX1, ARYTM_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ARYTM_2, ARYTM_1,
      NUMBERS, ARYTM_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, XXREAL_0;
 constructors FUNCT_4, ARYTM_1, ARYTM_0, XXREAL_0, XREAL_0, REAL_1, NAT_1;
 registrations XREAL_0, ARYTM_3, REAL_1, ORDINAL2, NUMBERS, ZFMISC_1, XBOOLE_0,
      XCMPLX_0, NAT_1, XXREAL_0, ORDINAL1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, XBOOLE_0;
 theorems REAL_1, NAT_1, AXIOMS, TARSKI, XREAL_0, XCMPLX_0, XCMPLX_1, ZFMISC_1,
      XBOOLE_0, NUMBERS, ARYTM_0, ARYTM_2, ARYTM_1, XREAL_1, XXREAL_0,
      ORDINAL1;
 schemes NAT_1, XBOOLE_0, REAL_1;

begin

 reserve X,x,y,z for set,
         k,l,n,n1,n2 for Element of NAT,
         r for real number;

Lm1:
  z in [:{0},NAT:] \ {[0,0]} implies ex k st z = -k
   proof assume
A1:   z in [:{0},NAT:] \ {[0,0]};
     then A2:    z in [:{0},NAT:];
     then consider x,y such that
    x in {0} and
A3:   y in NAT and
A4:   z = [x,y] by ZFMISC_1:103;
     reconsider y as Element of NAT by A3;
    take y;
A5:   z in NAT \/ [:{0},NAT:] by A2,XBOOLE_0:def 2;
        not z in {[0,0]} by A1,XBOOLE_0:def 4;
     then z in INT by A5,NUMBERS:def 4,XBOOLE_0:def 4;
     then reconsider z' = z as Element of REAL by NUMBERS:15;
     consider x1,x2,y1,y2 being Element of REAL such that
A6:   z' = [*x1,x2*] and
A7:   y = [*y1,y2*] and
A8:   z' + y = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4;
A9:  x2 = 0 by A6,ARYTM_0:26;
     then A10:  z' = x1 by A6,ARYTM_0:def 7;
A11:   y2 = 0 by A7,ARYTM_0:26;
     then A12:  y = y1 by A7,ARYTM_0:def 7;
       [:{0},NAT:] c= [:{0},REAL+:] by ARYTM_2:2,ZFMISC_1:118;
     then consider x',y' being Element of REAL+ such that
A13:   z' = [0,x'] and
A14:   y = y' and
A15:   +(z',y) = y' - x' by A2,A3,ARYTM_0:def 2,ARYTM_2:2;
        x' = y' by A4,A13,A14,ZFMISC_1:33;
     then A16:     y' - x' = 0 by ARYTM_1:18;
        +(x2,y2) = 0 by A9,A11,ARYTM_0:13;
     then z' + y = 0 by A8,A10,A12,A15,A16,ARYTM_0:def 7;
    hence z = -y;
   end;

Lm2:
  for k st x = -k & k <> x holds x in [:{0},NAT:] \ {[0,0]}
   proof let k such that
A1:  x = -k and
A2:  k <> x;
     reconsider r = x as Element of REAL by A1;
        r + k = 0 by A1;
     then consider x1,x2,y1,y2 being Element of REAL such that
A3:   r = [*x1,x2*] and
A4:   k = [*y1,y2*] and
A5:   0 = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4;
A6:   k in omega;
       x2 = 0 by A3,ARYTM_0:26;
     then A7:  x1 = r by A3,ARYTM_0:def 7;
     A8: y2 = 0 by A4,ARYTM_0:26;
     then A9:  y1 = k by A4,ARYTM_0:def 7;
        +(x2,y2) = 0 by A5,ARYTM_0:26;
     then A10: +(x1,y1) = 0 by A5,ARYTM_0:def 7;
     reconsider y2 = k as Element of REAL;
A11:   now assume x1 in REAL+;
       then consider x',y' being Element of REAL+ such that
A12:     x1 = x' and
A13:     y1 = y' and
A14:     0 = x' + y' by A6,A9,A10,ARYTM_0:def 2,ARYTM_2:2;
           x' = 0 & y' = 0 by A14,ARYTM_2:6;
      hence contradiction by A2,A3,A4,A8,A12,A13,ARYTM_0:26;
     end;
        r in REAL+ \/ [:{0},REAL+:] by NUMBERS:def 1,XBOOLE_0:def 4;
     then x in [:{0},REAL+:] by A7,A11,XBOOLE_0:def 2;
     then consider x',y' being Element of REAL+ such that
A15:   x1 = [0,x'] and
A16:   y1 = y' and
A17:   0 = y' - x' by A6,A7,A9,A10,ARYTM_0:def 2,ARYTM_2:2;
     A18: x' = y' by A17,ARYTM_0:6;
        0 in {0} by TARSKI:def 1;
     then A19:   x in [:{0},NAT:] by A7,A9,A15,A16,A18,ZFMISC_1:106;
        not r in {[0,0]} by NUMBERS:def 1,XBOOLE_0:def 4;
    hence x in [:{0},NAT:] \ {[0,0]} by A19,XBOOLE_0:def 4;
   end;

definition
  redefine func INT means
   :Def1: x in it iff ex k st x = k or x = - k;
  compatibility
   proof let I be set;
    thus I = INT implies for x holds x in I iff ex k st x = k or x = - k
     proof assume
A1:    I = INT;
      let x;
      thus x in I implies ex k st x = k or x = - k
       proof assume
      A2: x in I;
    then A3:      x in NAT \/ [:{0},NAT:] by A1,NUMBERS:def 4;
A4:       not x in {[0,0]} by A1,A2,NUMBERS:def 4,XBOOLE_0:def 4;
        per cases by A3,XBOOLE_0:def 2;
        suppose x in NAT;
        hence ex k st x = k or x = - k;
        end;
        suppose x in [:{0},NAT:];
         then x in [:{0},NAT:] \ {[0,0]} by A4,XBOOLE_0:def 4;
        hence ex k st x = k or x = - k by Lm1;
       end;
       end;
      given k such that
A5:     x = k or x = - k;
      per cases by A5;
      suppose A6: x = k;
       then A7:      x in NAT \/ [:{0},NAT:] by XBOOLE_0:def 2;
          not x in {[0,0]} by A6,NUMBERS:def 1,XBOOLE_0:def 4;
      hence x in I by A1,A7,NUMBERS:def 4,XBOOLE_0:def 4;
      end;
      suppose x = -k & k <> x;
       then A8:      x in [:{0},NAT:] \ {[0,0]} by Lm2;
       then x in [:{0},NAT:];
       then A9:      x in NAT \/ [:{0},NAT:] by XBOOLE_0:def 2;
          not x in {[0,0]} by A8,XBOOLE_0:def 4;
      hence x in I by A1,A9,NUMBERS:def 4,XBOOLE_0:def 4;
     end;
     end;
    assume
A10:    for x holds x in I iff ex k st x = k or x = - k;
    thus I c= INT
     proof let x;
      assume x in I;
       then consider k such that
A11:       x = k or x = - k by A10;
      per cases by A11;
      suppose A12: x = k;
       then A13:      x in NAT \/ [:{0},NAT:] by XBOOLE_0:def 2;
      not x in {[0,0]} by A12,NUMBERS:def 1,XBOOLE_0:def 4;
      hence x in INT by A13,NUMBERS:def 4,XBOOLE_0:def 4;
      end;
      suppose x = -k & k <> x;
       then A14:      x in [:{0},NAT:] \ {[0,0]} by Lm2;
       then x in [:{0},NAT:];
       then A15:      x in NAT \/ [:{0},NAT:] by XBOOLE_0:def 2;
       not x in {[0,0]} by A14,XBOOLE_0:def 4;
      hence x in INT by A15,NUMBERS:def 4,XBOOLE_0:def 4;
     end;
     end;
    let x;
    assume A16: x in INT;
     then A17:   x in NAT \/ [:{0},NAT:] by NUMBERS:def 4;
A18:    not x in {[0,0]} by A16,NUMBERS:def 4,XBOOLE_0:def 4;
     per cases by A17,XBOOLE_0:def 2;
     suppose x in NAT;
      hence x in I by A10;
     end;
     suppose x in [:{0},NAT:];
       then x in [:{0},NAT:] \ {[0,0]} by A18,XBOOLE_0:def 4;
       then ex k st x = k or x = - k by Lm1;
      hence x in I by A10;
   end;
   end;
end;

definition let i be number;
  attr i is integer means
   :Def2: i in INT;
end;

registration
  cluster integer Real;
  existence
   proof
    take 0;
    thus 0 in INT by Def1;
   end;
  cluster integer number;
  existence
   proof
    take 0;
    thus 0 in INT by Def1;
   end;
  cluster -> integer Element of INT;
  coherence by Def2;
end;

definition
  mode Integer is integer number;
end;

canceled 6;

theorem Th7:
  for k being natural number st r = k or r = -k holds r is Integer
proof let k be natural number;
A1: k in NAT by ORDINAL1:def 13;
 assume r = k or r = -k;
  then r in INT by A1,Def1;
 hence thesis by Def2;
end;

theorem Th8:
  r is Integer implies ex k st r = k or r = - k
   proof
    assume r is Integer;
     then r is Element of INT by Def2;
    hence thesis by Def1;
   end;

:: Relations between sets INT, NAT and REAL ( and their elements )

registration
  cluster -> integer Element of NAT;
  coherence by Th7;
  cluster natural -> integer number;
  coherence
  proof let n be number;
    assume n is natural;
    then n is Element of NAT by ORDINAL1:def 13;
    hence thesis by Th7;
  end;
end;

Lm3: x in INT implies x in REAL by NUMBERS:15;

registration
  cluster integer -> real number;
coherence
  proof
    let n be number;
    assume n is integer;
    then n is Element of INT by Def2;
    then reconsider n as Element of REAL by Lm3;
    n is real;
    hence thesis;
  end;
end;

 reserve i,i0,i1,i2,i3,i4,i5,i7,i8,i9,j for Integer;

:: Now we are ready to redefine some functions
:: Redefinition of functions "+", "*" and "-"

registration
  let i1,i2 be Integer;
  cluster i1 + i2 -> integer;
    coherence
     proof
      consider k such that A1: (i1 = k or i1 = - k) by Th8;
      consider l such that A2: (i2 = l or i2 = - l) by Th8;
A3:    now
       assume i1 = k & i2 = l;
       then i1 + i2 = k + l;
       hence i1 + i2 is Integer;
      end;
A4:    now
       assume A5: i1 = k & i2 = - l;
       A6: now
        assume k - l <= 0;
        then k <= 0 + l by XREAL_1:22;
        then consider z being Nat such that
        A7: l = k + z by NAT_1:10;
        - z = - l + k by A7;
        hence k - l is Integer by Th7;
       end;
       now
        assume 0 <= k - l;
        then 0 + l <= k by XREAL_1:21;
        then consider z being Nat such that
        A8: k = l + z by NAT_1:10;
        thus k - l is Integer by A8;
       end;
       hence i1 + i2 is Integer by A5,A6;
      end;
A9:    now
       assume A10: i1 = - k & i2 = l;
       A11: now
        assume l - k <= 0;
        then l <= 0 + k by XREAL_1:22;
        then consider z being Nat such that
        A12: k = l + z by NAT_1:10;
        - z = - k + l by A12;
        hence l - k is Integer by Th7;
       end;
        now
        assume 0 <= l - k;
        then 0 + k <= l by XREAL_1:21;
        then consider z being Nat such that
        A13: l = k + z by NAT_1:10;
        thus l - k is Integer by A13;
       end;
       hence i1 + i2 is Integer by A10,A11;
      end;
      now
       assume i1 = - k & i2 = - l;
       then i1 + i2 = - (k + l);
       hence i1 + i2 is Integer by Th7;
      end;
      hence thesis by A1,A2,A3,A4,A9;
     end;
  cluster i1 * i2 -> integer;
    coherence
     proof
      consider k such that A14: (i1 = k or i1 = - k) by Th8;
      consider l such that A15: (i2 = l or i2 = - l) by Th8;
A16:    now
       assume i1 = k & i2 = l;
       then i1 * i2 = k * l;
       hence i1 * i2 is Integer;
      end;
A17:    now
       assume i1 = - k & i2 = - l;
       then i1 * i2 = k * l;
       hence i1 * i2 is Integer;
      end;
      now
       assume (i1 = - k & i2 = l) or (i1 = k & i2 = - l);
       then i1 * i2 = - (k * l);
       hence i1 * i2 is Integer by Th7;
      end;
      hence i1 * i2 is integer by A14,A15,A16,A17;
     end;
end;

registration
  let i0 be Integer;
  cluster - i0 -> integer;
  coherence
  proof
    consider k such that A1: i0 = k or i0 = - k by Th8;
    thus thesis by A1,Th7;
  end;
end;

registration
  let i1,i2 be Integer;
  cluster i1 - i2 -> integer;
  coherence
  proof
    i1 - i2 = i1 + (- i2);
    hence i1 - i2 is integer;
  end;
end;

:: More redefinitions

registration
  let n be Element of NAT;
  cluster - n -> integer;
  coherence;
  let i1 be Integer;
  cluster i1 + n -> integer;
  coherence;
  cluster i1 * n -> integer;
  coherence;
  cluster i1 - n -> integer;
  coherence;
end;

registration let n1,n2;
  cluster n1 - n2 -> integer;
  coherence;
end;

:: Some basic theorems about integers

canceled 7;

theorem Th16:
  0 <= i0 implies i0 in NAT
   proof
    assume A1: 0 <= i0;
    consider k such that A2: i0 = k or i0 = - k by Th8;
    i0 = - k implies i0 is Element of NAT by A1,XXREAL_0:1;
    hence thesis by A2;
   end;

theorem
  r is Integer implies r + 1 is Integer & r - 1 is Integer
   proof
    assume r is Integer;
    then reconsider i1 = r as Integer;
    i1 + 1 is Integer & i1 - 1 is Integer;
    hence thesis;
   end;

theorem Th18:
  i2 <= i1 implies i1 - i2 in NAT
   proof
    assume i2 <= i1;
    then i2 - i2 <= i1 - i2 by XREAL_1:11;
    hence thesis by Th16;
   end;

theorem Th19:
  i1 + k = i2 implies i1 <= i2
   proof
    now
     assume A1: i1 + k = i2;
     reconsider i0 = k as Integer;
     0 + (i1 + k) <= k + i2 by A1,XREAL_1:8;
     then i1 + i0 - i0 <= i2 + i0 - i0 by XREAL_1:11;
     hence thesis;
    end;
    hence thesis;
   end;

Lm4:
 for j being Element of NAT holds j < 1 implies j = 0
 proof let j be Element of NAT; assume j < 1;
    then j < 0 + 1;
    then A1: j <= 0 by NAT_1:13;
   assume j <> 0;
  hence thesis by A1;
 end;

Lm5: 0 < i1 implies 1 <= i1
  proof
   assume A1: 0 < i1;
   then reconsider i2 = i1 as Element of NAT by Th16;
   0 <> i2 by A1;
   hence thesis by Lm4;
  end;

theorem Th20:
  i0 < i1 implies i0 + 1 <= i1
   proof
    assume i0 < i1;
    then i0 + (- i0) < i1 + (- i0) by XREAL_1:8;
    then 1 <= i1 + (- i0) by Lm5;
    then 1 + i0 <= i1 + (- i0) + i0 by XREAL_1:8;
    hence thesis;
   end;

theorem Th21:
  i1 < 0 implies i1 <= - 1
   proof
    assume i1 < 0;
    then 0 < - i1 by XREAL_1:60;
    then 1 <= - i1 by Lm5;
    then - - i1 <= - 1 by XREAL_1:26;
    hence i1 <= - 1;
   end;

theorem Th22:
  i1 * i2 = 1 iff (i1 = 1 & i2 = 1) or (i1 = - 1 & i2 = - 1)
   proof
    thus i1 * i2 = 1 implies (i1 = 1 & i2 = 1) or (i1 = - 1 & i2 = - 1)
     proof
      assume A1: i1 * i2 = 1;
then A2:    not(i1 = 0 or i2 = 0);
      A3: now
       assume 0 < i1 & 0 < i2;
       then i1 is Element of NAT & i2 is Element of NAT by Th16;
       hence i1 = 1 & i2 = 1 by A1,NAT_1:15;
      end;
      now
       assume i1 < 0 & i2 < 0;
       then 0 <= - i1 & 0 <= - i2 by XREAL_1:60;
       then A4: (- i1) is Element of NAT & (- i2) is Element of NAT by Th16;
       (- i1) * (- i2) = i1 * i2;
       then - (- i1) = - 1 & - (- i2) = - 1 by A1,A4,NAT_1:15;
       hence i1 = - 1 & i2 = - 1;
      end;
      hence thesis by A1,A2,A3,XREAL_1:134;
     end;
    thus thesis;
   end;

theorem
  i1 * i2 = - 1 iff (i1 = - 1 & i2 = 1) or (i1 = 1 & i2 = - 1)
   proof
    thus i1 * i2 = - 1 implies (i1 = - 1 & i2 = 1) or (i1 = 1 & i2 = - 1)
     proof
      assume A1: i1 * i2 = - 1;
      (- i1) * i2 = 1 by A1;
      then A2: (- (- i1) = - 1 & i2 = 1) or (- i1 = - 1 & i2 = - 1) by Th22;
      thus thesis by A2;
     end;
    assume (i1 = - 1 & i2 = 1) or (i1 = 1 & i2 = - 1);
    hence thesis;
   end;

Lm6: i0 <= i1 implies ex k st i0 + k = i1
 proof
  assume i0 <= i1;
  then reconsider k = i1 - i0 as Element of NAT by Th18;
  i0 + k = i1;
  hence thesis;
 end;

Lm7: i0 <= i1 implies ex k st i1 - k = i0
 proof
  assume i0 <= i1;
  then reconsider k = i1 - i0 as Element of NAT by Th18;
  i1 - k = i0;
  hence thesis;
 end;

 Lm8:
  r - 1 < r by XREAL_1:148;

scheme SepInt { P[Integer] } :
 ex X being Subset of INT st
  for x being Integer holds x in X iff P[x]
proof
     defpred P1[set] means ex i0 st i0 = $1 & P[i0];
    consider X such that
A1:   for y holds y in X iff
      y in INT & P1[y] from XBOOLE_0:sch 1;
     X is Subset of INT
     proof
      y in X implies y in INT by A1;
      hence thesis by TARSKI:def 3;
     end;
    then reconsider X as Subset of INT;
    take X;
    let i0;
A2:  i0 in X implies P[i0]
     proof
      assume i0 in X;
      then ex i1 st i0 = i1 & P[i1] by A1;
      hence thesis;
     end;
     P[i0] implies i0 in X
     proof
      assume A3: P[i0];
      i0 in INT by Def2;
      hence thesis by A1,A3;
     end;
    hence thesis by A2;
   end;

scheme IntIndUp { F() -> Integer, P[Integer] } :
 for i0 st F() <= i0 holds P[i0] provided
A1: P[F()] and
A2: for i2 st F() <= i2 holds P[i2] implies P[i2 + 1]
proof
  let i0;
  assume A3: F() <= i0;
  defpred Q[natural number] means
   for i2 st $1 = i2 - F() holds P[i2];
A4: Q[0] by A1;
A5: for k st Q[k] holds Q[k + 1]
    proof
     let k;
     reconsider i8 = k as Integer;
     assume A6: Q[k];
     let i2;
     assume A7: k + 1 = i2 - F();
     then k = i2 - 1 - F();
     then A8: P[i2 - 1] by A6;
     F() <= i2 - 1
      proof
        i2 - 1 = i8 + F() by A7;
       hence thesis by Th19;
      end;
     then P[i2 - 1 + 1] by A2,A8;
     hence thesis;
    end;
A9: for k holds Q[k] from NAT_1:sch 1(A4,A5);
  reconsider l = i0 - F() as Element of NAT by A3,Th18;
  l = i0 - F();
  hence P[i0] by A9;
 end;

scheme IntIndDown { F() -> Integer, P[Integer] } :
 for i0 st i0 <= F() holds P[i0] provided
  A1: P[F()] and
  A2: for i2 st i2 <= F() holds P[i2] implies P[i2 - 1]
proof
  let i0;
  assume A3: i0 <= F();
  defpred Q[Integer] means
   for i2 st $1 = - i2 holds P[i2];
A4: Q[- F()] by A1;
A5: for i2 st - F() <= i2 holds Q[i2] implies Q[i2 + 1]
    proof
     let i2;
     assume that A6: - F() <= i2 and A7: Q[i2];
     let i3;
     assume A8: i2 + 1 = - i3;
     then - i3 - 1 = i2;
     then i2 = - (i3 + 1);
     then A9: P[i3 + 1] by A7;
           i3 + 1 <= F()
      proof
       i2 = - i3 - 1 by A8;
       then - (- i3 - 1) <= - (- F()) by A6,XREAL_1:26;
       hence thesis;
      end;
     then P[i3 + 1 - 1] by A2,A9;
     hence thesis;
    end;
A10: for i2 st - F() <= i2 holds Q[i2] from IntIndUp(A4,A5);
       - F() <= - i0 by A3,XREAL_1:26;
  hence thesis by A10;
 end;

scheme IntIndFull { F() -> Integer, P[Integer] } :
 for i0 holds P[i0] provided
  A1: P[F()] and
  A2: for i2 holds P[i2] implies P[i2 - 1] & P[i2 + 1]
proof
    A3:P[F()] by A1;
  let i0;
A4: now
    assume A5: F() <= i0;
    A6: for i2 st F() <= i2 holds P[i2] implies P[i2 + 1] by A2;
    for i2 st F() <= i2 holds P[i2] from IntIndUp(A3,A6);
    hence P[i0] by A5;
   end;
   now
    assume A7: i0 <= F();
A8: for i2 st i2 <= F() holds P[i2] implies P[i2 - 1] by A2;
    for i2 st i2 <= F() holds P[i2] from IntIndDown(A3,A8);
    hence P[i0] by A7;
   end;
  hence thesis by A4;
 end;

scheme IntMin { F() -> Integer, P[Integer] } :
 ex i0 st P[i0] & for i1 st P[i1] holds i0 <= i1 provided
A1: for i1 st P[i1] holds F() <= i1 and
A2: ex i1 st P[i1]
proof
  consider i1 such that A3: P[i1] by A2;
       F() <= i1 by A1,A3;
  then A4: ex k st F() + k = i1 by Lm6;
  defpred Q[natural number] means P[F() + $1];
   A5: ex k st Q[k] by A3,A4;
   consider l such that A6: Q[l] & for n st Q[n] holds l <= n from NAT_1:sch 5
(A5);
   take i0 = F() + l;
      for i1 st P[i1] holds i0 <= i1
     proof
      let i1;
      assume A7: P[i1];
      then F() <= i1 by A1;
      then consider n such that A8: F() + n = i1 by Lm6;
       i0 - F() <= i1 - F() by A6,A7,A8;
      hence i0 <= i1 by XREAL_1:11;
     end;
   hence thesis by A6;
 end;

scheme IntMax { F() -> Integer, P[Integer] } :
 ex i0 st P[i0] & for i1 st P[i1] holds i1 <= i0 provided
A1: for i1 st P[i1] holds i1 <= F() and
A2: ex i1 st P[i1]
proof
  consider i1 such that A3: P[i1] by A2;
  i1 <= F() by A1,A3;
  then A4: ex k st i1 = F() - k by Lm7;
  defpred Q[natural number] means P[F() - $1];
   A5: ex k st Q[k] by A3,A4;
   consider l such that A6: Q[l] & for n st Q[n] holds l <= n from NAT_1:sch 5
(A5);
   take i0 = F() - l;
      for i1 st P[i1] holds i1 <= i0
     proof
      let i1;
      assume A7: P[i1];
      then i1 <= F() by A1;
      then consider n such that A8: F() - n = i1 by Lm7;
       l <= n by A6,A7,A8;
      then F() + (- i0) - F() <= F() - i1 - F() by A8,XREAL_1:11;
      then - i0 <= F() + (- i1) - F();
      hence i1 <= i0 by XREAL_1:26;
     end;
   hence thesis by A6;
 end;

:: abs and sgn functions with integers

:: registration let r;
::   cluster sgn r -> integer;
::    coherence
::     proof
::      r < 0 or 0 < r or r = 0;
::      hence thesis by ABSVALUE:def 2;
::     end;
:: end;

definition let i1,i2,i3 be Integer;
  pred i1,i2 are_congruent_mod i3 means
   :Def3: ex i4 st i3 * i4 = i1 - i2;
end;

canceled 8;

theorem
  i1,i1 are_congruent_mod i2
   proof
    i2 * 0 = i1 - i1;
    hence thesis by Def3;
   end;

theorem
  i1,0 are_congruent_mod i1 & 0,i1 are_congruent_mod i1
   proof
     i1 * 1 = i1 - 0 & i1 * (- 1) = 0 - i1;
    hence thesis by Def3;
   end;

theorem
  i1,i2 are_congruent_mod 1
   proof
    i1 - i2 = 1 * (i1 - i2);
    hence thesis by Def3;
   end;

theorem
  i1,i2 are_congruent_mod i3 implies i2,i1 are_congruent_mod i3
   proof
    assume i1,i2 are_congruent_mod i3;
    then consider i0 such that A1: (i1 - i2) = i3 * i0 by Def3;
    i2 - i1 = i3 * (- i0) by A1;
    hence thesis by Def3;
   end;

theorem
  i1,i2 are_congruent_mod i5 & i2,i3 are_congruent_mod i5
             implies i1,i3 are_congruent_mod i5
   proof
    assume A1: i1,i2 are_congruent_mod i5 & i2,i3 are_congruent_mod i5;
    then consider i8 such that A2: i5 * i8 = i1 - i2 by Def3;
    consider i9 such that A3: i5 * i9 = i2 - i3 by A1,Def3;
         (i5 * i8) + (i5 * i9) = i1 - i3 by A2,A3;
    then i5 * (i8 + i9) = i1 - i3;
    hence thesis by Def3;
   end;

theorem
  i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5
      implies (i1 + i3),(i2 + i4) are_congruent_mod i5
   proof
    assume A1: i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5;
    then consider i8 such that A2: i5 * i8 = i1 - i2 by Def3;
    consider i9 such that A3: i5 * i9 = i3 - i4 by A1,Def3;
         (i5 * i8) + (i5 * i9) = (i1 + i3) - (i2 + i4) by A2,A3;
    then i5 * (i8 + i9) = (i1 + i3) - (i2 + i4);
    hence thesis by Def3;
   end;

theorem
  i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5
            implies (i1 - i3),(i2 - i4) are_congruent_mod i5
   proof
    assume A1: i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5;
    then consider i8 such that A2: i5 * i8 = i1 - i2 by Def3;
    consider i9 such that A3: i5 * i9 = i3 - i4 by A1,Def3;
    ex i7 st i5 * i7 = (i1 - i3) - (i2 - i4)
     proof
      (i1 - i3) - (i2 - i4) = i5 * (i8 - i9) by A2,A3;
      hence thesis;
     end;
    hence thesis by Def3;
   end;

theorem
  i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5
          implies (i1 * i3),(i2 * i4) are_congruent_mod i5
   proof
    assume A1: i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5;
    then consider i8 such that A2: i5 * i8 = i1 - i2 by Def3;
    consider i9 such that A3: i5 * i9 = i3 - i4 by A1,Def3;
     ex i7 st i5 * i7 = (i1 * i3) - (i2 * i4)
     proof
      (i1 * i3) - (i2 * i4)
         = (i1 - i2) * i3 + (i3 - i4) * i2
        .= (i5 * i8) * i3 + (i5 * i9) * i2 by A2,A3
        .= i5 * ((i8 * i3) + (i9 * i2));
      hence thesis;
     end;
    hence thesis by Def3;
   end;

theorem
  (i1 + i2),i3 are_congruent_mod i5 iff i1, (i3 - i2) are_congruent_mod i5
   proof
    thus (i1 + i2),i3 are_congruent_mod i5
              implies i1,(i3 - i2) are_congruent_mod i5
     proof
      assume (i1 + i2),i3 are_congruent_mod i5;
      then A1: ex i0 st i5 * i0 = (i1 + i2) - i3 by Def3;
           (i1 + i2) - i3 = i1 - (i3 - i2);
      hence thesis by A1,Def3;
     end;
    assume i1, (i3 - i2) are_congruent_mod i5;
    then A2: ex i0 st i5 * i0 = i1 - (i3 - i2) by Def3;
         i1 - (i3 - i2) = (i1 + i2) - i3;
    hence thesis by A2,Def3;
   end;

theorem
  i4 * i5 = i3
   implies (i1,i2 are_congruent_mod i3 implies i1,i2 are_congruent_mod i4)
   proof
    assume A1: i4 * i5 = i3;
    assume i1,i2 are_congruent_mod i3;
    then consider i0 such that A2: i3 * i0 = i1 - i2 by Def3;
         i1 - i2 = i4 * (i5 * i0) by A1,A2;
    hence thesis by Def3;
   end;

theorem
  i1,i2 are_congruent_mod i5 iff (i1 + i5),i2 are_congruent_mod i5
   proof
    thus i1,i2 are_congruent_mod i5 implies (i1 + i5),i2 are_congruent_mod i5
     proof
      assume i1,i2 are_congruent_mod i5;
      then consider i0 such that A1: i5 * i0 = i1 - i2 by Def3;
           (i5 * i0) + (i5 * 1) = (i1 + i5) - i2 by A1;
      then i5 * (i0 + 1) = (i1 + i5) - i2 &
           (i0 + 1) is Integer;
      hence thesis by Def3;
     end;
    assume (i1 + i5),i2 are_congruent_mod i5;
    then consider i0 such that A2: i5 * i0 = (i1 + i5) - i2 by Def3;
         (i5 * i0) - (i5 * 1) = i1 - i2 by A2;
    then i5 * (i0 - 1) = i1 - i2 & (i0 - 1) is Integer;
    hence thesis by Def3;
   end;

theorem
  i1,i2 are_congruent_mod i5 iff (i1 - i5),i2 are_congruent_mod i5
   proof
    thus i1,i2 are_congruent_mod i5 implies (i1 - i5),i2 are_congruent_mod i5
     proof
      assume i1,i2 are_congruent_mod i5;
      then consider i0 such that A1: i5 * i0 = i1 - i2 by Def3;
           (i5 * i0) - (i5 * 1) = (i1 - i5) - i2 by A1;
      then i5 * (i0 - 1) = (i1 - i5) - i2 &
           (i0 - 1) is Integer;
      hence thesis by Def3;
     end;
    assume (i1 - i5),i2 are_congruent_mod i5;
    then consider i0 such that A2: i5 * i0 = (i1 - i5) - i2 by Def3;
         (i5 * i0) + (i5 * 1) = i1 - i2 by A2;
    then i5 * (i0 + 1) = i1 - i2 & (i0 + 1) is Integer;
    hence thesis by Def3;
   end;

theorem Th44:
  (i1 <= r & r - 1 < i1) & (i2 <= r & r - 1 < i2) implies i1 = i2
   proof
    assume A1: (i1 <= r & r - 1 < i1) & (i2 <= r & r - 1 < i2);
         i2 = i1 + (i2 - i1);
    then consider i0 such that A2: i2 = i1 + i0;
A3:   i0 = 0 implies i2 = i1 by A2;
A4:  now
     assume i0 < 0 & i1 <> i2;
     then i0 <= - 1 by Th21;
     then i1 + i0 <= r + (- 1) by A1,XREAL_1:9;
     hence contradiction by A1,A2;
    end;
       now
     assume 0 < i0 & i1 <> i2;
     then 1 <= i0 by Lm5;
     then r - 1 + 1 < i1 + i0 by A1,XREAL_1:10;
     hence contradiction by A1,A2;
    end;
    hence thesis by A3,A4;
   end;

theorem Th45:
  (r <= i1 & i1 < r + 1) & (r <= i2 & i2 < r + 1) implies i1 = i2
   proof
    assume A1: (r <= i1 & i1 < r + 1) & (r <= i2 & i2 < r + 1);
         i2 = i1 + (i2 - i1);
    then consider i0 such that A2: i2 = i1 + i0;
A3:   i0 = 0 implies i2 = i1 by A2;
A4:  now
     assume i0 < 0 & i1 <> i2;
     then i0 <= - 1 by Th21;
     then i1 + i0 < r + 1 + (- 1) by A1,XREAL_1:10;
     hence contradiction by A1,A2;
    end;
       now
     assume 0 < i0 & i1 <> i2;
     then 1 <= i0 by Lm5;
     hence contradiction by A1,A2,XREAL_1:9;
    end;
    hence thesis by A3,A4;
   end;

reserve r1,p,p1,g,g1,g2 for real number,
        Y for Subset of REAL;

Lm9:for r ex n st r<n
  proof
   let r;
   defpred P[Real] means for r st r in NAT holds not $1<r;
    consider Y such that
A1: for p1 being Real holds
    p1 in Y iff P[p1] from REAL_1:sch 1;
      for r,p1 st r in NAT & p1 in Y holds r <= p1 by A1;
   then consider g2 such that
A2:  for r,p st r in NAT & p in Y holds r <= g2 & g2 <= p by AXIOMS:26;
A3:   g2-1 is Real by XREAL_0:def 1;
       A4: g2+-1<g2+0 by XREAL_1:8;
          for g ex r st r in NAT & g<r
  proof
    given g1 such that
A5:  for r st r in NAT holds not g1<r;
         g1 is Real by XREAL_0:def 1;
then A6: g1 in Y by A1,A5;
         now assume not g2-1 in Y;
      then consider r1 such that
  A7: r1 in NAT and
  A8: g2-1<r1 by A1,A3;
  A9: g2-1+1<r1+1 by A8,XREAL_1:8;
      r1+1 in NAT by A7,AXIOMS:28;
      hence contradiction by A2,A6,A9;
     end;
    hence contradiction by A2,A4;
   end;
   then consider p such that
A10: p in NAT and
A11: r<p;
   reconsider p as Element of NAT by A10;
   take p;
   thus r<p by A11;
  end;

definition
  let r be real number;
  func [\ r /] -> Integer means :Def4:
  it <= r & r - 1 < it;
   existence
    proof
    consider n such that A1: - r < n by Lm9;
A2: - n < -- r by A1,XREAL_1:26;
    defpred P[Integer] means r < $1;
A3:   for i1 st P[i1] holds -n <= i1
       proof
        let i1;
        assume r < i1;
        then r + -n < i1 + r by A2,XREAL_1:10;
        hence -n <= i1 by XREAL_1:8;
       end;
    consider n such that A4: r < n by Lm9;
    reconsider i0 = n as Integer;
       r < i0 by A4;
    then A5: ex i0 st P[i0];
      consider i1 such that
A6:    P[i1] & for i2 st P[i2] holds i1 <= i2 from IntMin(A3,A5);
A7:   r < i1 - 1 implies i1 <= i1-1 by A6;
     r - 1 < i1 - 1 by A6,XREAL_1:11;
     hence thesis by A7,Lm8;
    end;
   uniqueness by Th44;
end;

canceled;

theorem Th47:
  [\ r /] = r iff r is integer
   proof
     r is Integer implies [\ r /] = r
     proof
      r + 0 < r + 1 by XREAL_1:8;
      then A1: r - 1 < r + 1 - 1 by XREAL_1:11;
      assume r is Integer;
      hence thesis by A1,Def4;
     end;
    hence thesis;
   end;

theorem Th48:
  [\ r /] < r iff r is not integer
   proof
   now
     assume A1: not r is Integer;
     [\ r /] <= r by Def4;
     hence [\ r /] < r by A1,REAL_1:def 5;
    end;
    hence thesis by Th47;
   end;

canceled;

theorem
  [\ r /] - 1 < r & [\ r /] < r + 1
   proof
    [\ r /] <= r by Def4;
    then A1: [\ r /] + 0 < r + 1 by XREAL_1:10;
    then [\ r /] + (- 1) < r + 1 + (- 1) by XREAL_1:8;
    hence thesis by A1;
   end;

theorem Th51:
  [\ r /] + i0 = [\ r + i0 /]
   proof
    A1: r - 1 < [\ r /] & [\ r /] <= r by Def4;
    then r - 1 + i0 < [\ r /] + i0 by XREAL_1:8;
    then A2: r + i0 - 1 < [\ r /] + i0;
    [\ r /] + i0 <= r + i0 by A1,XREAL_1:8;
    hence thesis by A2,Def4;
   end;

theorem Th52:
  r < [\ r /] + 1
   proof
    r - 1 < [\ r /] by Def4;
    then r - 1 + 1 < [\ r /] + 1 by XREAL_1:8;
    hence r < [\ r /] + 1;
   end;

definition
  let r be real number;
  func [/ r \] -> Integer means :Def5:
  r <= it & it < r + 1;
   existence
    proof
A1:  now
      assume
A2:    r is Integer;
      r + 0 < r + 1 by XREAL_1:8;
      hence r <= [\ r /] & [\ r /] < r + 1 by A2,Th47;
     end;
     now assume not r is Integer;
      then [\ r /] < r by Th48;
      hence r <= [\ r /] + 1 & [\ r /] + 1 < r + 1 by Th52,XREAL_1:8;
     end;
     hence thesis by A1;
    end;
   uniqueness by Th45;
end;

canceled;

theorem Th54:
  [/ r \] = r iff r is integer
   proof
    r is Integer implies [/ r \] = r
     proof
      r + 0 < r + 1 by XREAL_1:8;
      hence thesis by Def5;
     end;
    hence thesis;
   end;

theorem Th55:
  r < [/ r \] iff r is not integer
  proof
   now
     assume A1: not r is Integer;
     r <= [/ r \] by Def5;
     hence r < [/ r \] by A1,REAL_1:def 5;
    end;
    hence thesis by Th54;
  end;

canceled;

theorem
  r - 1 < [/ r \] & r < [/ r \] + 1
   proof
    r <= [/ r \] by Def5;
    then A1: r + 0 < [/ r \] + 1 by XREAL_1:10;
    then r + (- 1) < [/ r \] + 1 + (- 1) by XREAL_1:8;
    hence thesis by A1;
   end;

theorem
  [/ r \] + i0 = [/ r + i0 \]
   proof
    A1: r <= [/ r \] & [/ r \] < r + 1 by Def5;
    then [/ r \] + i0 < r + 1 + i0 by XREAL_1:8;
    then A2: [/ r \] + i0 < r + i0 + 1;
    r + i0 <= [/ r \] + i0 by A1,XREAL_1:8;
    hence thesis by A2,Def5;
   end;

theorem Th59:
  [\ r /] = [/ r \] iff r is integer
  proof
A1:  now
     assume r is Integer;
     hence [\ r /] = r & r = [/ r \] by Th47,Th54;
     hence [\ r /] = [/ r \];
    end;
    now
     assume not r is Integer;
     then [\ r /] < r & r < [/ r \] by Th48,Th55;
     hence [\ r /] <> [/ r \];
    end;
    hence thesis by A1;
  end;

theorem Th60:
  [\ r /] < [/ r \] iff r is not integer
  proof
    now
     assume not r is Integer;
     then [\ r /] < r & r < [/ r \] by Th48,Th55;
     hence [\ r /] < [/ r \] by XXREAL_0:2;
    end;
    hence thesis by Th59;
  end;

theorem
  [\ r /] <= [/ r \]
   proof
    [\ r /] <= r & r <= [/ r \] by Def4,Def5;
    hence thesis by XXREAL_0:2;
   end;

theorem
  [\ ([/ r \]) /] = [/ r \] by Th47;

theorem
  [\ ([\ r /]) /] = [\ r /] by Th47;

theorem
  [/ ([/ r \]) \] = [/ r \] by Th54;

theorem
  [/ ([\ r /]) \] = [\ r /] by Th54;

theorem
  [\ r /] = [/ r \] iff not [\ r /] + 1 = [/ r \]
   proof
    set Diff = [/ r \] + (- [\ r /]);
    reconsider i0 = 1 as Integer;
A1:  now
     assume r is Integer;
     then [\ r /] = [/ r \] by Th59;
     hence [\ r /] = [/ r \] & [\ r /] + 1 <> [/ r \];
    end;
    now
     assume  not r is Integer;
     then [\ r /] < [/ r \] by Th60;
     then [\ r /] + (- [\ r /]) < Diff by XREAL_1:8;
     then A2: 1 <= Diff by Lm5;
A3:   [/ r \] < r + 1 by Def5;
     r - 1 < [\ r /] by Def4;
     then - [\ r /] < - (r - 1) by XREAL_1:26;
     then Diff < r + 1 + (- (r - 1)) by A3,XREAL_1:10;
     then Diff + 1 + (- 1) <= 1 + 1 + (- 1) by Th20;
     then [\ r /] + 1 = [\ r /] + Diff by A2,XXREAL_0:1;
     hence [\ r /] + 1 = [/ r \] & [\ r /] <> [/ r \];
    end;
    hence thesis by A1;
   end;

definition
  let r be real number;
  func frac r equals
     r - [\ r /];
  coherence;
end;

registration
  let r be real number;
  cluster frac r -> real;
  coherence;
end;

definition
  let r be real number;
  redefine func frac r -> Real;
  coherence by XREAL_0:def 1;
end;

canceled;

theorem
  r = [\ r /] + frac r;

theorem Th69:
  frac r < 1 & 0 <= frac r
   proof
A1: r - 1 < [\ r /] & [\ r /] <= r by Def4;
    then frac r + (r - 1) < r - [\ r /] + [\ r /] by XREAL_1:8;
    then frac r + (- 1) + r - r < r - r by XREAL_1:11;
    then A2: frac r - 1 + 1 < 0 + 1 by XREAL_1:8;
    [\ r /] + (r - [\ r /]) <= r + frac r by A1,XREAL_1:8;
    then r - r <= r + frac r - r by XREAL_1:11;
    hence thesis by A2;
   end;

theorem
  [\ frac r /] = 0
   proof
     [\ frac r /] = [\ (r + (- [\ r /])) /]
     .= [\ r /] + (- [\ r /]) by Th51
     .= 0;
    hence thesis;
   end;

theorem Th71:
  frac r = 0 iff r is integer
    proof
A1:   now
      assume r is Integer;
      then A2: r = [\ r /] by Th47;
      thus frac r = 0 by A2;
     end;
     thus thesis by A1;
    end;

theorem
  0 < frac r iff r is not integer
    proof
    now
      assume not r is Integer;
      then 0 <> frac r;
      hence 0 < frac r by Th69;
     end;
     hence thesis by Th71;
    end;

:: Functions div and mod

definition
  let i1,i2 be Integer;
  func i1 div i2 -> Integer equals
    [\ i1 / i2 /];
  correctness;
end;

definition
  let i1,i2 be Integer;
  func i1 mod i2 -> Integer equals
    :Def8:  i1 - (i1 div i2) * i2 if i2 <> 0
            otherwise 0;
  correctness;
end;

:: The divisibility relation

definition
  let i1,i2 be Integer;
  pred i1 divides i2 means
    ex i3 st i2 = i1 * i3;
  reflexivity
  proof
   let a be Integer;
   reconsider x = 1 as Integer;
   take x;
   thus thesis;
  end;
end;

canceled;

theorem Th74:
  for r being real number st r <> 0 holds [\ r / r /] = 1
  proof
    let r be real number;
    assume r <> 0;
    hence [\ r / r /] = [\ 1 /] by XCMPLX_1:60
     .= 1 by Th47;
  end;

theorem
  for i being Integer holds i div 0 = 0
  proof
    let i be Integer;
A1: 0 - 1 < 0;
    i / 0 = i * 0" by XCMPLX_0:def 9
         .= i * 0;
    then [\ i / 0 /] = 0 by A1,Def4;
    hence thesis;
  end;

theorem Th76:
  for i being Integer st i <> 0 holds i div i = 1 by Th74;

theorem
  for i being Integer holds i mod i = 0
  proof
    let i be Integer;
    per cases;
      suppose i = 0;
      hence i mod i = 0 by Def8;
      end;
      suppose A1:i <> 0;
      hence i mod i = i - (i div i) * i by Def8 .= i - 1 * i by A1,Th76
         .= 0;
  end;
  end;

begin :: Addenda

:: from FSM_1

theorem
  k < i implies ex j being Element of NAT st j = i-k & 1 <= j
proof
  assume k < i; then A1: k - k < i - k by XREAL_1:11;
  then A2: 0 < i - k;
  reconsider j = i - k as Element of NAT by A1,Th16;
  take j; thus j = i - k;
  reconsider j' = j, 0' = 0 as Integer;
  0' + 1 <= j' by A2,Th20;
  hence 1 <= j;
end;

:: from SCMFSA_7, 2005.02.05, A.T.

theorem
 for a,b being Integer st a < b holds a <= b - 1
 proof
    let a,b be Integer;
    assume a < b;
    then a - 1 < b - 1 by XREAL_1:11;
    then a - 1 + 1 <= b - 1 by Th20;
    hence thesis;
 end;

:: from UNIFORM1, 2005.08.22, A.T.

theorem for r being real number st r>=0 holds
[/ r \]>=0 & [\ r /]>=0 & [/ r \] is Element of NAT &
 [\ r /] is Element of NAT
proof let r be real number;assume A1:r>=0;
      r-1<[\ r /] by Def4; then r-1+1<[\ r /]+1 by XREAL_1:8;
  then 0-1<[\ r /]+1-1 by A1,XREAL_1:11;
  then A2:[\ r /]>=0 by Th21;
      r<=[/ r \] by Def5;
 hence thesis by A1,A2,Th16;
end;

:: from SCMFSA9A, 2005.11.16, A.T.

theorem Th81:
  for i being Integer, r being real number st i <= r holds i <= [\ r /]
proof
  let i be Integer; let r be real number;
  assume
A1: i <= r;
A2: r-1 < [\ r /] by Def4;
    i-1 <= r-1 by A1,XREAL_1:11;
   then i-1 < [\ r /] by A2,XXREAL_0:2;
   then i-1+1 <= [\ r /] by Th20;
 hence i <= [\ r /];
end;

theorem
 for m,n being natural number holds 0 <= m qua Integer div n by Th81;

:: from SCMFSA9A, 2006.03.14, A.T.

theorem
 0 < i & 1 < j implies i div j < i
proof assume that
A1: 0 < i and
A2: 1 < j;
A3: 0 <= j by A2;
A4: j <> 0 by A2;
   assume
A5: i <= i div j;
   then 0 < i div j by A1;
   then A6: 0 < (i div j)" by XREAL_1:124;
   i div j <= i/j by Def4;
   then j * (i div j) <= j * (i/j) by A3,XREAL_1:66;
   then j * (i div j) <= i by A4,XCMPLX_1:88;
   then j * (i div j) <= i div j by A5,XXREAL_0:2;
   then j * (i div j) * (i div j)" <= (i div j) * (i div j)" by A6,XREAL_1:66;
   then j * ((i div j) * (i div j)") <= (i div j) * (i div j)";
   then j * 1 <= (i div j) * (i div j)" by A1,A5,XCMPLX_0:def 7;
 hence contradiction by A1,A2,A5,XCMPLX_0:def 7;
end;

:: from NEWTON, 2007.01.02, AK

theorem
  i2 >= 0 implies i1 mod i2 >= 0
  proof
   assume A1:i2 >= 0;
   per cases by A1;
   suppose A2:i2 > 0;
   [\ i1/i2 /] <= i1/i2 by Def4;
   then (i1 div i2)*i2 <= (i1/i2)*i2 by A2,XREAL_1:66;
   then (i1 div i2)*i2 <= i1 by A2,XCMPLX_1:88;
   then i1 - (i1 div i2)*i2 >= 0 by XREAL_1:50;
   hence thesis by A2,Def8;
   end;
   suppose i2 = 0;
   hence thesis by Def8;
 end;
 end;

theorem
  i2 > 0 implies i1 mod i2 < i2
proof
  assume A1: i2 > 0;
  i1/i2 -1 < [\ i1/i2 /] by Def4;
  then (i1/i2 -1)*i2 < (i1 div i2)*i2 by A1,XREAL_1:70;
  then i1/i2*i2 -1*i2 < (i1 div i2)*i2;
  then i1 -i2 < (i1 div i2)*i2-0 by A1,XCMPLX_1:88;
  then i1 -(i1 div i2)*i2 < i2-0 by XREAL_1:19;
  hence thesis by A1,Def8;
end;

theorem
  i2 <> 0 implies i1 = (i1 div i2) * i2 + (i1 mod i2)
proof
  assume i2 <> 0;
  then (i1 div i2) * i2 +(i1 mod i2) =
  (i1 div i2 )*i2 + (i1 - ( i1 div i2 )*i2 ) by Def8  .= i1;
  hence thesis;
end;