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

Lm1: for z being object st z in [:{0},NAT:] \ {[0,0]} holds
ex k being Nat st z = - k

proof end;

Lm2: for x being object
for k being Nat st x = - k & k <> x holds
x in [:{0},NAT:] \ {[0,0]}

proof end;

definition

redefine func INT means :Def1: :: INT_1:def 1
for x being object holds
( x in it iff ex k being Nat st
( x = k or x = - k ) );

compatibility
for b₁ being set holds
( b₁ = INT iff for x being object holds
( x in b₁ iff ex k being Nat st
( x = k or x = - k ) ) )

proof end;

end;

:: deftheorem Def1 defines INT INT_1:def 1 :
for b₁ being set holds
( b₁ = INT iff for x being object holds
( x in b₁ iff ex k being Nat st
( x = k or x = - k ) ) );

definition

let i be Number ;

attr i 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 complex real integer for object ;

existence
ex b₁ being Real st b₁ is integer

proof end;

cluster integer for set ;

existence
ex b₁ being number st b₁ is integer

proof end;

cluster -> integer for Element of INT ;

coherence
for b₁ being Element of INT holds b₁ is integer ;

end;

definition

mode Integer is integer Number ;

end;

theorem Th1: :: INT_1:1

for r being Real
for k being natural Number st ( r = k or r = - k ) holds
r is Integer

proof end;

theorem Th2: :: INT_1:2

for r being Real st r is Integer holds
ex k being Nat st
( r = k or r = - k )

proof end;

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

registration

cluster natural -> integer for object ;

coherence
for b₁ being object st b₁ is natural holds
b₁ is integer by Th1;

end;

registration

cluster integer -> real for object ;

coherence
for b₁ being object st b₁ is integer holds
b₁ is real by NUMBERS:15;

end;

registration

let i1, i2 be Integer;

cluster i1 + i2 -> integer ;

coherence
i1 + i2 is integer

proof end;

cluster i1 * i2 -> integer ;

coherence
i1 * i2 is integer

proof end;

end;

registration

let i0 be Integer;

cluster - i0 -> integer ;

coherence
- i0 is integer

proof end;

end;

registration

let i1, i2 be Integer;

cluster i1 - i2 -> integer ;

coherence
i1 - i2 is integer

proof end;

end;

:: Some basic theorems about integers

theorem Th3: :: INT_1:3

for i0 being Integer st 0 <= i0 holds
i0 in NAT

proof end;

theorem :: INT_1:4

for r being Real st r is Integer holds
( r + 1 is Integer & r - 1 is Integer ) ;

theorem Th5: :: INT_1:5

for i1, i2 being Integer st i2 <= i1 holds
i1 - i2 in NAT

proof end;

theorem Th6: :: INT_1:6

for k being Nat
for i1, i2 being Integer st i1 + k = i2 holds
i1 <= i2

proof end;

Lm3: for j being Element of NAT st j < 1 holds
j = 0

proof end;

Lm4: for i1 being Integer st 0 < i1 holds
1 <= i1

proof end;

theorem Th7: :: INT_1:7

for i0, i1 being Integer st i0 < i1 holds
i0 + 1 <= i1

proof end;

theorem Th8: :: INT_1:8

for i1 being Integer st i1 < 0 holds
i1 <= - 1

proof end;

theorem Th9: :: INT_1:9

for i1, i2 being Integer holds
( i1 * i2 = 1 iff ( ( i1 = 1 & i2 = 1 ) or ( i1 = - 1 & i2 = - 1 ) ) )

proof end;

theorem :: INT_1:10

for i1, i2 being Integer holds
( i1 * i2 = - 1 iff ( ( i1 = - 1 & i2 = 1 ) or ( i1 = 1 & i2 = - 1 ) ) )

proof end;

Lm5: for i0, i1 being Integer st i0 <= i1 holds
ex k being Nat st i0 + k = i1

proof end;

Lm6: for i0, i1 being Integer st i0 <= i1 holds
ex k being Nat st i1 - k = i0

proof end;

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] )

proof end;

scheme :: INT_1:sch 2
IntIndUp{ F₁() -> Integer, P₁[ Integer] } :

for i0 being Integer st F₁() <= i0 holds
P₁[i0]

provided

A1: P₁[F₁()] and
A2: for i2 being Integer st F₁() <= i2 & P₁[i2] holds
P₁[i2 + 1]

proof end;

scheme :: INT_1:sch 3
IntIndDown{ F₁() -> Integer, P₁[ Integer] } :

for i0 being Integer st i0 <= F₁() holds
P₁[i0]

provided

A1: P₁[F₁()] and
A2: for i2 being Integer st i2 <= F₁() & P₁[i2] holds
P₁[i2 - 1]

