:: The Divisibility of Integers and Integer Relatively Primes
:: by Rafa{\l} Kwiatek and Grzegorz Zwara
::
:: Received July 10, 1990
:: Copyright (c) 1990-2011 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

proof end;

end;

theorem Th1: :: INT_2:1

for a, b, c being Integer st a divides b & a divides b + c holds
a divides c

proof end;

theorem Th2: :: INT_2:2

for a, b, c being Integer st a divides b holds
a divides b * c

proof end;

theorem Th3: :: INT_2:3

for a being Integer holds
( 0 divides a iff a = 0 )

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;
canceled;
func a lcm b -> Nat means :Def2: :: INT_2:def 2
( a divides it & b divides it & ( for m being Integer st a divides m & b divides m holds
it divides m ) );
existence
ex b₁ being Nat st
( a divides b₁ & b divides b₁ & ( for m being Integer st a divides m & b divides m holds
b₁ divides m ) )

proof end;

uniqueness
for b₁, b₂ being Nat st a divides b₁ & b divides b₁ & ( for m being Integer st a divides m & b divides m holds
b₁ divides m ) & a divides b₂ & b divides b₂ & ( for m being Integer st a divides m & b divides m holds
b₂ divides m ) holds
b₁ = b₂

proof end;

commutativity
for b₁ being Nat
for a, b being Integer st a divides b₁ & b divides b₁ & ( for m being Integer st a divides m & b divides m holds
b₁ divides m ) holds
( b divides b₁ & a divides b₁ & ( for m being Integer st b divides m & a divides m holds
b₁ divides m ) ) ;

end;

:: deftheorem INT_2:def 1 :
canceled;

:: deftheorem Def2 defines lcm INT_2:def 2 :
for a, b being Integer
for b₃ being Nat holds
( b₃ = a lcm b iff ( a divides b₃ & b divides b₃ & ( for m being Integer st a divides m & b divides m holds
b₃ divides m ) ) );

theorem Th4: :: INT_2:4

for a, b being Integer holds
( ( a = 0 or b = 0 ) iff a lcm b = 0 )

proof end;

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

proof end;

definition

let a, b be Integer;
func a gcd b -> Nat means :Def3: :: INT_2:def 3
( it divides a & it divides b & ( for m being Integer st m divides a & m divides b holds
m divides it ) );
existence
ex b₁ being Nat st
( b₁ divides a & b₁ divides b & ( for m being Integer st m divides a & m divides b holds
m divides b₁ ) )

proof end;

uniqueness
for b₁, b₂ being Nat st b₁ divides a & b₁ divides b & ( for m being Integer st m divides a & m divides b holds
m divides b₁ ) & b₂ divides a & b₂ divides b & ( for m being Integer st m divides a & m divides b holds
m divides b₂ ) holds
b₁ = b₂

proof end;

commutativity
for b₁ being Nat
for a, b being Integer st b₁ divides a & b₁ divides b & ( for m being Integer st m divides a & m divides b holds
m divides b₁ ) holds
( b₁ divides b & b₁ divides a & ( for m being Integer st m divides b & m divides a holds
m divides b₁ ) ) ;

end;

:: deftheorem Def3 defines gcd INT_2:def 3 :
for a, b being Integer
for b₃ being Nat holds
( b₃ = a gcd b iff ( b₃ divides a & b₃ divides b & ( for m being Integer st m divides a & m divides b holds
m divides b₃ ) ) );

theorem Th5: :: INT_2:5

for a, b being Integer holds
( ( a = 0 & b = 0 ) iff a gcd b = 0 )

proof end;

theorem :: INT_2:6

canceled;

theorem :: INT_2:7

canceled;

theorem Th8: :: INT_2:8

for n being natural number holds
( - n is Element of NAT iff n = 0 )

proof end;

registration

let n be non zero natural number ;
cluster - n -> non natural ;
coherence
not - n is natural

proof end;

end;

theorem :: INT_2:9

- 1 is not Element of NAT ;

theorem :: INT_2:10

canceled;

theorem :: INT_2:11

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

theorem :: INT_2:12

canceled;

theorem :: INT_2:13

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

theorem Th14: :: INT_2:14

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

proof end;

theorem :: INT_2:15

for a, b being Integer st a divides b & b divides a & not a = b holds
a = - b

proof end;

theorem :: INT_2:16

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

theorem Th17: :: INT_2:17

for a being Integer holds
( ( not a divides 1 & not a divides - 1 ) or a = 1 or a = - 1 )

