W artykule wprowadzone zostały następujące pojęcia:
zbiór liczb całkowitych i jego elementy, kongruencje,
zaokrąglanie liczb rzeczywistych w dół i w górę, część ułamkowa liczby rzeczywistej,
dzielenie całkowite i reszta dzielenia całkowitego.
Dodane także następujące schematy: schemat rozdzielania,
schemat indukcji całkowitej, schematy minimum i maksimum
(istnienie najmniejszej i największej liczby całkowitej spełniającej zadaną własność).
Identyfikator Mizar Mathematical Library: INT_1.
Abstrakt w wersji PDF: tutaj.
Białystok, 1990.
Pliki:
:: 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 = ik & 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);
Góra
:: 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: g21 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 g21 in Y;
then consider r1 such that
A7: r1 in NAT and
A8: g21<r1 by A1,A3;
A9: g21+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 <= i11 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 = ik & 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;
r1<[\ r /] by Def4; then r1+1<[\ r /]+1 by XREAL_1:8;
then 01<[\ r /]+11 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: r1 < [\ r /] by Def4;
i1 <= r1 by A1,XREAL_1:11;
then i1 < [\ r /] by A2,XXREAL_0:2;
then i1+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)*i20 by A1,XCMPLX_1:88;
then i1 (i1 div i2)*i2 < i20 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;
Góra