proof end;

scheme :: INT_1:sch 4
IntIndFull{ F₁() -> Integer, P₁[ Integer] } :

for i0 being Integer holds P₁[i0]

provided

A1: P₁[F₁()] and
A2: for i2 being Integer st P₁[i2] holds
( P₁[i2 - 1] & P₁[i2 + 1] )

proof end;

scheme :: INT_1:sch 5
IntMin{ F₁() -> Integer, P₁[ Integer] } :

ex i0 being Integer st
( P₁[i0] & ( for i1 being Integer st P₁[i1] holds
i0 <= i1 ) )

provided

A1: for i1 being Integer st P₁[i1] holds
F₁() <= i1 and
A2: ex i1 being Integer st P₁[i1]

proof end;

scheme :: INT_1:sch 6
IntMax{ F₁() -> Integer, P₁[ Integer] } :

ex i0 being Integer st
( P₁[i0] & ( for i1 being Integer st P₁[i1] holds
i1 <= i0 ) )

provided

A1: for i1 being Integer st P₁[i1] holds
i1 <= F₁() and
A2: ex i1 being Integer st P₁[i1]

proof end;

:: The divisibility relation

definition

let i1, i2 be Integer;

pred i1 divides i2 means :: 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

proof end;

end;

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

pred i1,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 :: 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 )

proof end;

end;

:: deftheorem 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

proof end;

theorem :: INT_1:12

for i1 being Integer holds
( i1, 0 are_congruent_mod i1 & 0 ,i1 are_congruent_mod i1 )

proof end;

theorem :: INT_1:13

for i1, i2 being Integer holds i1,i2 are_congruent_mod 1

proof end;

theorem :: INT_1:14

for i1, i2, i3 being Integer st i1,i2 are_congruent_mod i3 holds
i2,i1 are_congruent_mod i3

proof end;

theorem :: INT_1:15

for i1, i2, i3, i5 being Integer st i1,i2 are_congruent_mod i5 & i2,i3 are_congruent_mod i5 holds
i1,i3 are_congruent_mod i5

proof end;

theorem :: INT_1:16

for i1, i2, i3, i4, i5 being Integer st i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5 holds
i1 + i3,i2 + i4 are_congruent_mod i5

proof end;

theorem :: INT_1:17

for i1, i2, i3, i4, i5 being Integer st i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5 holds
i1 - i3,i2 - i4 are_congruent_mod i5

proof end;

theorem :: INT_1:18

for i1, i2, i3, i4, i5 being Integer st i1,i2 are_congruent_mod i5 & i3,i4 are_congruent_mod i5 holds
i1 * i3,i2 * i4 are_congruent_mod i5

proof end;

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

theorem :: INT_1:20

for i1, i2, i3, i4, i5 being Integer st i4 * i5 = i3 & i1,i2 are_congruent_mod i3 holds
i1,i2 are_congruent_mod i4

proof end;

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 )

proof end;

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 )

proof end;

theorem Th23: :: INT_1:23

for r being Real
for i1, i2 being Integer st i1 <= r & r - 1 < i1 & i2 <= r & r - 1 < i2 holds
i1 = i2

proof end;

theorem Th24: :: INT_1:24

for r being Real
for i1, i2 being Integer st r <= i1 & i1 < r + 1 & r <= i2 & i2 < r + 1 holds
i1 = i2

proof end;

Lm7: for r being Real ex n being Nat st r < n

proof end;

definition

let r be Real;

func [\r/] -> Integer means :Def6: :: INT_1:def 6
( it <= r & r - 1 < it );

existence
ex b₁ being Integer st
( b₁ <= r & r - 1 < b₁ )

proof end;

uniqueness
for b₁, b₂ being Integer st b₁ <= r & r - 1 < b₁ & b₂ <= r & r - 1 < b₂ holds
b₁ = b₂ by Th23;
projectivity
for b₁ being Integer
for b₂ being Real st b₁ <= b₂ & b₂ - 1 < b₁ holds
( b₁ <= b₁ & b₁ - 1 < b₁ ) by XREAL_1:44;

end;

