:: Integers
:: by Micha{\l} J. Trybulec
::
:: Received February 7, 1990
:: Copyright (c) 1990-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, XREAL_0, ORDINAL1, ZFMISC_1, CARD_1, XBOOLE_0,
ARYTM_1, TARSKI, ARYTM_2, ARYTM_3, ARYTM_0, REAL_1, XXREAL_0, NAT_1,
RELAT_1, INT_1, FUNCT_7, XCMPLX_0;
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, REAL_1, NAT_1, FINSET_1,
CARD_1, XREAL_0, NUMBERS;
registrations ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, CARD_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin
reserve X for set, x,y,z for object,
k,l,n for Nat,
r for Real;
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 for Real;
cluster integer for number;
cluster -> integer for Element of INT;
end;
definition
mode Integer is integer Number;
end;
theorem :: INT_1:1
for k being natural Number st r = k or r = -k holds r is Integer;
theorem :: INT_1:2
r is Integer implies ex k st r = k or r = - k;
:: Relations between sets INT, NAT and REAL ( and their elements )
registration
cluster natural -> integer for object;
end;
registration
cluster integer -> real for object;
end;
reserve i,i0,i1,i2,i3,i4,i5,i8,i9,j for Integer;
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;
:: Some basic theorems about integers
theorem :: INT_1:3
0 <= i0 implies i0 in NAT;
theorem :: INT_1:4
r is Integer implies r + 1 is Integer & r - 1 is Integer;
theorem :: INT_1:5
i2 <= i1 implies i1 - i2 in NAT;
theorem :: INT_1:6
i1 + k = i2 implies i1 <= i2;
theorem :: INT_1:7
i0 < i1 implies i0 + 1 <= i1;
theorem :: INT_1:8
i1 < 0 implies i1 <= - 1;
theorem :: INT_1:9
i1 * i2 = 1 iff i1 = 1 & i2 = 1 or i1 = - 1 & i2 = - 1;
theorem :: INT_1:10
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];
:: The divisibility relation
definition
let i1,i2 be Integer;
pred i1 divides i2 means
:: INT_1:def 3
ex i3 st i2 = i1 * i3;
reflexivity;
end;
definition
let i1,i2,i3 be Integer;
pred i1,i2 are_congruent_mod i3 means
:: INT_1:def 4
i3 divides i1 - i2;
end;
definition
let i1,i2,i3 be Integer;
redefine pred i1,i2 are_congruent_mod i3 means
:: INT_1:def 5
ex i4 st i3 * i4 = i1 - i2;
end;
theorem :: INT_1:11
i1,i1 are_congruent_mod i2;
theorem :: INT_1:12
i1,0 are_congruent_mod i1 & 0,i1 are_congruent_mod i1;
theorem :: INT_1:13
i1,i2 are_congruent_mod 1;
theorem :: INT_1:14
i1,i2 are_congruent_mod i3 implies i2,i1 are_congruent_mod i3;
theorem :: INT_1:15
i1,i2 are_congruent_mod i5 & i2,i3 are_congruent_mod i5 implies
i1,i3 are_congruent_mod i5;
theorem :: INT_1:16
i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5 implies
(i1 + i3),(i2 + i4) are_congruent_mod i5;
theorem :: INT_1:17
i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5 implies
(i1 - i3),(i2 - i4) are_congruent_mod i5;
theorem :: INT_1:18
i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5 implies
(i1 * i3),(i2 * i4) are_congruent_mod i5;
theorem :: INT_1:19
(i1 + i2),i3 are_congruent_mod i5 iff i1, (i3 - i2) are_congruent_mod i5;
theorem :: INT_1:20
i4 * i5 = i3 implies (i1,i2 are_congruent_mod i3 implies
i1,i2 are_congruent_mod i4);
theorem :: INT_1:21
i1,i2 are_congruent_mod i5 iff (i1 + i5),i2 are_congruent_mod i5;
theorem :: INT_1:22
i1,i2 are_congruent_mod i5 iff (i1 - i5),i2 are_congruent_mod i5;
theorem :: INT_1:23
i1 <= r & r - 1 < i1 & i2 <= r & r - 1 < i2 implies i1 = i2;
theorem :: INT_1:24
r <= i1 & i1 < r + 1 & r <= i2 & i2 < r + 1 implies i1 = i2;
reserve r1,p,p1,g,g1,g2 for Real,
Y for Subset of REAL;
definition
let r be Real;
func [\ r /] -> Integer means
:: INT_1:def 6
it <= r & r - 1 < it;
projectivity;
end;
theorem :: INT_1:25
[\ r /] = r iff r is integer;
theorem :: INT_1:26
[\ r /] < r iff r is not integer;
theorem :: INT_1:27
[\ r /] - 1 < r & [\ r /] < r + 1;
theorem :: INT_1:28
[\ r /] + i0 = [\ r + i0 /];
theorem :: INT_1:29
r < [\ r /] + 1;
definition
let r be Real;
func [/ r \] -> Integer means
:: INT_1:def 7
r <= it & it < r + 1;
projectivity;
end;
theorem :: INT_1:30
[/ r \] = r iff r is integer;
theorem :: INT_1:31
r < [/ r \] iff r is not integer;
theorem :: INT_1:32
r - 1 < [/ r \] & r < [/ r \] + 1;
theorem :: INT_1:33
[/ r \] + i0 = [/ r + i0 \];
theorem :: INT_1:34
[\ r /] = [/ r \] iff r is integer;
theorem :: INT_1:35
[\ r /] < [/ r \] iff r is not integer;
theorem :: INT_1:36
[\ r /] <= [/ r \];
theorem :: INT_1:37
[\ ([/ r \]) /] = [/ r \];
::$CT 2
theorem :: INT_1:40
[/ ([\ r /]) \] = [\ r /];
theorem :: INT_1:41
[\ r /] = [/ r \] iff not [\ r /] + 1 = [/ r \];
definition
let r be Real;
func frac r -> set equals
:: INT_1:def 8
r - [\ r /];
end;
registration
let r be Real;
cluster frac r -> real;
end;
theorem :: INT_1:42
r = [\ r /] + frac r;
theorem :: INT_1:43
frac r < 1 & 0 <= frac r;
theorem :: INT_1:44
[\ frac r /] = 0;
theorem :: INT_1:45
frac r = 0 iff r is integer;
theorem :: INT_1:46
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 9
[\ i1 / i2 /];
end;
definition
let i1,i2 be Integer;
func i1 mod i2 -> Integer equals
:: INT_1:def 10
i1 - (i1 div i2) * i2 if i2 <> 0
otherwise 0;
end;
theorem :: INT_1:47
for r being Real st r <> 0 holds [\ r / r /] = 1;
theorem :: INT_1:48
for i being Integer holds i div 0 = 0;
theorem :: INT_1:49
for i being Integer st i <> 0 holds i div i = 1;
theorem :: INT_1:50
for i being Integer holds i mod i = 0;
begin :: Addenda
:: from FSM_1
theorem :: INT_1:51
for k, i being Integer holds
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:52
for a,b being Integer st a < b holds a <= b - 1;
:: from UNIFORM1, 2005.08.22, A.T.
theorem :: INT_1:53
for r being Real 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:54
for i being Integer, r being Real st i <= r holds i <= [\ r /];
theorem :: INT_1:55
for m,n being Nat holds 0 <= m qua Integer div n;
:: from SCMFSA9A, 2006.03.14, A.T.
theorem :: INT_1:56
0 < i & 1 < j implies i div j < i;
:: from NEWTON, 2007.01.02, AK
theorem :: INT_1:57
i2 >= 0 implies i1 mod i2 >= 0;
theorem :: INT_1:58
i2 > 0 implies i1 mod i2 < i2;
theorem :: INT_1:59
i2 <> 0 implies i1 = (i1 div i2) * i2 + (i1 mod i2);
:: from AMI_3, 2007.06.14, A.T.
theorem :: INT_1:60
for m,j being Integer holds m*j, 0 are_congruent_mod m;
:: from AMI_4, 2007.06.14, A.T.
theorem :: INT_1:61
i >= 0 & j >= 0 implies i div j >= 0;
:: from INT_3, 2007.07.27, A.T.
theorem :: INT_1:62
for n being Nat st n > 0 for a being Integer holds a mod n
= 0 iff n divides a;
:: from JORDAN1D, 2007.07.27, A.T.
reserve r, s for Real;
theorem :: INT_1:63
r/s is not Integer implies - [\ r/s /] = [\ (-r) / s /] + 1;
theorem :: INT_1:64
r/s is Integer implies - [\ r/s /] = [\ (-r) / s /];
:: missing, 2008.05.16, A.T.
theorem :: INT_1:65
r <= i implies [/ r \] <= i;
:: from POLYNOM2, 2010.02.13, A.T.
scheme :: INT_1:sch 7
FinInd{M, N() -> Element of NAT, P[Nat]} : for i being Element of NAT st M()
<= i & i <= N() holds P[i]
provided
P[M()] and
for j being Element of NAT st M() <= j & j < N() holds P[j] implies P[j+1];
scheme :: INT_1:sch 8
FinInd2{M,N() -> Element of NAT, P[Nat]} : for i being Element of NAT st M()
<= i & i <= N() holds P[i]
provided
P[M()] and
for j being Element of NAT st M() <= j & j < N() holds (for j9 being
Element of NAT st M() <= j9 & j9 <= j holds P[j9]) implies P[j+1];
:: from TOPREALA, 2011.04.27, A.T.
reserve i for Integer,
a, b, r, s for Real;
theorem :: INT_1:66
frac(r+i) = frac r;
theorem :: INT_1:67
r <= a & a < [\r/]+1 implies [\a/] = [\r/];
theorem :: INT_1:68
r <= a & a < [\r/]+1 implies frac r <= frac a;
theorem :: INT_1:69
r < a & a < [\r/]+1 implies frac r < frac a;
theorem :: INT_1:70
a >= [\r/]+1 & a <= r+1 implies [\a/] = [\r/]+1;
theorem :: INT_1:71
a >= [\r/]+1 & a < r+1 implies frac a < frac r;
theorem :: INT_1:72
r <= a & a < r+1 & r <= b & b < r+1 & frac a = frac b implies a = b;
:: 28.05.2012, A.T.
registration let i be Integer;
reduce In(i,INT) to i;
end;
definition let x be Number;
attr x is dim-like means
:: INT_1:def 11
x = -1 or x is natural;
end;
registration
cluster natural -> dim-like for object;
cluster dim-like -> integer for object;
cluster -1 -> dim-like for object;
end;
registration
cluster dim-like for set;
end;
registration let d be dim-like object;
cluster d + 1 -> natural;
end;
registration let k be dim-like object, n be non zero natural Number;
cluster k+n -> natural;
end;