:: by Rafa{\l} Kwiatek and Grzegorz Zwara

::

:: Received July 10, 1990

:: Copyright (c) 1990-2016 Association of Mizar Users

definition

let a be Integer;

:: original: |.

redefine func |.a.| -> Element of NAT ;

coherence

|.a.| is Element of NAT

end;
:: original: |.

redefine func |.a.| -> Element of NAT ;

coherence

|.a.| is Element of NAT

proof end;

Lm1: for a being Integer holds

( a divides - a & - a divides a )

proof end;

Lm2: for a, b, c being Integer st a divides b & b divides c holds

a divides c

proof end;

Lm3: for a, b being Integer holds

( a divides b iff a divides - b )

proof end;

Lm4: for a, b being Integer holds

( a divides b iff - a divides b )

proof end;

Lm5: for a being Integer holds

( a divides 0 & 1 divides a & - 1 divides a )

proof end;

Lm6: for a, b, c being Integer st a divides b & a divides c holds

a divides b mod c

proof end;

Lm7: for k, l being Nat holds

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

proof end;

Lm8: for i, j being Nat st i divides j & j divides i holds

i = j

proof end;

definition

let a, b be Integer;

ex b_{1} being Nat st

( a divides b_{1} & b divides b_{1} & ( for m being Integer st a divides m & b divides m holds

b_{1} divides m ) )

for b_{1}, b_{2} being Nat st a divides b_{1} & b divides b_{1} & ( for m being Integer st a divides m & b divides m holds

b_{1} divides m ) & a divides b_{2} & b divides b_{2} & ( for m being Integer st a divides m & b divides m holds

b_{2} divides m ) holds

b_{1} = b_{2}

for b_{1} being Nat

for a, b being Integer st a divides b_{1} & b divides b_{1} & ( for m being Integer st a divides m & b divides m holds

b_{1} divides m ) holds

( b divides b_{1} & a divides b_{1} & ( for m being Integer st b divides m & a divides m holds

b_{1} divides m ) )
;

end;
func a lcm b -> Nat means :Def1: :: INT_2:def 1

( a divides it & b divides it & ( for m being Integer st a divides m & b divides m holds

it divides m ) );

existence ( a divides it & b divides it & ( for m being Integer st a divides m & b divides m holds

it divides m ) );

ex b