:: deftheorem Def6 defines [\ INT_1:def 6 :
for r being Real
for b₂ being Integer holds
( b₂ = [\r/] iff ( b₂ <= r & r - 1 < b₂ ) );

theorem Th25: :: INT_1:25

for r being Real holds
( [\r/] = r iff r is integer )

proof end;

theorem Th26: :: INT_1:26

for r being Real holds
( [\r/] < r iff not r is integer )

proof end;

theorem :: INT_1:27

for r being Real holds
( [\r/] - 1 < r & [\r/] < r + 1 )

proof end;

theorem Th28: :: INT_1:28

for r being Real
for i0 being Integer holds [\r/] + i0 = [\(r + i0)/]

proof end;

theorem Th29: :: INT_1:29

for r being Real holds r < [\r/] + 1

proof end;

definition

let r be Real;

func [/r\] -> Integer means :Def7: :: INT_1:def 7
( r <= it & it < r + 1 );

existence
ex b₁ being Integer st
( r <= b₁ & b₁ < r + 1 )

proof end;

uniqueness
for b₁, b₂ being Integer st r <= b₁ & b₁ < r + 1 & r <= b₂ & b₂ < r + 1 holds
b₁ = b₂ by Th24;
projectivity
for b₁ being Integer
for b₂ being Real st b₂ <= b₁ & b₁ < b₂ + 1 holds
( b₁ <= b₁ & b₁ < b₁ + 1 ) by XREAL_1:29;

end;

:: deftheorem Def7 defines [/ INT_1:def 7 :
for r being Real
for b₂ being Integer holds
( b₂ = [/r\] iff ( r <= b₂ & b₂ < r + 1 ) );

theorem Th30: :: INT_1:30

for r being Real holds
( [/r\] = r iff r is integer )

proof end;

theorem Th31: :: INT_1:31

for r being Real holds
( r < [/r\] iff not r is integer )

proof end;

theorem :: INT_1:32

for r being Real holds
( r - 1 < [/r\] & r < [/r\] + 1 )

proof end;

theorem :: INT_1:33

for r being Real
for i0 being Integer holds [/r\] + i0 = [/(r + i0)\]

proof end;

theorem Th34: :: INT_1:34

for r being Real holds
( [\r/] = [/r\] iff r is integer )

proof end;

theorem Th35: :: INT_1:35

for r being Real holds
( [\r/] < [/r\] iff not r is integer )

proof end;

theorem :: INT_1:36

for r being Real holds [\r/] <= [/r\]

proof end;

theorem :: INT_1:37

for r being Real holds [\[/r\]/] = [/r\] by Th25;

theorem :: INT_1:38

canceled;

theorem :: INT_1:39

canceled;

::$CT 2

theorem :: INT_1:40

for r being Real holds [/[\r/]\] = [\r/] by Th30;

theorem :: INT_1:41

for r being Real holds
( [\r/] = [/r\] iff not [\r/] + 1 = [/r\] )

proof end;

definition

let r be Real;

func frac r -> number equals :: INT_1:def 8
r - [\r/];

coherence
r - [\r/] is number ;

end;

:: deftheorem defines frac INT_1:def 8 :
for r being Real holds frac r = r - [\r/];

registration

let r be Real;

cluster frac r -> real ;

coherence
frac r is real ;

end;

theorem :: INT_1:42

for r being Real holds r = [\r/] + (frac r) ;

theorem Th41: :: INT_1:43

for r being Real holds
( frac r < 1 & 0 <= frac r )

proof end;

theorem :: INT_1:44

for r being Real holds [\(frac r)/] = 0

proof end;

theorem Th43: :: INT_1:45

for r being Real holds
( frac r = 0 iff r is integer )

proof end;

theorem :: INT_1:46

for r being Real holds
( 0 < frac r iff not r is integer )

proof end;

:: Functions div and mod

definition

let i1, i2 be Integer;

func i1 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;

func i1 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 ) & ( not i2 <> 0 implies 0 is Integer ) );
consistency
for b₁ 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) ) & ( not i2 <> 0 implies i1 mod i2 = 0 ) );

theorem Th45: :: INT_1:47

for r being Real st r <> 0 holds
[\(r / r)/] = 1

proof end;

theorem :: INT_1:48

for i being Integer holds i div 0 = 0

proof end;

theorem :: INT_1:49

for i being Integer st i <> 0 holds
i div i = 1 by Th45;

theorem :: INT_1:50

for i being Integer holds i mod i = 0

proof end;

:: 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 & 1 <= j )

proof end;

:: from SCMFSA_7, 2005.02.05, A.T.

theorem Th50: :: INT_1:52

for a, b being Integer st a < b holds
a <= b - 1

proof end;

:: 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 )

proof end;

:: from SCMFSA9A, 2005.11.16, A.T.

theorem Th52: :: INT_1:54

for i being Integer
for r being Real st i <= r holds
i <= [\r/]

proof end;

theorem :: INT_1:55

for m, n being Nat holds 0 <= m div n by Th52;

:: from SCMFSA9A, 2006.03.14, A.T.

theorem :: INT_1:56

for i, j being Integer st 0 < i & 1 < j holds
i div j < i

proof end;

:: from NEWTON, 2007.01.02, AK

