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

proof end;

Lm2: for x being set

for k being Element of NAT st x = - k & k <> x holds

x in [:{0},NAT:] \ {[0,0]}

proof end;

definition

for b_{1} being set holds

( b_{1} = INT iff for x being set holds

( x in b_{1} iff ex k being Element of NAT st

( x = k or x = - k ) ) )
end;

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 x being set holds

( x in it iff ex k being Element of NAT st

( x = k or x = - k ) );

for b

( b

( x in b

( x = k or x = - k ) ) )

proof end;

:: deftheorem Def1 defines INT INT_1:def 1 :

for b_{1} being set holds

( b_{1} = INT iff for x being set holds

( x in b_{1} iff ex k being Element of NAT st

( x = k or x = - k ) ) );

for b

( b

( x in b

( x = k or x = - k ) ) );

:: deftheorem Def2 defines integer INT_1:def 2 :

for i being number holds

( i is integer iff i in INT );

for i being number holds

( i is integer iff i in INT );

registration

existence

ex b_{1} being Real st b_{1} is integer

ex b_{1} being number st b_{1} is integer

for b_{1} being Element of INT holds b_{1} is integer
by Def2;

end;
ex b

proof end;

existence ex b

proof end;

coherence for b

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

registration
end;

Lm3: for x being set st x in INT holds

x in REAL

by NUMBERS:15;

registration
end;

registration

let i1, i2 be Integer;

coherence

i1 + i2 is integer

i1 * i2 is integer

end;
coherence

i1 + i2 is integer

proof end;

coherence i1 * i2 is integer

proof end;

registration
end;

:: Some basic theorems about integers

theorem :: INT_1:4

Lm4: for j being Element of NAT st j < 1 holds

j = 0

proof end;

Lm5: for i1 being Integer st 0 < i1 holds

1 <= i1

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

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

( i1 * i2 = - 1 iff ( ( i1 = - 1 & i2 = 1 ) or ( i1 = 1 & i2 = - 1 ) ) )

proof end;

Lm6: for i0, i1 being Integer st i0 <= i1 holds

ex k being Element of NAT st i0 + k = i1

proof end;

Lm7: for i0, i1 being Integer st i0 <= i1 holds

ex k being Element of NAT st i1 - k = i0

proof end;

:: The divisibility relation

definition

let i1, i2 be Integer;

reflexivity

for i1 being Integer ex i3 being Integer st i1 = i1 * i3

end;
reflexivity

for i1 being Integer ex i3 being Integer st i1 = i1 * i3

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

for i1, i2 being Integer holds

( i1 divides i2 iff ex i3 being Integer st i2 = i1 * i3 );

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

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;

( i1,i2 are_congruent_mod i3 iff ex i4 being Integer st i3 * i4 = i1 - i2 )

end;
redefine pred i1,i2 are_congruent_mod i3 means :Def5: :: INT_1:def 5

ex i4 being Integer st i3 * i4 = i1 - i2;

compatibility ex i4 being Integer st i3 * i4 = i1 - i2;

( i1,i2 are_congruent_mod i3 iff ex i4 being Integer st i3 * i4 = i1 - i2 )

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

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

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

i1,i3 are_congruent_mod i5

i1,i3 are_congruent_mod i5

proof end;

theorem :: INT_1:16

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

i1 + i3,i2 + i4 are_congruent_mod i5

i1 + i3,i2 + i4 are_congruent_mod i5

proof end;

theorem :: INT_1:17

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

i1 - i3,i2 - i4 are_congruent_mod i5

i1 - i3,i2 - i4 are_congruent_mod i5

proof end;

theorem :: INT_1:18

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

i1 * i3,i2 * i4 are_congruent_mod i5

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 )

( i1 + i2,i3 are_congruent_mod i5 iff i1,i3 - i2 are_congruent_mod i5 )

proof end;

theorem :: INT_1:20

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

i1,i2 are_congruent_mod i4

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 )

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