proof end;

theorem :: INT_2:18

for a being Integer st ( a = 1 or a = - 1 ) holds
( a divides 1 & a divides - 1 ) by Lm5;

theorem :: INT_2:19

for a, b, c being Integer holds
( a,b are_congruent_mod c iff c divides a - b )

proof end;

theorem :: INT_2:20

canceled;

theorem :: INT_2:21

for a, b being Integer holds
( a divides b iff abs a divides abs b )

proof end;

theorem :: INT_2:22

canceled;

theorem :: INT_2:23

for a, b being Integer holds a lcm b is Element of NAT by ORDINAL1:def 13;

theorem :: INT_2:24

canceled;

theorem :: INT_2:25

for a, b being Integer holds a divides a lcm b by Def2;

theorem :: INT_2:26

canceled;

theorem :: INT_2:27

for a, b, c being Integer st a divides c & b divides c holds
a lcm b divides c by Def2;

theorem :: INT_2:28

canceled;

theorem :: INT_2:29

for a, b being Integer holds a gcd b is Element of NAT by ORDINAL1:def 13;

theorem :: INT_2:30

canceled;

theorem Th31: :: INT_2:31

for a, b being Integer holds a gcd b divides a by Def3;

theorem :: INT_2:32

canceled;

theorem :: INT_2:33

for a, b, c being Integer st c divides a & c divides b holds
c divides a gcd b by Def3;

definition

let a, b be Integer;
pred a,b are_relative_prime means :Def4: :: INT_2:def 4
a gcd b = 1;
symmetry
for a, b being Integer st a gcd b = 1 holds
b gcd a = 1 ;

end;

:: deftheorem Def4 defines are_relative_prime INT_2:def 4 :
for a, b being Integer holds
( a,b are_relative_prime iff a gcd b = 1 );

theorem :: INT_2:34

canceled;

theorem :: INT_2:35

canceled;

theorem :: INT_2:36

canceled;

theorem :: INT_2:37

canceled;

theorem :: INT_2:38

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

proof end;

theorem Th39: :: INT_2:39

for a, b, c being Integer st a,b are_relative_prime holds
( (c * a) gcd (c * b) = abs c & (c * a) gcd (b * c) = abs c & (a * c) gcd (c * b) = abs c & (a * c) gcd (b * c) = abs c )

proof end;

theorem Th40: :: INT_2:40

for c, a, b being Integer st c divides a * b & a,c are_relative_prime holds
c divides b

proof end;

theorem :: INT_2:41

for a, c, b being Integer st a,c are_relative_prime & b,c are_relative_prime holds
a * b,c are_relative_prime

proof end;

definition

let p be natural number ;
attr p is prime means :Def5: :: INT_2:def 5
( p > 1 & ( for n being natural number holds
( not n divides p or n = 1 or n = p ) ) );

end;

:: deftheorem Def5 defines prime INT_2:def 5 :
for p being natural number holds
( p is prime iff ( p > 1 & ( for n being natural number holds
( not n divides p or n = 1 or n = p ) ) ) );

theorem :: INT_2:42

canceled;

theorem Th43: :: INT_2:43

for b, a being Integer st 0 < b & a divides b holds
a <= b

proof end;

theorem Th44: :: INT_2:44

2 is prime

proof end;

theorem :: INT_2:45

canceled;

theorem Th46: :: INT_2:46

not 4 is prime

proof end;

registration

cluster ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer prime set ;
existence
ex b₁ being natural number st b₁ is prime by Th44;
cluster ext-real non negative non zero epsilon-transitive epsilon-connected ordinal natural complex V15() integer non prime set ;
existence
ex b₁ being natural number st
( not b₁ is zero & not b₁ is prime ) by Th46;

end;

theorem :: INT_2:47

for p, q being natural number st p is prime & q is prime & not p,q are_relative_prime holds
p = q

proof end;

theorem :: INT_2:48

for l being natural number st l >= 2 holds
ex p being Element of NAT st
( p is prime & p divides l )

proof end;

begin

theorem :: INT_2:49

for i, j being Integer st i >= 0 & j >= 0 holds
( (abs i) mod (abs j) = i mod j & (abs i) div (abs j) = i div j )

proof end;

theorem :: INT_2:50

for a, b being Integer holds a lcm b = (abs a) lcm (abs b)

proof end;

theorem :: INT_2:51

for a, b being Integer holds a gcd b = (abs a) gcd (abs b)

proof end;