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


begin

Lm1:  for z being set st z in [:{0},NAT:] \ {[0,0]} holds
ex k being Element of NAT st z = - k
proofend;

Lm2:  for x being set
for k being Element of NAT st x = - k &amp; k <> x holds
x in [:{0},NAT:] \ {[0,0]}
proofend;

definition
redefine func INT  means :Def1: :: INT_1:def 1
 for x being set holds
( x in it iff ex k being Element of NAT st
( x = k or x = - k ) );
compatibility
 for b1 being set holds
( b1 = INT iff for x being set holds
( x in b1 iff ex k being Element of NAT st
( x = k or x = - k ) ) )
proofend;
end;

:: deftheorem Def1 defines INT INT_1:def_1_:_
 for b1 being set holds
( b1 = INT iff for x being set holds
( x in b1 iff ex k being Element of NAT st
( x = k or x = - k ) ) );

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

:: deftheorem Def2 defines integer INT_1:def_2_:_
 for i being number holds
( i is integer iff i in INT );

registration
cluster ext-real V31() real integer for Element of REAL ;
existence
 ex b1 being Real st b1 is integer
proofend;
cluster integer for set ;
existence
 ex b1 being number st b1 is integer
proofend;
cluster  ->  integer for Element of INT ;
coherence
 for b1 being Element of INT holds b1 is integer by Def2;
end;

definition
mode Integer is integer number ;
end;

theorem Th1: :: INT_1:1
for r being real number
for k being Nat st ( r = k or r = - k ) holds
r is Integer
proofend;

theorem Th2: :: INT_1:2
for r being real number st r is Integer holds
ex k being Element of NAT st
( r = k or r = - k )
proofend;

:: Relations between sets INT, NAT and REAL ( and their elements )
registration
cluster natural  ->  integer for set ;
coherence
 for b1 being number st b1 is natural holds
b1 is integer by Th1;
end;

Lm3:  for x being set st x in INT holds
x in REAL
by NUMBERS:15;

registration
cluster integer  ->  real for set ;
coherence
 for b1 being number st b1 is integer holds
b1 is real
proofend;
end;

registration
let i1, i2 be Integer;
clusteri1 + i2 ->  integer ;
coherence
 i1 + i2 is integer
proofend;
clusteri1 * i2 ->  integer ;
coherence
 i1 * i2 is integer
proofend;
end;

registration
let i0 be Integer;
cluster - i0 ->  integer ;
coherence
 - i0 is integer
proofend;
end;

registration
let i1, i2 be Integer;
clusteri1 - i2 ->  integer ;
coherence
 i1 - i2 is integer
proofend;
end;

:: Some basic theorems about integers
theorem Th3: :: INT_1:3
for i0 being Integer st 0 <= i0 holds
i0 in NAT
proofend;

theorem :: INT_1:4
for r being real number st r is Integer holds
( r + 1 is Integer &amp; r - 1 is Integer ) ;

theorem Th5: :: INT_1:5
for i2, i1 being Integer st i2 <= i1 holds
i1 - i2 in NAT
proofend;

theorem Th6: :: INT_1:6
for k being Element of NAT
for i1, i2 being Integer st i1 + k = i2 holds
i1 <= i2
proofend;

Lm4:  for j being Element of NAT st j < 1 holds
j = 0
proofend;

Lm5:  for i1 being Integer st 0 < i1 holds
1 <= i1
proofend;

theorem Th7: :: INT_1:7
for i0, i1 being Integer st i0 < i1 holds
i0 + 1 <= i1
proofend;

theorem Th8: :: INT_1:8
for i1 being Integer st i1 < 0 holds
i1 <= - 1
proofend;

theorem Th9: :: INT_1:9
for i1, i2 being Integer holds
( i1 * i2 = 1 iff ( ( i1 = 1 &amp; i2 = 1 ) or ( i1 = - 1 &amp; i2 = - 1 ) ) )
proofend;

theorem :: INT_1:10
for i1, i2 being Integer holds
( i1 * i2 = - 1 iff ( ( i1 = - 1 &amp; i2 = 1 ) or ( i1 = 1 &amp; i2 = - 1 ) ) )
proofend;

