:: by Grzegorz Bancerek

::

:: Received January 3, 2007

:: Copyright (c) 2007-2012 Association of Mizar Users

begin

Lm1: now :: thesis: for k, l being Nat holds k div l is Nat

let k, l be Nat; :: thesis: k div l is Nat

k div l in NAT by INT_1:3, INT_1:55;

hence k div l is Nat ; :: thesis: verum

end;
k div l in NAT by INT_1:3, INT_1:55;

hence k div l is Nat ; :: thesis: verum

Lm2: now :: thesis: for k, l being Nat holds k mod l is Nat

let k, l be Nat; :: thesis: k mod l is Nat

k mod l in NAT by INT_1:3, INT_1:57;

hence k mod l is Nat ; :: thesis: verum

end;
k mod l in NAT by INT_1:3, INT_1:57;

hence k mod l is Nat ; :: thesis: verum

definition

let k, l be Nat;

for b_{1} being Nat holds

( b_{1} = k div l iff ( ex t being Nat st

( k = (l * b_{1}) + t & t < l ) or ( b_{1} = 0 & l = 0 ) ) )

k div l is Nat by Lm1;

end;
:: original: div

redefine func k div l -> Nat means :Def1: :: NAT_D:def 1

( ex t being Nat st

( k = (l * it) + t & t < l ) or ( it = 0 & l = 0 ) );

compatibility redefine func k div l -> Nat means :Def1: :: NAT_D:def 1

( ex t being Nat st

( k = (l * it) + t & t < l ) or ( it = 0 & l = 0 ) );

for b