( 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 number

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

i1 = i2

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 number

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

i1 = i2

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

i1 = i2

proof end;

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

proof end;

definition

let r be real number ;

existence

ex b_{1} being Integer st

( b_{1} <= r & r - 1 < b_{1} )

for b_{1}, b_{2} being Integer st b_{1} <= r & r - 1 < b_{1} & b_{2} <= r & r - 1 < b_{2} holds

b_{1} = b_{2}
by Th23;

projectivity

for b_{1} being Integer

for b_{2} being real number st b_{1} <= b_{2} & b_{2} - 1 < b_{1} holds

( b_{1} <= b_{1} & b_{1} - 1 < b_{1} )
by XREAL_1:44;

end;
existence

ex b

( b

proof end;

uniqueness for b

b

projectivity

for b

for b

( b

:: deftheorem Def6 defines [\ INT_1:def 6 :

for r being real number

for b_{2} being Integer holds

( b_{2} = [\r/] iff ( b_{2} <= r & r - 1 < b_{2} ) );

for r being real number

for b

( b

definition

let r be real number ;

existence

ex b_{1} being Integer st

( r <= b_{1} & b_{1} < r + 1 )

for b_{1}, b_{2} being Integer st r <= b_{1} & b_{1} < r + 1 & r <= b_{2} & b_{2} < r + 1 holds

b_{1} = b_{2}
by Th24;

projectivity

for b_{1} being Integer

for b_{2} being real number st b_{2} <= b_{1} & b_{1} < b_{2} + 1 holds

( b_{1} <= b_{1} & b_{1} < b_{1} + 1 )
by XREAL_1:29;

end;
existence

ex b

( r <= b

proof end;

uniqueness for b

b

projectivity

for b

for b

( b

:: deftheorem Def7 defines [/ INT_1:def 7 :

for r being real number

for b_{2} being Integer holds

( b_{2} = [/r\] iff ( r <= b_{2} & b_{2} < r + 1 ) );

for r being real number

for b

( b

definition

let r be real number ;

:: original: frac

redefine func frac r -> Real;

coherence

frac r is Real by XREAL_0:def 1;

end;
:: original: frac

redefine func frac r -> Real;

coherence

frac r is Real by XREAL_0:def 1;

:: Functions div and mod

definition

let i1, i2 be Integer;

coherence

( ( i2 <> 0 implies i1 - ((i1 div i2) * i2) is Integer ) & ( not i2 <> 0 implies 0 is Integer ) );

consistency

for b_{1} being Integer holds verum;

;

end;
func i1 mod i2 -> Integer equals :Def10: :: INT_1:def 10

i1 - ((i1 div i2) * i2) if i2 <> 0

otherwise 0 ;

correctness i1 - ((i1 div i2) * i2) if i2 <> 0

otherwise 0 ;

coherence

( ( i2 <> 0 implies i1 - ((i1 div i2) * i2) is Integer ) & ( not i2 <> 0 implies 0 is Integer ) );

consistency

for b

;

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

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

begin

:: from FSM_1

:: from SCMFSA_7, 2005.02.05, A.T.

:: from UNIFORM1, 2005.08.22, A.T.

theorem :: INT_1:53

for r being real number st r >= 0 holds

( [/r\] >= 0 & [\r/] >= 0 & [/r\] is Element of NAT & [\r/] is Element of NAT )

( [/r\] >= 0 & [\r/] >= 0 & [/r\] is Element of NAT & [\r/] is Element of NAT )

proof end;

:: from SCMFSA9A, 2005.11.16, A.T.

:: from SCMFSA9A, 2006.03.14, A.T.

:: from NEWTON, 2007.01.02, AK

:: from AMI_3, 2007.06.14, A.T.

:: from AMI_4, 2007.06.14, A.T.

:: from INT_3, 2007.07.27, A.T.

:: missing, 2008.05.16, A.T.

:: from POLYNOM2, 2010.02.13, A.T.

scheme :: INT_1:sch 8

FinInd2{ F_{1}() -> Element of NAT , F_{2}() -> Element of NAT , P_{1}[ Nat] } :

provided

FinInd2{ F

provided

A1:
P_{1}[F_{1}()]
and

A2: for j being Element of NAT st F_{1}() <= j & j < F_{2}() & ( for j9 being Element of NAT st F_{1}() <= j9 & j9 <= j holds

P_{1}[j9] ) holds

P_{1}[j + 1]

A2: for j being Element of NAT st F

P

P

proof end;

theorem :: INT_1:72

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

a = b

a = b

proof end;