Lm6:  for i0, i1 being Integer st i0 <= i1 holds
ex k being Element of NAT st i0 + k = i1
proofend;

Lm7:  for i0, i1 being Integer st i0 <= i1 holds
ex k being Element of NAT st i1 - k = i0
proofend;

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

scheme :: INT_1:sch 2
IntIndUp{ F1() ->  Integer, P1[ Integer] } :
 for i0 being Integer st F1() <= i0 holds
P1[i0]
provided
A1: P1[F1()] and
A2: for i2 being Integer st F1() <= i2 &amp; P1[i2] holds
P1[i2 + 1]
proofend;

scheme :: INT_1:sch 3
IntIndDown{ F1() ->  Integer, P1[ Integer] } :
 for i0 being Integer st i0 <= F1() holds
P1[i0]
provided
A1: P1[F1()] and
A2: for i2 being Integer st i2 <= F1() &amp; P1[i2] holds
P1[i2 - 1]
proofend;

scheme :: INT_1:sch 4
IntIndFull{ F1() ->  Integer, P1[ Integer] } :
 for i0 being Integer holds P1[i0]
provided
A1: P1[F1()] and
A2: for i2 being Integer st P1[i2] holds
( P1[i2 - 1] &amp; P1[i2 + 1] )
proofend;

scheme :: INT_1:sch 5
IntMin{ F1() ->  Integer, P1[ Integer] } :
 ex i0 being Integer st
( P1[i0] &amp; ( for i1 being Integer st P1[i1] holds
i0 <= i1 ) )
provided
A1: for i1 being Integer st P1[i1] holds
F1() <= i1 and
A2: ex i1 being Integer st P1[i1]
proofend;

scheme :: INT_1:sch 6
IntMax{ F1() ->  Integer, P1[ Integer] } :
 ex i0 being Integer st
( P1[i0] &amp; ( for i1 being Integer st P1[i1] holds
i1 <= i0 ) )
provided
A1: for i1 being Integer st P1[i1] holds
i1 <= F1() and
A2: ex i1 being Integer st P1[i1]
proofend;

:: The divisibility relation
definition
let i1, i2 be Integer;
predi1 divides i2 means :Def3: :: INT_1:def 3
 ex i3 being Integer st i2 = i1 * i3;
reflexivity
 for i1 being Integer ex i3 being Integer st i1 = i1 * i3
proofend;
end;

:: deftheorem Def3 defines divides INT_1:def_3_:_
 for i1, i2 being Integer holds
( i1 divides i2 iff ex i3 being Integer st i2 = i1 * i3 );

definition
let i1, i2, i3 be Integer;
predi1,i2 are_congruent_mod i3 means :: INT_1:def 4
i3 divides i1 - i2;
end;

:: deftheorem  defines are_congruent_mod INT_1:def_4_:_
 for i1, i2, i3 being Integer holds
( i1,i2 are_congruent_mod i3 iff i3 divides i1 - i2 );

definition
let i1, i2, i3 be Integer;
redefine pred i1,i2 are_congruent_mod i3 means :Def5: :: INT_1:def 5
 ex i4 being Integer st i3 * i4 = i1 - i2;
compatibility
 ( i1,i2 are_congruent_mod i3 iff ex i4 being Integer st i3 * i4 = i1 - i2 )
proofend;
end;

:: deftheorem Def5 defines are_congruent_mod INT_1:def_5_:_
 for i1, i2, i3 being Integer holds
( i1,i2 are_congruent_mod i3 iff ex i4 being Integer st i3 * i4 = i1 - i2 );

theorem :: INT_1:11
for i1, i2 being Integer holds i1,i1 are_congruent_mod i2
proofend;

theorem :: INT_1:12
for i1 being Integer holds
( i1, 0 are_congruent_mod i1 &amp; 0 ,i1 are_congruent_mod i1 )
proofend;

theorem :: INT_1:13
for i1, i2 being Integer holds i1,i2 are_congruent_mod 1
proofend;

theorem :: INT_1:14
for i1, i2, i3 being Integer st i1,i2 are_congruent_mod i3 holds
i2,i1 are_congruent_mod i3
proofend;