theorem :: INT_1:57

for i1, i2 being Integer st i2 >= 0 holds
i1 mod i2 >= 0

proof end;

theorem :: INT_1:58

for i1, i2 being Integer st i2 > 0 holds
i1 mod i2 < i2

proof end;

theorem :: INT_1:59

for i1, i2 being Integer st i2 <> 0 holds
i1 = ((i1 div i2) * i2) + (i1 mod i2)

proof end;

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

for i, j being Integer st i >= 0 & j >= 0 holds
i div j >= 0

proof end;

:: from INT_3, 2007.07.27, A.T.

theorem :: INT_1:62

for n being Integer st n > 0 holds
for a being Integer holds
( a mod n = 0 iff n divides a )

proof end;

theorem :: INT_1:63

for r, s being Real st r / s is not Integer holds
- [\(r / s)/] = [\((- r) / s)/] + 1

proof end;

theorem :: INT_1:64

for r, s being Real st r / s is Integer holds
- [\(r / s)/] = [\((- r) / s)/]

proof end;

:: missing, 2008.05.16, A.T.

theorem :: INT_1:65

for i being Integer
for r being Real st r <= i holds
[/r\] <= i

proof end;

:: from POLYNOM2, 2010.02.13, A.T.

scheme :: INT_1:sch 7
FinInd{ F₁() -> Element of NAT , F₂() -> Element of NAT , P₁[ Nat] } :

for i being Element of NAT st F₁() <= i & i <= F₂() holds
P₁[i]

provided

A1: P₁[F₁()] and
A2: for j being Element of NAT st F₁() <= j & j < F₂() & P₁[j] holds
P₁[j + 1]

proof end;

scheme :: INT_1:sch 8
FinInd2{ F₁() -> Element of NAT , F₂() -> Element of NAT , P₁[ Nat] } :

for i being Element of NAT st F₁() <= i & i <= F₂() holds
P₁[i]

provided

A1: P₁[F₁()] and
A2: for j being Element of NAT st F₁() <= j & j < F₂() & ( for j9 being Element of NAT st F₁() <= j9 & j9 <= j holds
P₁[j9] ) holds
P₁[j + 1]

proof end;

theorem :: INT_1:66

for i being Integer
for r being Real holds frac (r + i) = frac r

proof end;

theorem Th65: :: INT_1:67

for a, r being Real st r <= a & a < [\r/] + 1 holds
[\a/] = [\r/]

proof end;

theorem Th66: :: INT_1:68

for a, r being Real st r <= a & a < [\r/] + 1 holds
frac r <= frac a

proof end;

theorem :: INT_1:69

for a, r being Real st r < a & a < [\r/] + 1 holds
frac r < frac a

proof end;

theorem Th68: :: INT_1:70

for a, r being Real st a >= [\r/] + 1 & a <= r + 1 holds
[\a/] = [\r/] + 1

proof end;

theorem Th69: :: INT_1:71

for a, r being Real st a >= [\r/] + 1 & a < r + 1 holds
frac a < frac r

proof end;

theorem :: INT_1:72

for a, b, r being Real st r <= a & a < r + 1 & r <= b & b < r + 1 & frac a = frac b holds
a = b

proof end;

:: 28.05.2012, A.T.

registration

let i be Integer;

reduce In (i,INT) to i;

reducibility
In (i,INT) = i by Def2, SUBSET_1:def 8;

end;

definition

let x be Number ;

attr x is dim-like means :Def11: :: INT_1:def 11
( x = - 1 or x is natural );

end;

:: deftheorem Def11 defines dim-like INT_1:def 11 :
for x being Number holds
( x is dim-like iff ( x = - 1 or x is natural ) );

registration

cluster natural -> dim-like for object ;

coherence
for b₁ being object st b₁ is natural holds
b₁ is dim-like ;

cluster dim-like -> integer for object ;

coherence
for b₁ being object st b₁ is dim-like holds
b₁ is integer ;

cluster - 1 -> dim-like for object ;

coherence
for b₁ being object st b₁ = - 1 holds
b₁ is dim-like ;

end;

registration

cluster dim-like for set ;

existence
ex b₁ being set st b₁ is dim-like

proof end;

end;

registration

let d be dim-like object ;

cluster d + 1 -> natural ;

coherence
d + 1 is natural

proof end;

end;

registration

let k be dim-like object ;
let n be natural non zero Number ;

cluster k + n -> natural ;

coherence
k + n is natural

proof end;

end;

theorem :: INT_1:73

for i being Integer holds 0 = 0 mod i

proof end;

theorem :: INT_1:74

for n being non zero Nat holds
( n - 1 is Nat & 1 <= n )

proof end;