:: The Divisibility of Integers and Integer Relatively Primes
:: by Rafa{\l} Kwiatek and Grzegorz Zwara
::
:: Received July 10, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
let a be integer number ;
:: original:|.
redefine func abs a ->  Element of NAT ;
coherence
 |.a.| is Element of NAT
proofend;
end;

theorem Th1: :: INT_2:1
for a, b, c being Integer st a divides b & a divides b + c holds
a divides c
proofend;

theorem Th2: :: INT_2:2
for a, b, c being Integer st a divides b holds
a divides b * c
proofend;

theorem Th3: :: INT_2:3
for a being Integer holds
( 0 divides a iff a = 0 )
proofend;

Lm1:  for a being Integer holds
( a divides - a & - a divides a )
proofend;

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

Lm3:  for a, b being Integer holds
( a divides b iff a divides - b )
proofend;

Lm4:  for a, b being Integer holds
( a divides b iff - a divides b )
proofend;

Lm5:  for a being Integer holds
( a divides 0 & 1 divides a & - 1 divides a )
proofend;

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

Lm7:  for k, l being Nat holds
( k divides l iff ex t being Nat st l = k * t )
proofend;

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

definition
let a, b be Integer;
funca 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
 ex b1 being Nat st
( a divides b1 & b divides b1 & ( for m being Integer st a divides m & b divides m holds
b1 divides m ) )
proofend;
uniqueness
 for b1, b2 being Nat st a divides b1 & b divides b1 & ( for m being Integer st a divides m & b divides m holds
b1 divides m ) & a divides b2 & b divides b2 & ( for m being Integer st a divides m & b divides m holds
b2 divides m ) holds
b1 = b2
proofend;
commutativity
 for b1 being Nat
for a, b being Integer st a divides b1 & b divides b1 & ( for m being Integer st a divides m & b divides m holds
b1 divides m ) holds
( b divides b1 & a divides b1 & ( for m being Integer st b divides m & a divides m holds
b1 divides m ) ) ;
end;

:: deftheorem Def1 defines lcm INT_2:def_1_:_
 for a, b being Integer
for b3 being Nat holds
( b3 = a lcm b iff ( a divides b3 & b divides b3 & ( for m being Integer st a divides m & b divides m holds
b3 divides m ) ) );

theorem Th4: :: INT_2:4
for a, b being Integer holds
( ( a = 0 or b = 0 ) iff a lcm b = 0 )
proofend;

Lm9:  for j, i being Nat st 0 < j &amp; i divides j holds
i <= j
proofend;

definition
let a, b be Integer;
funca gcd b ->  Nat means :Def2: :: INT_2:def 2
( it divides a &amp; it divides b &amp; ( for m being Integer st m divides a &amp; m divides b holds
m divides it ) );
existence
 ex b1 being Nat st
( b1 divides a &amp; b1 divides b &amp; ( for m being Integer st m divides a &amp; m divides b holds
m divides b1 ) )
proofend;
uniqueness
 for b1, b2 being Nat st b1 divides a &amp; b1 divides b &amp; ( for m being Integer st m divides a &amp; m divides b holds
m divides b1 ) &amp; b2 divides a &amp; b2 divides b &amp; ( for m being Integer st m divides a &amp; m divides b holds
m divides b2 ) holds
b1 = b2
proofend;
commutativity
 for b1 being Nat
for a, b being Integer st b1 divides a &amp; b1 divides b &amp; ( for m being Integer st m divides a &amp; m divides b holds
m divides b1 ) holds
( b1 divides b &amp; b1 divides a &amp; ( for m being Integer st m divides b &amp; m divides a holds
m divides b1 ) ) ;
end;

:: deftheorem Def2 defines gcd INT_2:def_2_:_
 for a, b being Integer
for b3 being Nat holds
( b3 = a gcd b iff ( b3 divides a &amp; b3 divides b &amp; ( for m being Integer st m divides a &amp; m divides b holds
m divides b3 ) ) );

theorem Th5: :: INT_2:5
for a, b being Integer holds
( ( a = 0 &amp; b = 0 ) iff a gcd b = 0 )
proofend;

theorem Th6: :: INT_2:6
for n being Nat holds
( - n is Element of NAT iff n = 0 )
proofend;

registration
let n be non zero Nat;
cluster - n ->  non natural ;
coherence
 not - n is natural
proofend;
end;

theorem :: INT_2:7
- 1 is not Element of NAT ;

theorem :: INT_2:8
for a being Integer holds
( a divides - a &amp; - a divides a ) by Lm1;

theorem :: INT_2:9
for a, b, c being Integer st a divides b &amp; b divides c holds
a divides c by Lm2;

