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 Th16: :: INT_2:16

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

proof end;

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

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

for a being Integer holds abs a is Nat ;

theorem Th21: :: INT_2:21

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

proof end;

definition

let a, b be Integer;
canceled;
func a lcm' b -> Integer equals :: INT_2:def 2
(abs a) lcm (abs b);
coherence ;
commutativity ;

end;

:: deftheorem INT_2:def 1 :

:: deftheorem defines lcm' INT_2:def 2 :

theorem :: INT_2:22

canceled;

theorem :: INT_2:23

for a, b being Integer holds a lcm' b is Nat ;

theorem :: INT_2:24

canceled;

theorem Th25: :: INT_2:25

for a, b being Integer holds a divides a lcm' b

proof end;

theorem :: INT_2:26

for b, a being Integer holds b divides a lcm' b by Th25;

theorem Th27: :: INT_2:27

for a, b, c being Integer st a divides c & b divides c holds
a lcm' b divides c

proof end;

definition

let a, b be Integer;
func a gcd b -> Integer equals :: INT_2:def 3
(abs a) hcf (abs b);
coherence ;
commutativity ;

end;

:: deftheorem defines gcd INT_2:def 3 :

theorem :: INT_2:28

canceled;

theorem :: INT_2:29

for a, b being Integer holds a gcd b is Nat ;

theorem :: INT_2:30

canceled;

theorem Th31: :: INT_2:31

for a, b being Integer holds a gcd b divides a

proof end;

theorem :: INT_2:32

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

theorem Th33: :: INT_2:33

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

proof end;

theorem :: INT_2:34

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

proof end;

theorem Th35: :: INT_2:35

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

proof end;

definition

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

end;

:: deftheorem Def4 defines are_relative_prime INT_2:def 4 :

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 Nat;
attr p is prime means :Def5: :: INT_2:def 5
( p > 1 & ( for n being Nat holds
( not n divides p or n = 1 or n = p ) ) );

end;

:: deftheorem Def5 defines prime INT_2:def 5 :

definition

let m, n be Nat;
pred m,n are_relative_prime means :Def6: :: INT_2:def 6
m hcf n = 1;
symmetry ;

end;

:: deftheorem Def6 defines are_relative_prime INT_2:def 6 :

theorem :: INT_2:42

canceled;

theorem :: INT_2:43

canceled;

theorem :: INT_2:44

2 is prime

proof end;

theorem :: INT_2:45

canceled;

theorem :: INT_2:46

not 4 is prime

proof end;

theorem :: INT_2:47

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

proof end;

scheme :: INT_2:sch 1
Ind1{ F₁() -> Nat, P₁[ Nat] } :

for k being Nat st k >= F₁() holds
P₁[k]

provided

A1: P₁[F₁()] and
A2: for k being Nat st k >= F₁() & P₁[k] holds
P₁[k + 1]

proof end;

scheme :: INT_2:sch 2
CompInd1{ F₁() -> Nat, P₁[ Nat] } :

for k being Nat st k >= F₁() holds
P₁[k]

provided

A1: for k being Nat st k >= F₁() & ( for n being Nat st n >= F₁() & n < k holds
P₁[n] ) holds
P₁[k]

proof end;

theorem :: INT_2:48

for l being Nat st l >= 2 holds
ex p being Nat st
( p is prime & p divides l )

proof end;