( a divides b

b

proof end;

uniqueness for b

b

b

b

proof end;

commutativity for b

for a, b being Integer st a divides b

b

( b divides b

b

:: deftheorem Def1 defines lcm INT_2:def 1 :

for a, b being Integer

for b_{3} being Nat holds

( b_{3} = a lcm b iff ( a divides b_{3} & b divides b_{3} & ( for m being Integer st a divides m & b divides m holds

b_{3} divides m ) ) );

for a, b being Integer

for b

( b

b

Lm9: for i, j being Nat st 0 < j & i divides j holds

i <= j

proof end;

definition

let a, b be Integer;

ex b_{1} being Nat st

( b_{1} divides a & b_{1} divides b & ( for m being Integer st m divides a & m divides b holds

m divides b_{1} ) )

for b_{1}, b_{2} being Nat st b_{1} divides a & b_{1} divides b & ( for m being Integer st m divides a & m divides b holds

m divides b_{1} ) & b_{2} divides a & b_{2} divides b & ( for m being Integer st m divides a & m divides b holds

m divides b_{2} ) holds

b_{1} = b_{2}

for b_{1} being Nat

for a, b being Integer st b_{1} divides a & b_{1} divides b & ( for m being Integer st m divides a & m divides b holds

m divides b_{1} ) holds

( b_{1} divides b & b_{1} divides a & ( for m being Integer st m divides b & m divides a holds

m divides b_{1} ) )
;

end;
func a gcd b -> Nat means :Def2: :: INT_2:def 2

( it divides a & it divides b & ( for m being Integer st m divides a & m divides b holds

m divides it ) );

existence ( it divides a & it divides b & ( for m being Integer st m divides a & m divides b holds

m divides it ) );

ex b

( b

m divides b

proof end;

uniqueness for b

m divides b

m divides b

b

proof end;

commutativity for b

for a, b being Integer st b

m divides b

( b

m divides b

:: deftheorem Def2 defines gcd INT_2:def 2 :

for a, b being Integer

for b_{3} being Nat holds

( b_{3} = a gcd b iff ( b_{3} divides a & b_{3} divides b & ( for m being Integer st m divides a & m divides b holds

m divides b_{3} ) ) );

for a, b being Integer

for b

( b

m divides b

registration
end;

theorem Th10: :: INT_2:10

for a, b being Integer holds

( ( a divides b implies a divides - b ) & ( a divides - b implies a divides b ) & ( a divides b implies - a divides b ) & ( - a divides b implies a divides b ) & ( a divides b implies - a divides - b ) & ( - a divides - b implies a divides b ) & ( a divides - b implies - a divides b ) & ( - a divides b implies a divides - b ) )

( ( a divides b implies a divides - b ) & ( a divides - b implies a divides b ) & ( a divides b implies - a divides b ) & ( - a divides b implies a divides b ) & ( a divides b implies - a divides - b ) & ( - a divides - b implies a divides b ) & ( a divides - b implies - a divides b ) & ( - a divides b implies a divides - b ) )

proof end;

theorem :: INT_2:14

theorem :: INT_2:15

theorem :: INT_2:19

theorem :: INT_2:22

:: Relative Prime Numbers

definition
end;

:: deftheorem defines are_coprime INT_2:def 3 :

for a, b being Integer holds

( a,b are_coprime iff a gcd b = 1 );

for a, b being Integer holds

( a,b are_coprime iff a gcd b = 1 );

theorem :: INT_2:23

for a, b being Integer st ( a <> 0 or b <> 0 ) holds

ex a1, b1 being Integer st

( a = (a gcd b) * a1 & b = (a gcd b) * b1 & a1,b1 are_coprime )

ex a1, b1 being Integer st

( a = (a gcd b) * a1 & b = (a gcd b) * b1 & a1,b1 are_coprime )

proof end;

theorem Th24: :: INT_2:24

for a, b, c being Integer st a,b are_coprime holds

( (c * a) gcd (c * b) = |.c.| & (c * a) gcd (b * c) = |.c.| & (a * c) gcd (c * b) = |.c.| & (a * c) gcd (b * c) = |.c.| )

( (c * a) gcd (c * b) = |.c.| & (c * a) gcd (b * c) = |.c.| & (a * c) gcd (c * b) = |.c.| & (a * c) gcd (b * c) = |.c.| )

proof end;

:: deftheorem defines prime INT_2:def 4 :

for p being integer Number holds

( p is prime iff ( p > 1 & ( for n being Nat holds

( not n divides p or n = 1 or n = p ) ) ) );

for p being integer Number holds

( p is prime iff ( p > 1 & ( for n being Nat holds

( not n divides p or n = 1 or n = p ) ) ) );

registration
end;

registration

ex b_{1} being Nat st b_{1} is prime
by Th28;

ex b_{1} being Nat st

( not b_{1} is zero & not b_{1} is prime )
by Th29;

end;

cluster ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V38() integer dim-like V41() V46() prime for set ;

existence ex b

cluster ext-real non negative epsilon-transitive epsilon-connected ordinal natural non zero complex V38() integer dim-like V41() V46() non prime for set ;

existence ex b

( not b

:: from AMI_4, 2007.06.14, A.T.

theorem :: INT_2:32

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

( |.i.| mod |.j.| = i mod j & |.i.| div |.j.| = i div j )

( |.i.| mod |.j.| = i mod j & |.i.| div |.j.| = i div j )

proof end;

:: old definitions, 2007.11.07, A.T