Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Integers

by
Michal J. Trybulec

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;

```