( b

( k = (l * b

proof end;

coherence k div l is Nat by Lm1;

:: deftheorem Def1 defines div NAT_D:def 1 :

for k, l, b_{3} being Nat holds

( b_{3} = k div l iff ( ex t being Nat st

( k = (l * b_{3}) + t & t < l ) or ( b_{3} = 0 & l = 0 ) ) );

for k, l, b

( b

( k = (l * b

definition

let k, l be Nat;

for b_{1} being Nat holds

( b_{1} = k mod l iff ( ex t being Nat st

( k = (l * t) + b_{1} & b_{1} < l ) or ( b_{1} = 0 & l = 0 ) ) )

k mod l is Nat by Lm2;

end;
:: original: mod

redefine func k mod l -> Nat means :Def2: :: NAT_D:def 2

( ex t being Nat st

( k = (l * t) + it & it < l ) or ( it = 0 & l = 0 ) );

compatibility redefine func k mod l -> Nat means :Def2: :: NAT_D:def 2

( ex t being Nat st

( k = (l * t) + it & it < l ) or ( it = 0 & l = 0 ) );

for b

( b

( k = (l * t) + b

proof end;

coherence k mod l is Nat by Lm2;

:: deftheorem Def2 defines mod NAT_D:def 2 :

for k, l, b_{3} being Nat holds

( b_{3} = k mod l iff ( ex t being Nat st

( k = (l * t) + b_{3} & b_{3} < l ) or ( b_{3} = 0 & l = 0 ) ) );

for k, l, b

( b

( k = (l * t) + b

definition

let k, l be Nat;

:: original: div

redefine func k div l -> Element of NAT ;

coherence

k div l is Element of NAT

redefine func k mod l -> Element of NAT ;

coherence

k mod l is Element of NAT

end;
:: original: div

redefine func k div l -> Element of NAT ;

coherence

k div l is Element of NAT

proof end;

:: original: modredefine func k mod l -> Element of NAT ;

coherence

k mod l is Element of NAT

proof end;

:: The divisibility relation

definition

let k, l be Nat;

( k divides l iff ex t being Nat st l = k * t )

for k being Nat ex t being Nat st k = k * t

end;
:: original: divides

redefine pred k divides l means :Def3: :: NAT_D:def 3

ex t being Nat st l = k * t;

compatibility redefine pred k divides l means :Def3: :: NAT_D:def 3

ex t being Nat st l = k * t;

( k divides l iff ex t being Nat st l = k * t )

proof end;

reflexivity for k being Nat ex t being Nat st k = k * t

proof end;

:: deftheorem Def3 defines divides NAT_D:def 3 :

for k, l being Nat holds

( k divides l iff ex t being Nat st l = k * t );

for k, l being Nat holds

( k divides l iff ex t being Nat st l = k * t );

:: The least common multiple and the greatest common divisor

definition

let k, n be Nat;

for b_{1} being set holds

( b_{1} = k lcm n iff ( k divides b_{1} & n divides b_{1} & ( for m being Nat st k divides m & n divides m holds

b_{1} divides m ) ) )

end;
redefine func k lcm n means :Def4: :: NAT_D:def 4

( k divides it & n divides it & ( for m being Nat st k divides m & n divides m holds

it divides m ) );

compatibility ( k divides it & n divides it & ( for m being Nat st k divides m & n divides m holds

it divides m ) );

for b

( b

b

proof end;

:: deftheorem Def4 defines lcm NAT_D:def 4 :

for k, n being Nat

for b_{3} being set holds

( b_{3} = k lcm n iff ( k divides b_{3} & n divides b_{3} & ( for m being Nat st k divides m & n divides m holds

b_{3} divides m ) ) );

for k, n being Nat

for b

( b

b

definition

let k, n be Nat;

:: original: lcm

redefine func k lcm n -> Element of NAT ;

coherence

k lcm n is Element of NAT by ORDINAL1:def 12;

end;
:: original: lcm

redefine func k lcm n -> Element of NAT ;

coherence

k lcm n is Element of NAT by ORDINAL1:def 12;

definition

let k, n be Nat;

for b_{1} being set holds

( b_{1} = k gcd n iff ( b_{1} divides k & b_{1} divides n & ( for m being Nat st m divides k & m divides n holds

m divides b_{1} ) ) )

end;
redefine func k gcd n means :Def5: :: NAT_D:def 5

( it divides k & it divides n & ( for m being Nat st m divides k & m divides n holds

m divides it ) );

compatibility ( it divides k & it divides n & ( for m being Nat st m divides k & m divides n holds

m divides it ) );

for b

( b

m divides b

proof end;

:: deftheorem Def5 defines gcd NAT_D:def 5 :

for k, n being Nat

for b_{3} being set holds

( b_{3} = k gcd n iff ( b_{3} divides k & b_{3} divides n & ( for m being Nat st m divides k & m divides n holds

m divides b_{3} ) ) );

for k, n being Nat

for b

( b

m divides b

definition

let k, n be Nat;

:: original: gcd

redefine func k gcd n -> Element of NAT ;

coherence

k gcd n is Element of NAT by ORDINAL1:def 12;

end;
:: original: gcd

redefine func k gcd n -> Element of NAT ;

coherence

k gcd n is Element of NAT by ORDINAL1:def 12;

begin

:: from AMI_5, 2005.11.16, A.T.

:: from GR_CY_1, 2005.11.16, A.T.

:: from JORDAN4

:: Moved from SCMP_GCD by AK on 28.12.2006

:: from AMI_3, 2007.06.14, A.T.

:: moved from INT_2, 2007.11.7, A.T,

:: from from SCMP_GCD, 2007.07.26, A.T.

:: ???, 2007.07.26, A.T.

:: from SCMPDS_9. 2008.05.06, A.T.

:: from BINARITH, 2008.08.18, A.T.

definition

let i, j be Nat;

:: original: -'

redefine func i -' j -> Element of NAT ;

coherence

i -' j is Element of NAT

end;
:: original: -'

redefine func i -' j -> Element of NAT ;

coherence

i -' j is Element of NAT

proof end;

theorem :: NAT_D:37

theorem :: NAT_D:47

for i1, i2 being Nat st ( i1 + 2 <= i2 or (i1 + 1) + 1 <= i2 ) holds

( i1 + 1 < i2 & (i1 + 1) -' 1 < i2 & (i1 + 1) -' 2 < i2 & i1 + 1 <= i2 & (i1 -' 1) + 1 < i2 & ((i1 -' 1) + 1) -' 1 < i2 & i1 < i2 & i1 -' 1 < i2 & i1 -' 2 < i2 & i1 <= i2 )

( i1 + 1 < i2 & (i1 + 1) -' 1 < i2 & (i1 + 1) -' 2 < i2 & i1 + 1 <= i2 & (i1 -' 1) + 1 < i2 & ((i1 -' 1) + 1) -' 1 < i2 & i1 < i2 & i1 -' 1 < i2 & i1 -' 2 < i2 & i1 <= i2 )

proof end;

theorem :: NAT_D:48

for i1, i2 being Nat st ( i1 <= i2 or i1 <= i2 -' 1 ) holds

( i1 < i2 + 1 & i1 <= i2 + 1 & i1 < (i2 + 1) + 1 & i1 <= (i2 + 1) + 1 & i1 < i2 + 2 & i1 <= i2 + 2 )

( i1 < i2 + 1 & i1 <= i2 + 1 & i1 < (i2 + 1) + 1 & i1 <= (i2 + 1) + 1 & i1 < i2 + 2 & i1 <= i2 + 2 )

proof end;

:: form JCT_MISC, 2008.08.21, A.T.

:: from LEXBFS, 2008.08.23, A.T.

:: from INT_3, 2011.04.28, A.T.

theorem Th61: :: NAT_D:61

for n, a, k being Integer holds

( ( n <> 0 implies (a + (n * k)) div n = (a div n) + k ) & (a + (n * k)) mod n = a mod n )

( ( n <> 0 implies (a + (n * k)) div n = (a div n) + k ) & (a + (n * k)) mod n = a mod n )

proof end;

theorem Th63: :: NAT_D:63

for n, a being Integer holds

( ( 0 <= a & a < n implies a mod n = a ) & ( 0 > a & a >= - n implies a mod n = n + a ) )

( ( 0 <= a & a < n implies a mod n = a ) & ( 0 > a & a >= - n implies a mod n = n + a ) )

proof end;

theorem Th64: :: NAT_D:64

for n, a, b being Integer holds

( ( n <> 0 & a mod n = b mod n implies a,b are_congruent_mod n ) & ( a,b are_congruent_mod n implies a mod n = b mod n ) )

( ( n <> 0 & a mod n = b mod n implies a,b are_congruent_mod n ) & ( a,b are_congruent_mod n implies a mod n = b mod n ) )

proof end;

:: from RADIX_1, 2011.07.31, A.T.