theorem :: INT_1:15
for i1, i2, i5, i3 being Integer st i1,i2 are_congruent_mod i5 &amp; i2,i3 are_congruent_mod i5 holds
i1,i3 are_congruent_mod i5
proofend;

theorem :: INT_1:16
for i1, i2, i5, i3, i4 being Integer st i1,i2 are_congruent_mod i5 &amp; i3,i4 are_congruent_mod i5 holds
i1 + i3,i2 + i4 are_congruent_mod i5
proofend;

theorem :: INT_1:17
for i1, i2, i5, i3, i4 being Integer st i1,i2 are_congruent_mod i5 &amp; i3,i4 are_congruent_mod i5 holds
i1 - i3,i2 - i4 are_congruent_mod i5
proofend;

theorem :: INT_1:18
for i1, i2, i5, i3, i4 being Integer st i1,i2 are_congruent_mod i5 &amp; i3,i4 are_congruent_mod i5 holds
i1 * i3,i2 * i4 are_congruent_mod i5
proofend;

theorem :: INT_1:19
for i1, i2, i3, i5 being Integer holds
( i1 + i2,i3 are_congruent_mod i5 iff i1,i3 - i2 are_congruent_mod i5 )
proofend;

theorem :: INT_1:20
for i4, i5, i3, i1, i2 being Integer st i4 * i5 = i3 &amp; i1,i2 are_congruent_mod i3 holds
i1,i2 are_congruent_mod i4
proofend;

theorem :: INT_1:21
for i1, i2, i5 being Integer holds
( i1,i2 are_congruent_mod i5 iff i1 + i5,i2 are_congruent_mod i5 )
proofend;

theorem :: INT_1:22
for i1, i2, i5 being Integer holds
( i1,i2 are_congruent_mod i5 iff i1 - i5,i2 are_congruent_mod i5 )
proofend;

theorem Th23: :: INT_1:23
for r being real number
for i1, i2 being Integer st i1 <= r &amp; r - 1 < i1 &amp; i2 <= r &amp; r - 1 < i2 holds
i1 = i2
proofend;

theorem Th24: :: INT_1:24
for r being real number
for i1, i2 being Integer st r <= i1 &amp; i1 < r + 1 &amp; r <= i2 &amp; i2 < r + 1 holds
i1 = i2
proofend;

Lm8:  for r being real number ex n being Element of NAT st r < n
proofend;

definition
let r be real number ;
func[\r/] ->  Integer means :Def6: :: INT_1:def 6
( it <= r &amp; r - 1 < it );
existence
 ex b1 being Integer st
( b1 <= r &amp; r - 1 < b1 )
proofend;
uniqueness
 for b1, b2 being Integer st b1 <= r &amp; r - 1 < b1 &amp; b2 <= r &amp; r - 1 < b2 holds
b1 = b2 by Th23;
projectivity
 for b1 being Integer
for b2 being real number st b1 <= b2 &amp; b2 - 1 < b1 holds
( b1 <= b1 &amp; b1 - 1 < b1 ) by XREAL_1:44;
end;