theorem Th10: :: INT_2:10
for a, b being Integer holds
( ( a divides b implies a divides - b ) &amp; ( a divides - b implies a divides b ) &amp; ( a divides b implies - a divides b ) &amp; ( - a divides b implies a divides b ) &amp; ( a divides b implies - a divides - b ) &amp; ( - a divides - b implies a divides b ) &amp; ( a divides - b implies - a divides b ) &amp; ( - a divides b implies a divides - b ) )
proofend;

theorem :: INT_2:11
for a, b being Integer st a divides b &amp; b divides a &amp; not a = b holds
a = - b
proofend;

theorem :: INT_2:12
for a being Integer holds
( a divides 0 &amp; 1 divides a &amp; - 1 divides a ) by Lm5;

theorem Th13: :: INT_2:13
for a being Integer holds
( ( not a divides 1 &amp; not a divides - 1 ) or a = 1 or a = - 1 )
proofend;

theorem :: INT_2:14
for a being Integer st ( a = 1 or a = - 1 ) holds
( a divides 1 &amp; a divides - 1 ) by Lm5;

theorem :: INT_2:15
for a, b, c being Integer holds
( a,b are_congruent_mod c iff c divides a - b )
proofend;

theorem :: INT_2:16
for a, b being Integer holds
( a divides b iff abs a divides abs b )
proofend;

theorem :: INT_2:17
for a, b being Integer holds a lcm b is Element of NAT by ORDINAL1:def_12;

theorem :: INT_2:18
for a, b being Integer holds a divides a lcm b by Def1;

theorem :: INT_2:19
for a, b, c being Integer st a divides c &amp; b divides c holds
a lcm b divides c by Def1;

theorem :: INT_2:20
for a, b being Integer holds a gcd b is Element of NAT by ORDINAL1:def_12;

theorem Th21: :: INT_2:21
for a, b being Integer holds a gcd b divides a by Def2;

theorem :: INT_2:22
for a, b, c being Integer st c divides a &amp; c divides b holds
c divides a gcd b by Def2;

:: Relative Prime Numbers
definition
let a, b be Integer;
preda,b are_relative_prime  means :Def3: :: INT_2:def 3
a gcd b = 1;
symmetry
 for a, b being Integer st a gcd b = 1 holds
b gcd a = 1 ;
end;

:: deftheorem Def3 defines are_relative_prime INT_2:def_3_:_
 for a, b being Integer holds
( a,b are_relative_prime 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 &amp; b = (a gcd b) * b1 &amp; a1,b1 are_relative_prime )
proofend;

theorem Th24: :: INT_2:24
for a, b, c being Integer st a,b are_relative_prime holds
( (c * a) gcd (c * b) = abs c &amp; (c * a) gcd (b * c) = abs c &amp; (a * c) gcd (c * b) = abs c &amp; (a * c) gcd (b * c) = abs c )
proofend;

theorem Th25: :: INT_2:25
for c, a, b being Integer st c divides a * b &amp; a,c are_relative_prime holds
c divides b
proofend;

theorem :: INT_2:26
for a, c, b being Integer st a,c are_relative_prime &amp; b,c are_relative_prime holds
a * b,c are_relative_prime
proofend;

definition
let p be Nat;
attrp is prime  means :Def4: :: INT_2:def 4
( p > 1 &amp; ( for n being Nat holds
( not n divides p or n = 1 or n = p ) ) );
end;

:: deftheorem Def4 defines prime INT_2:def_4_:_
 for p being Nat holds
( p is prime iff ( p > 1 &amp; ( for n being Nat holds
( not n divides p or n = 1 or n = p ) ) ) );

theorem Th27: :: INT_2:27
for b, a being Integer st 0 < b &amp; a divides b holds
a <= b
proofend;

theorem Th28: :: INT_2:28
2 is prime
proofend;

theorem Th29: :: INT_2:29
not 4 is prime
proofend;

registration
cluster ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer prime for set ;
existence
 ex b1 being Nat st b1 is prime by Th28;
cluster ext-real non negative non zero epsilon-transitive epsilon-connected ordinal natural complex V15() integer non prime for set ;
existence
 ex b1 being Nat st
( not b1 is zero &amp; not b1 is prime ) by Th29;
end;

theorem :: INT_2:30
for p, q being Nat st p is prime &amp; q is prime &amp; not p,q are_relative_prime holds
p = q
proofend;

theorem :: INT_2:31
for l being Nat st l >= 2 holds
ex p being Element of NAT st
( p is prime &amp; p divides l )
proofend;

begin

:: from AMI_4, 2007.06.14, A.T.
theorem :: INT_2:32
for i, j being Integer st i >= 0 &amp; j >= 0 holds
( (abs i) mod (abs j) = i mod j &amp; (abs i) div (abs j) = i div j )
proofend;

:: old definitions, 2007.11.07, A.T
theorem :: INT_2:33
for a, b being Integer holds a lcm b = (abs a) lcm (abs b)
proofend;

theorem :: INT_2:34
for a, b being Integer holds a gcd b = (abs a) gcd (abs b)
proofend;