The abstract of the Mizar article:

Integers

by

Michal J. Trybulec

Received February 7, 1990

MML identifier: INT_1

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM, ARYTM_1, ORDINAL2, ABSVALUE, NAT_1, ARYTM_3, RELAT_1, INT_1,
      BOOLE, COMPLEX1, ARYTM_2, XCMPLX_0;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ORDINAL2, ARYTM_2,
      ARYTM_1, NUMBERS, ARYTM_0, XCMPLX_0, XREAL_0, REAL_1, ABSVALUE, NAT_1;
 constructors REAL_1, ABSVALUE, NAT_1, XCMPLX_0, XREAL_0, XBOOLE_0, ARYTM_0,
      ARYTM_3, ARYTM_2, FUNCT_4, ARYTM_1;
 clusters XREAL_0, ARYTM_3, REAL_1, ORDINAL2, NUMBERS, ZFMISC_1, XBOOLE_0,
      XCMPLX_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

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

definition
 cluster -> complex Element of COMPLEX;
end;

 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 is Element of INT;
 end;

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

definition
  mode Integer is integer number;
end;

canceled 7;

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

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

definition
 cluster -> integer Nat;
 cluster natural -> integer number;
end;

canceled 2;

 theorem :: INT_1:11
  x in INT implies x in REAL;

definition
 cluster integer -> real number;
end;

 theorem :: INT_1:12
  x is Integer iff x in INT;

canceled;

 theorem :: INT_1:14
    NAT c= INT;

 theorem :: INT_1:15
    INT c= REAL;

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

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

 definition
  let i1,i2 be Integer;
   cluster i1 + i2 -> integer;

   cluster i1 * i2 -> integer;
 end;

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

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

:: More redefinitions

 definition
  let n be Nat;
   cluster - n -> integer;
  let i1 be Integer;
   cluster i1 + n -> integer;
   cluster i1 * n -> integer;
   cluster i1 - n -> integer;
 end;

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

:: Some basic theorems about integers

 theorem :: INT_1:16
  0 <= i0 implies i0 is 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 is 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);

canceled 2;

 theorem :: INT_1:26
  r - 1 < r;

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

scheme Int_Ind_Up { 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_Ind_Down { 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_Ind_Full { 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_Min { 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_Max { 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

 definition
  let r;
   cluster sgn r -> integer;
 end;

canceled 2;

 theorem :: INT_1:29
    sgn r = 1 or sgn r = - 1 or sgn r = 0;

 theorem :: INT_1:30
  abs r = r or abs r = - r;

 definition
  let i0;
   cluster abs i0 -> integer;
 end;

:: Congruences

 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;

 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,
        X,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;

 definition
  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;