:: deftheorem Def6 defines [\ INT_1:def_6_:_
 for r being real number
for b2 being Integer holds
( b2 = [\r/] iff ( b2 <= r &amp; r - 1 < b2 ) );

theorem Th25: :: INT_1:25
for r being real number holds
( [\r/] = r iff r is integer )
proofend;

theorem Th26: :: INT_1:26
for r being real number holds
( [\r/] < r iff not r is integer )
proofend;

theorem :: INT_1:27
for r being real number holds
( [\r/] - 1 < r &amp; [\r/] < r + 1 )
proofend;

theorem Th28: :: INT_1:28
for r being real number
for i0 being Integer holds [\r/] + i0 = [\(r + i0)/]
proofend;

theorem Th29: :: INT_1:29
for r being real number holds r < [\r/] + 1
proofend;

definition
let r be real number ;
func[/r\] ->  Integer means :Def7: :: INT_1:def 7
( r <= it &amp; it < r + 1 );
existence
 ex b1 being Integer st
( r <= b1 &amp; b1 < r + 1 )
proofend;
uniqueness
 for b1, b2 being Integer st r <= b1 &amp; b1 < r + 1 &amp; r <= b2 &amp; b2 < r + 1 holds
b1 = b2 by Th24;
projectivity
 for b1 being Integer
for b2 being real number st b2 <= b1 &amp; b1 < b2 + 1 holds
( b1 <= b1 &amp; b1 < b1 + 1 ) by XREAL_1:29;
end;

:: deftheorem Def7 defines [/ INT_1:def_7_:_
 for r being real number
for b2 being Integer holds
( b2 = [/r\] iff ( r <= b2 &amp; b2 < r + 1 ) );

theorem Th30: :: INT_1:30
for r being real number holds
( [/r\] = r iff r is integer )
proofend;

theorem Th31: :: INT_1:31
for r being real number holds
( r < [/r\] iff not r is integer )
proofend;

theorem :: INT_1:32
for r being real number holds
( r - 1 < [/r\] &amp; r < [/r\] + 1 )
proofend;

theorem :: INT_1:33
for r being real number
for i0 being Integer holds [/r\] + i0 = [/(r + i0)\]
proofend;

theorem Th34: :: INT_1:34
for r being real number holds
( [\r/] = [/r\] iff r is integer )
proofend;

theorem Th35: :: INT_1:35
for r being real number holds
( [\r/] < [/r\] iff not r is integer )
proofend;

theorem :: INT_1:36
for r being real number holds [\r/] <= [/r\]
proofend;

theorem :: INT_1:37
for r being real number holds [\[/r\]/] = [/r\] by Th25;

theorem :: INT_1:38
canceled;

theorem :: INT_1:39
canceled;

theorem :: INT_1:40
for r being real number holds [/[\r/]\] = [\r/] by Th30;

theorem :: INT_1:41
for r being real number holds
( [\r/] = [/r\] iff not [\r/] + 1 = [/r\] )
proofend;

definition
let r be real number ;
func frac r ->  set  equals :: INT_1:def 8
r - [\r/];
coherence
 r - [\r/] is set ;
end;

:: deftheorem  defines frac INT_1:def_8_:_
 for r being real number holds frac r = r - [\r/];

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

definition
let r be real number ;
:: original:frac
redefine func frac r ->  Real;
coherence
 frac r is Real by XREAL_0:def_1;
end;

theorem :: INT_1:42
for r being real number holds r = [\r/] + (frac r) ;

theorem Th43: :: INT_1:43
for r being real number holds
( frac r < 1 &amp; 0 <= frac r )
proofend;

theorem :: INT_1:44
for r being real number holds [\(frac r)/] = 0
proofend;

theorem Th45: :: INT_1:45
for r being real number holds
( frac r = 0 iff r is integer )
proofend;

theorem :: INT_1:46
for r being real number holds
( 0 < frac r iff not r is integer )
proofend;

:: Functions div and mod
definition
let i1, i2 be Integer;
funci1 div i2 ->  Integer equals :: INT_1:def 9
[\(i1 / i2)/];
correctness
coherence
[\(i1 / i2)/] is Integer;
;
end;

:: deftheorem  defines div INT_1:def_9_:_
 for i1, i2 being Integer holds i1 div i2 = [\(i1 / i2)/];

definition
let i1, i2 be Integer;
funci1 mod i2 ->  Integer equals :Def10: :: INT_1:def 10
i1 - ((i1 div i2) * i2) if i2 <> 0
otherwise  0 ;
correctness
coherence
( ( i2 <> 0 implies i1 - ((i1 div i2) * i2) is Integer ) &amp; ( not i2 <> 0 implies 0 is Integer ) );
consistency
for b1 being Integer holds verum;
;
end;

:: deftheorem Def10 defines mod INT_1:def_10_:_
 for i1, i2 being Integer holds
( ( i2 <> 0 implies i1 mod i2 = i1 - ((i1 div i2) * i2) ) &amp; ( not i2 <> 0 implies i1 mod i2 = 0 ) );

theorem Th47: :: INT_1:47
for r being real number st r <> 0 holds
[\(r / r)/] = 1
proofend;

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

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

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

begin

:: from FSM_1
theorem :: INT_1:51
for k, i being Integer st k < i holds
ex j being Element of NAT st
( j = i - k &amp; 1 <= j )
proofend;

:: from SCMFSA_7, 2005.02.05, A.T.
theorem Th52: :: INT_1:52
for a, b being Integer st a < b holds
a <= b - 1
proofend;

:: from UNIFORM1, 2005.08.22, A.T.
theorem :: INT_1:53
for r being real number st r >= 0 holds
( [/r\] >= 0 &amp; [\r/] >= 0 &amp; [/r\] is Element of NAT &amp; [\r/] is Element of NAT )
proofend;

:: from SCMFSA9A, 2005.11.16, A.T.
theorem Th54: :: INT_1:54
for i being Integer
for r being real number st i <= r holds
i <= [\r/]
proofend;

theorem :: INT_1:55
for m, n being Nat holds 0 <= m div n by Th54;

:: from SCMFSA9A, 2006.03.14, A.T.
theorem :: INT_1:56
for i, j being Integer st 0 < i &amp; 1 < j holds
i div j < i
proofend;

:: from NEWTON, 2007.01.02, AK
theorem :: INT_1:57
for i2, i1 being Integer st i2 >= 0 holds
i1 mod i2 >= 0
proofend;

theorem :: INT_1:58
for i2, i1 being Integer st i2 > 0 holds
i1 mod i2 < i2
proofend;

theorem :: INT_1:59
for i2, i1 being Integer st i2 <> 0 holds
i1 = ((i1 div i2) * i2) + (i1 mod i2)
proofend;

:: 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
proofend;

:: from AMI_4, 2007.06.14, A.T.
theorem :: INT_1:61
for i, j being Integer st i >= 0 &amp; j >= 0 holds
i div j >= 0
proofend;

:: from INT_3, 2007.07.27, A.T.
theorem :: INT_1:62
for n being Nat st n > 0 holds
for a being Integer holds
( a mod n = 0 iff n divides a )
proofend;

theorem :: INT_1:63
for r, s being real number st r / s is not Integer holds
- [\(r / s)/] = [\((- r) / s)/] + 1
proofend;

theorem :: INT_1:64
for r, s being real number st r / s is Integer holds
- [\(r / s)/] = [\((- r) / s)/]
proofend;

:: missing, 2008.05.16, A.T.
theorem :: INT_1:65
for i being Integer
for r being real number st r <= i holds
[/r\] <= i
proofend;

scheme :: INT_1:sch 7
FinInd{ F1() ->  Element of NAT , F2() ->  Element of NAT , P1[ Nat] } :
 for i being Element of NAT st F1() <= i &amp; i <= F2() holds
P1[i]
provided
A1: P1[F1()] and
A2: for j being Element of NAT st F1() <= j &amp; j < F2() &amp; P1[j] holds
P1[j + 1]
proofend;

scheme :: INT_1:sch 8
FinInd2{ F1() ->  Element of NAT , F2() ->  Element of NAT , P1[ Nat] } :
 for i being Element of NAT st F1() <= i &amp; i <= F2() holds
P1[i]
provided
A1: P1[F1()] and
A2: for j being Element of NAT st F1() <= j &amp; j < F2() &amp; ( for j9 being Element of NAT st F1() <= j9 &amp; j9 <= j holds
P1[j9] ) holds
P1[j + 1]
proofend;

theorem :: INT_1:66
for i being Integer
for r being real number holds frac (r + i) = frac r
proofend;

theorem Th67: :: INT_1:67
for r, a being real number st r <= a &amp; a < [\r/] + 1 holds
[\a/] = [\r/]
proofend;

theorem Th68: :: INT_1:68
for r, a being real number st r <= a &amp; a < [\r/] + 1 holds
frac r <= frac a
proofend;

theorem :: INT_1:69
for r, a being real number st r < a &amp; a < [\r/] + 1 holds
frac r < frac a
proofend;

theorem Th70: :: INT_1:70
for a, r being real number st a >= [\r/] + 1 &amp; a <= r + 1 holds
[\a/] = [\r/] + 1
proofend;

theorem Th71: :: INT_1:71
for a, r being real number st a >= [\r/] + 1 &amp; a < r + 1 holds
frac a < frac r
proofend;

theorem :: INT_1:72
for r, a, b being real number st r <= a &amp; a < r + 1 &amp; r <= b &amp; b < r + 1 &amp; frac a = frac b holds
a = b
proofend;