:: INT_2 semantic presentation

begin

definition
let a be integer number ;
:: original: |.
redefine func abs a ->  Element of NAT ;
coherence
 |.a.| is Element of NAT
proof
percases ( a >= 0 or a < 0 ) ;
supposeA1: a >= 0 ; ::_thesis: |.a.| is Element of NAT
then  abs a = a by ABSVALUE:def_1;
hence  |.a.| is Element of NAT by A1, INT_1:3; ::_thesis: verum
end;
suppose a < 0 ; ::_thesis: |.a.| is Element of NAT
then  ( abs a = - a & - a > 0 ) by ABSVALUE:def_1, XREAL_1:58;
hence  |.a.| is Element of NAT by INT_1:3; ::_thesis: verum
end;
end;
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
let a, b, c be Integer; ::_thesis: ( a divides b & a divides b + c implies a divides c )
given u being Integer such that A1: b = a * u ; :: according to INT_1:def_3 ::_thesis: ( not a divides b + c or a divides c )
given t being Integer such that A2: b + c = a * t ; :: according to INT_1:def_3 ::_thesis: a divides c
 c = a * (t - u) by A1, A2;
hence  a divides c by INT_1:def_3; ::_thesis: verum
end;

theorem Th2: :: INT_2:2
for a, b, c being Integer st a divides b holds
a divides b * c
proof
let a, b, c be Integer; ::_thesis: ( a divides b implies a divides b * c )
assume  a divides b ; ::_thesis: a divides b * c
then consider l being Integer such that
A1: b = a * l by INT_1:def_3;
 (a * l) * c = a * (l * c) ;
hence  a divides b * c by A1, INT_1:def_3; ::_thesis: verum
end;

theorem Th3: :: INT_2:3
for a being Integer holds
( 0 divides a iff a = 0 )
proof
let a be Integer; ::_thesis: ( 0 divides a iff a = 0 )
 ( 0 divides a implies a = 0 )
proof
assume  0 divides a ; ::_thesis: a = 0
then  ex b being Integer st a = 0 * b by INT_1:def_3;
hence  a = 0 ; ::_thesis: verum
end;
hence  ( 0 divides a iff a = 0 ) ; ::_thesis: verum
end;

Lm1:  for a being Integer holds
( a divides - a & - a divides a )
proof
let a be Integer; ::_thesis: ( a divides - a & - a divides a )
 - a = a * (- 1) ;
hence  a divides - a by INT_1:def_3; ::_thesis: - a divides a
 a = (- a) * (- 1) ;
hence  - a divides a by INT_1:def_3; ::_thesis: verum
end;

Lm2:  for a, b, c being Integer st a divides b & b divides c holds
a divides c
proof
let a, b, c be Integer; ::_thesis: ( a divides b & b divides c implies a divides c )
assume that
A1: a divides b and
A2: b divides c ; ::_thesis: a divides c
consider k being Integer such that
A3: b = a * k by A1, INT_1:def_3;
consider l being Integer such that
A4: c = b * l by A2, INT_1:def_3;
 c = a * (k * l) by A3, A4;
hence  a divides c by INT_1:def_3; ::_thesis: verum
end;

Lm3:  for a, b being Integer holds
( a divides b iff a divides - b )
proof
let a, b be Integer; ::_thesis: ( a divides b iff a divides - b )
thus  ( a divides b implies a divides - b ) ::_thesis: ( a divides - b implies a divides b )
proof
assume A1: a divides b ; ::_thesis: a divides - b
 b divides - b by Lm1;
hence  a divides - b by A1, Lm2; ::_thesis: verum
end;
assume A2: a divides - b ; ::_thesis: a divides b
 - b divides b by Lm1;
hence  a divides b by A2, Lm2; ::_thesis: verum
end;

Lm4:  for a, b being Integer holds
( a divides b iff - a divides b )
proof
let a, b be Integer; ::_thesis: ( a divides b iff - a divides b )
thus  ( a divides b implies - a divides b ) ::_thesis: ( - a divides b implies a divides b )
proof
assume A1: a divides b ; ::_thesis: - a divides b
 - a divides a by Lm1;
hence  - a divides b by A1, Lm2; ::_thesis: verum
end;
assume A2: - a divides b ; ::_thesis: a divides b
 a divides - a by Lm1;
hence  a divides b by A2, Lm2; ::_thesis: verum
end;

Lm5:  for a being Integer holds
( a divides 0 & 1 divides a & - 1 divides a )
proof
let a be Integer; ::_thesis: ( a divides 0 & 1 divides a & - 1 divides a )
 0 = a * 0 ;
hence  a divides 0 by INT_1:def_3; ::_thesis: ( 1 divides a & - 1 divides a )
 a = 1 * a ;
hence  1 divides a by INT_1:def_3; ::_thesis: - 1 divides a
 a = (- 1) * (- a) ;
hence  - 1 divides a by INT_1:def_3; ::_thesis: verum
end;

Lm6:  for a, b, c being Integer st a divides b & a divides c holds
a divides b mod c
proof
let a, b, c be Integer; ::_thesis: ( a divides b & a divides c implies a divides b mod c )
assume that
A1: a divides b and
A2: a divides c ; ::_thesis: a divides b mod c
A3: now__::_thesis:_(_c_<>_0_implies_a_divides_b_mod_c_)
assume  c <> 0 ; ::_thesis: a divides b mod c
then A4: b = (c * (b div c)) + (b mod c) by INT_1:59;
 a divides c * (b div c) by A2, Th2;
hence  a divides b mod c by A1, A4, Th1; ::_thesis: verum
end;
now__::_thesis:_(_c_=_0_implies_a_divides_b_mod_c_)
assume  c = 0 ; ::_thesis: a divides b mod c
then  b mod c = 0 by INT_1:def_10;
hence  a divides b mod c by Lm5; ::_thesis: verum
end;
hence  a divides b mod c by A3; ::_thesis: verum
end;

    Lm7:  for k, l being Nat holds
( k divides l iff ex t being Nat st l = k * t )
proof
let k, l be Nat; ::_thesis: ( k divides l iff ex t being Nat st l = k * t )
hereby  ::_thesis: ( ex t being Nat st l = k * t implies k divides l )
assume A1: k divides l ; ::_thesis: ex t being Nat st l = k * t
thus  ex t being Nat st l = k * t ::_thesis: verum
proof
A2: k >= 0 by NAT_1:2;
consider t being Integer such that
A3: l = k * t by A1, INT_1:def_3;
percases ( 0 < l or l = 0 ) by NAT_1:3;
suppose 0 < l ; ::_thesis: ex t being Nat st l = k * t
then  0 <= t by A3, A2, XREAL_1:131;
then reconsider t = t as Element of NAT by INT_1:3;
take  t ; ::_thesis: l = k * t
thus  l = k * t by A3; ::_thesis: verum
end;
supposeA4: l = 0 ; ::_thesis: ex t being Nat st l = k * t
take  0 ; ::_thesis: l = k * 0
thus  l = k * 0 by A4; ::_thesis: verum
end;
end;
end;
end;
assume  ex t being Nat st l = k * t ; ::_thesis: k divides l
hence  k divides l by INT_1:def_3; ::_thesis: verum
end;

Lm8:  for i, j being Nat st i divides j & j divides i holds
i = j
proof
let i, j be Nat; ::_thesis: ( i divides j & j divides i implies i = j )
assume  i divides j ; ::_thesis: ( not j divides i or i = j )
then consider a being Integer such that
A1: j = i * a by INT_1:def_3;
assume  j divides i ; ::_thesis: i = j
then consider b being Integer such that
A2: i = j * b by INT_1:def_3;
 ( i <> 0 implies i = j )
proof
A3: i >= 0 by NAT_1:2;
assume A4: i <> 0 ; ::_thesis: i = j
 1 * i = i * (a * b) by A1, A2;
then  a * b = 1 by A4, XCMPLX_1:5;
then  ( i = j * 1 or i = j * (- 1) ) by A2, INT_1:9;
hence  i = j by A4, A3; ::_thesis: verum
end;
hence  i = j by A1; ::_thesis: verum
end;

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 ) )
proof
percases ( a = 0 or b = 0 or ( a <> 0 & b <> 0 ) ) ;
supposeA1: ( a = 0 or b = 0 ) ; ::_thesis: 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 ) )
take  0 ; ::_thesis: ( a divides 0 & b divides 0 & ( for m being Integer st a divides m & b divides m holds
0 divides m ) )
thus  ( a divides 0 & b divides 0 ) by Lm5; ::_thesis: for m being Integer st a divides m & b divides m holds
0 divides m
thus  for m being Integer st a divides m & b divides m holds
0 divides m by A1; ::_thesis: verum
end;
supposeA2: ( a <> 0 & b <> 0 ) ; ::_thesis: 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 ) )
defpred S1[ Nat] means ( a divides $1 & b divides $1 & $1 <> 0 );
 a * b in INT by INT_1:def_2;
then consider k being Element of NAT  such that
A3: ( a * b = k or a * b = - k ) by INT_1:def_1;
 b divides a * b by INT_1:def_3;
then A4: b divides k by A3, Lm3;
 a divides a * b by INT_1:def_3;
then A5: a divides k by A3, Lm3;
 k <> 0 by A2, A3, XCMPLX_1:6;
then A6: ex k being Nat st S1[k] by A5, A4;
consider k being Nat such that
A7: S1[k] and
A8: for n being Nat st S1[n] holds
k <= n from NAT_1:sch_5(A6);
take  k ; ::_thesis: ( a divides k & b divides k & ( for m being Integer st a divides m & b divides m holds
k divides m ) )
thus  ( a divides k & b divides k ) by A7; ::_thesis: for m being Integer st a divides m & b divides m holds
k divides m
let m be Integer; ::_thesis: ( a divides m & b divides m implies k divides m )
 m in INT by INT_1:def_2;
then consider n being Element of NAT  such that
A9: ( m = n or m = - n ) by INT_1:def_1;
assume that
A10: a divides m and
A11: b divides m ; ::_thesis: k divides m
 b divides n by A9, A11, Lm3;
then A12: b divides n mod k by A7, Lm6;
A13: k > 0 by A7, NAT_1:3;
then  n mod k in NAT by INT_1:3, INT_1:57;
then reconsider i = n mod k as Nat ;
assume A14: not k divides m ; ::_thesis: contradiction
A15: now__::_thesis:_not_i_=_0
assume  i = 0 ; ::_thesis: contradiction
then  n - ((n div k) * k) = 0 by A7, INT_1:def_10;
then  k divides n by INT_1:def_3;
hence  contradiction by A9, A14, Lm3; ::_thesis: verum
end;
 a divides n by A9, A10, Lm3;
then  a divides n mod k by A7, Lm6;
then  k divides n by A8, A13, A12, A15, INT_1:58;
hence  contradiction by A9, A14, Lm3; ::_thesis: verum
end;
end;
end;
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
proof
let IT1, IT2 be Nat; ::_thesis: ( a divides IT1 & b divides IT1 & ( for m being Integer st a divides m & b divides m holds
IT1 divides m ) & a divides IT2 & b divides IT2 & ( for m being Integer st a divides m & b divides m holds
IT2 divides m ) implies IT1 = IT2 )
assume  ( a divides IT1 & b divides IT1 & ( for m being Integer st a divides m & b divides m holds
IT1 divides m ) & a divides IT2 & b divides IT2 & ( for m being Integer st a divides m & b divides m holds
IT2 divides m ) ) ; ::_thesis: IT1 = IT2
then  ( IT1 divides IT2 & IT2 divides IT1 ) ;
hence  IT1 = IT2 by Lm8; ::_thesis: verum
end;
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 )
proof
let a, b be Integer; ::_thesis: ( ( a = 0 or b = 0 ) iff a lcm b = 0 )
A1: ( b = 0 implies a lcm b = 0 )
proof
assume  b = 0 ; ::_thesis: a lcm b = 0
then  0 divides a lcm b by Def1;
hence  a lcm b = 0 by Th3; ::_thesis: verum
end;
A2: ( not a lcm b = 0 or a = 0 or b = 0 )
proof
A3: ( b divides b implies b divides b * a ) by Th2;
assume A4: a lcm b = 0 ; ::_thesis: ( a = 0 or b = 0 )
 ( a divides a implies a divides a * b ) by Th2;
then  0 divides a * b by A4, A3, Def1;
then  a * b = 0 by Th3;
hence  ( a = 0 or b = 0 ) by XCMPLX_1:6; ::_thesis: verum
end;
 ( a = 0 implies a lcm b = 0 )
proof
assume  a = 0 ; ::_thesis: a lcm b = 0
then  0 divides a lcm b by Def1;
hence  a lcm b = 0 by Th3; ::_thesis: verum
end;
hence  ( ( a = 0 or b = 0 ) iff a lcm b = 0 ) by A1, A2; ::_thesis: verum
end;

Lm9:  for j, i being Nat st 0 < j & i divides j holds
i <= j
proof
let j, i be Nat; ::_thesis: ( 0 < j & i divides j implies i <= j )
assume that
A1: 0 < j and
A2: i divides j ; ::_thesis: i <= j
consider l being Nat such that
A3: j = i * l by A2, Lm7;
 l <> 0 by A1, A3;
then consider k being Nat such that
A4: l = k + 1 by NAT_1:6;
 i * (k + 1) = i + (i * k) ;
hence  i <= j by A3, A4, NAT_1:11; ::_thesis: verum
end;

definition
let a, b be Integer;
funca 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
 ex b1 being Nat st
( b1 divides a & b1 divides b & ( for m being Integer st m divides a & m divides b holds
m divides b1 ) )
proof
percases ( a = 0 or b = 0 or ( a <> 0 & b <> 0 ) ) ;
supposeA1: a = 0 ; ::_thesis: ex b1 being Nat st
( b1 divides a & b1 divides b & ( for m being Integer st m divides a & m divides b holds
m divides b1 ) )
 b in INT by INT_1:def_2;
then consider k being Element of NAT  such that
A2: ( b = k or b = - k ) by INT_1:def_1;
take  k ; ::_thesis: ( k divides a & k divides b & ( for m being Integer st m divides a & m divides b holds
m divides k ) )
thus  ( k divides a & k divides b ) by A1, A2, Lm4, Lm5; ::_thesis: for m being Integer st m divides a & m divides b holds
m divides k
let m be Integer; ::_thesis: ( m divides a & m divides b implies m divides k )
assume that
 m divides a and
A3: m divides b ; ::_thesis: m divides k
thus  m divides k by A2, A3, Lm3; ::_thesis: verum
end;
supposeA4: b = 0 ; ::_thesis: ex b1 being Nat st
( b1 divides a & b1 divides b & ( for m being Integer st m divides a & m divides b holds
m divides b1 ) )
 a in INT by INT_1:def_2;
then consider k being Element of NAT  such that
A5: ( a = k or a = - k ) by INT_1:def_1;
take  k ; ::_thesis: ( k divides a & k divides b & ( for m being Integer st m divides a & m divides b holds
m divides k ) )
thus  ( k divides a & k divides b ) by A4, A5, Lm4, Lm5; ::_thesis: for m being Integer st m divides a & m divides b holds
m divides k
let m be Integer; ::_thesis: ( m divides a & m divides b implies m divides k )
assume that
A6: m divides a and
 m divides b ; ::_thesis: m divides k
thus  m divides k by A5, A6, Lm3; ::_thesis: verum
end;
supposeA7: ( a <> 0 & b <> 0 ) ; ::_thesis: ex b1 being Nat st
( b1 divides a & b1 divides b & ( for m being Integer st m divides a & m divides b holds
m divides b1 ) )
defpred S1[ Nat] means ( $1 divides a & $1 divides b & $1 <> 0 );
A8: a divides a * b by INT_1:def_3;
 a * b in INT by INT_1:def_2;
then consider k being Element of NAT  such that
A9: ( a * b = k or a * b = - k ) by INT_1:def_1;
 k <> 0 by A7, A9, XCMPLX_1:6;
then A10: k > 0 by NAT_1:3;
A11: for i being Nat st S1[i] holds
i <= k
proof
let i be Nat; ::_thesis: ( S1[i] implies i <= k )
assume  S1[i] ; ::_thesis: i <= k
then  i divides a * b by A8, Lm2;
then  i divides k by A9, Lm3;
hence  i <= k by A10, Lm9; ::_thesis: verum
end;
 ( 1 divides a & 1 divides b ) by Lm5;
then A12: ex k being Nat st S1[k] ;
consider k being Nat such that
A13: S1[k] and
A14: for n being Nat st S1[n] holds
n <= k from NAT_1:sch_6(A11, A12);
take  k ; ::_thesis: ( k divides a & k divides b & ( for m being Integer st m divides a & m divides b holds
m divides k ) )
thus  ( k divides a & k divides b ) by A13; ::_thesis: for m being Integer st m divides a & m divides b holds
m divides k
let m be Integer; ::_thesis: ( m divides a & m divides b implies m divides k )
assume that
A15: m divides a and
A16: m divides b ; ::_thesis: m divides k
 m in INT by INT_1:def_2;
then consider n being Element of NAT  such that
A17: ( m = n or m = - n ) by INT_1:def_1;
set i = n lcm k;
A18: k divides n lcm k by Def1;
A19: now__::_thesis:_not_n_lcm_k_=_0
assume  n lcm k = 0 ; ::_thesis: contradiction
then  ( n = 0 or k = 0 ) by Th4;
hence  contradiction by A7, A13, A17, A15, Th3; ::_thesis: verum
end;
then  0 < n lcm k by NAT_1:3;
then A20: k <= n lcm k by A18, Lm9;
 n divides b by A17, A16, Lm4;
then A21: n lcm k divides b by A13, Def1;
 n divides a by A17, A15, Lm4;
then  n lcm k divides a by A13, Def1;
then  k >= n lcm k by A14, A21, A19;
then  k = n lcm k by A20, XXREAL_0:1;
then A22: n divides k by Def1;
assume  not m divides k ; ::_thesis: contradiction
hence  contradiction by A17, A22, Lm4; ::_thesis: verum
end;
end;
end;
uniqueness
 for b1, b2 being Nat st b1 divides a & b1 divides b & ( for m being Integer st m divides a & m divides b holds
m divides b1 ) & b2 divides a & b2 divides b & ( for m being Integer st m divides a & m divides b holds
m divides b2 ) holds
b1 = b2
proof
let IT1, IT2 be Nat; ::_thesis: ( IT1 divides a & IT1 divides b & ( for m being Integer st m divides a & m divides b holds
m divides IT1 ) & IT2 divides a & IT2 divides b & ( for m being Integer st m divides a & m divides b holds
m divides IT2 ) implies IT1 = IT2 )
assume  ( IT1 divides a & IT1 divides b & ( for m being Integer st m divides a & m divides b holds
m divides IT1 ) & IT2 divides a & IT2 divides b & ( for m being Integer st m divides a & m divides b holds
m divides IT2 ) ) ; ::_thesis: IT1 = IT2
then  ( IT1 divides IT2 & IT2 divides IT1 ) ;
hence  IT1 = IT2 by Lm8; ::_thesis: verum
end;
commutativity
 for b1 being Nat
for a, b being Integer st b1 divides a & b1 divides b & ( for m being Integer st m divides a & m divides b holds
m divides b1 ) holds
( b1 divides b & b1 divides a & ( for m being Integer st m divides b & 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 & b3 divides b & ( for m being Integer st m divides a & m divides b holds
m divides b3 ) ) );

theorem Th5: :: INT_2:5
for a, b being Integer holds
( ( a = 0 & b = 0 ) iff a gcd b = 0 )
proof
let a, b be Integer; ::_thesis: ( ( a = 0 & b = 0 ) iff a gcd b = 0 )
 0 divides 0 gcd 0 by Def2;
hence  ( a = 0 & b = 0 implies a gcd b = 0 ) by Th3; ::_thesis: ( a gcd b = 0 implies ( a = 0 & b = 0 ) )
assume  a gcd b = 0 ; ::_thesis: ( a = 0 & b = 0 )
then  ( 0 divides a & 0 divides b ) by Def2;
hence  ( a = 0 & b = 0 ) by Th3; ::_thesis: verum
end;


theorem Th6: :: INT_2:6
for n being Nat holds
( - n is Element of NAT iff n = 0 )
proof
let n be Nat; ::_thesis: ( - n is Element of NAT iff n = 0 )
thus  ( - n is Element of NAT implies n = 0 ) ::_thesis: ( n = 0 implies - n is Element of NAT )
proof
assume  - n is Element of NAT ; ::_thesis: n = 0
then  ( - n >= 0 & n + (- n) >= 0 + n ) by NAT_1:2;
hence  n = 0 ; ::_thesis: verum
end;
thus  ( n = 0 implies - n is Element of NAT ) ; ::_thesis: verum
end;

registration
let n be non zero Nat;
cluster - n ->  non natural ;
coherence
 not - n is natural
proof
 - n is not Element of NAT by Th6;
hence  not - n is natural by ORDINAL1:def_12; ::_thesis: verum
end;
end;

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

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

theorem :: INT_2:9
for a, b, c being Integer st a divides b & 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 ) & ( 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
let a, b be Integer; ::_thesis: ( ( 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 ) )
A1: ( a divides b implies a divides - b )
proof
assume A2: a divides b ; ::_thesis: a divides - b
 b divides - b by Lm1;
hence  a divides - b by A2, Lm2; ::_thesis: verum
end;
A3: ( a divides - b implies a divides b )
proof
assume A4: a divides - b ; ::_thesis: a divides b
 - b divides b by Lm1;
hence  a divides b by A4, Lm2; ::_thesis: verum
end;
hence  ( a divides b iff a divides - b ) by A1; ::_thesis: ( ( 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 ) )
A5: ( - a divides b implies a divides b )
proof
assume A6: - a divides b ; ::_thesis: a divides b
 a divides - a by Lm1;
hence  a divides b by A6, Lm2; ::_thesis: verum
end;
A7: ( - a divides - b implies a divides b )
proof
assume A8: - a divides - b ; ::_thesis: a divides b
 - b divides b by Lm1;
hence  a divides b by A5, A8, Lm2; ::_thesis: verum
end;
A9: ( a divides b implies - a divides b )
proof
assume A10: a divides b ; ::_thesis: - a divides b
 - a divides a by Lm1;
hence  - a divides b by A10, Lm2; ::_thesis: verum
end;
hence  ( a divides b iff - a divides b ) by A5; ::_thesis: ( ( 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
assume A11: a divides b ; ::_thesis: - a divides - b
 - a divides a by Lm1;
hence  - a divides - b by A1, A11, Lm2; ::_thesis: verum
end;
hence  ( a divides b iff - a divides - b ) by A7; ::_thesis: ( a divides - b iff - a divides b )
thus  ( a divides - b iff - a divides b ) by A1, A3, A9, A5; ::_thesis: verum
end;

theorem :: INT_2:11
for a, b being Integer st a divides b & b divides a & not a = b holds
a = - b
proof
let a, b be Integer; ::_thesis: ( a divides b & b divides a & not a = b implies a = - b )
assume that
A1: a divides b and
A2: b divides a ; ::_thesis: ( a = b or a = - b )
consider a1 being Integer such that
A3: b = a * a1 by A1, INT_1:def_3;
consider b1 being Integer such that
A4: a = b * b1 by A2, INT_1:def_3;
 ( not a <> 0 or a = b or a = - b )
proof
assume A5: a <> 0 ; ::_thesis: ( a = b or a = - b )
 1 * a = a * (a1 * b1) by A3, A4;
then  a1 * b1 = 1 by A5, XCMPLX_1:5;
then  ( a = b * 1 or a = b * (- 1) ) by A4, INT_1:9;
hence  ( a = b or a = - b ) ; ::_thesis: verum
end;
hence  ( a = b or a = - b ) by A1, Th3; ::_thesis: verum
end;

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

theorem Th13: :: INT_2:13
for a being Integer holds
( ( not a divides 1 & not a divides - 1 ) or a = 1 or a = - 1 )
proof
let a be Integer; ::_thesis: ( ( not a divides 1 & not a divides - 1 ) or a = 1 or a = - 1 )
A1: ( not a divides 1 or a = 1 or a = - 1 )
proof
assume  a divides 1 ; ::_thesis: ( a = 1 or a = - 1 )
then  ex b being Integer st 1 = a * b by INT_1:def_3;
hence  ( a = 1 or a = - 1 ) by INT_1:9; ::_thesis: verum
end;
A2: ( not a divides - 1 or a = 1 or a = - 1 )
proof
assume  a divides - 1 ; ::_thesis: ( a = 1 or a = - 1 )
then  ex b being Integer st - 1 = a * b by INT_1:def_3;
hence  ( a = 1 or a = - 1 ) by INT_1:10; ::_thesis: verum
end;
assume  ( a divides 1 or a divides - 1 ) ; ::_thesis: ( a = 1 or a = - 1 )
hence  ( a = 1 or a = - 1 ) by A1, A2; ::_thesis: verum
end;

theorem :: INT_2:14
for a being Integer st ( a = 1 or a = - 1 ) holds
( a divides 1 & 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 )
proof
let a, b, c be Integer; ::_thesis: ( a,b are_congruent_mod c iff c divides a - b )
thus  ( a,b are_congruent_mod c implies c divides a - b ) ::_thesis: ( c divides a - b implies a,b are_congruent_mod c )
proof
assume  a,b are_congruent_mod c ; ::_thesis: c divides a - b
then  ex d being Integer st a - b = c * d by INT_1:def_5;
hence  c divides a - b by INT_1:def_3; ::_thesis: verum
end;
assume  c divides a - b ; ::_thesis: a,b are_congruent_mod c
then  ex d being Integer st a - b = c * d by INT_1:def_3;
hence  a,b are_congruent_mod c by INT_1:def_5; ::_thesis: verum
end;

theorem :: INT_2:16
for a, b being Integer holds
( a divides b iff abs a divides abs b )
proof
let a, b be Integer; ::_thesis: ( a divides b iff abs a divides abs b )
thus  ( a divides b implies abs a divides abs b ) ::_thesis: ( abs a divides abs b implies a divides b )
proof
assume  a divides b ; ::_thesis: abs a divides abs b
then consider c being Integer such that
A1: b = a * c by INT_1:def_3;
 abs b = (abs a) * (abs c) by A1, COMPLEX1:65;
hence  abs a divides abs b by INT_1:def_3; ::_thesis: verum
end;
assume  abs a divides abs b ; ::_thesis: a divides b
then consider m being Integer such that
A2: abs b = (abs a) * m by INT_1:def_3;
A3: ( a >= 0 implies a divides b )
proof
assume  a >= 0 ; ::_thesis: a divides b
then A4: abs b = a * m by A2, ABSVALUE:def_1;
percases ( b < 0 or b >= 0 ) ;
suppose b < 0 ; ::_thesis: a divides b
then  - b = a * m by A4, ABSVALUE:def_1;
then  b = a * (- m) ;
hence  a divides b by INT_1:def_3; ::_thesis: verum
end;
suppose b >= 0 ; ::_thesis: a divides b
then  b = a * m by A4, ABSVALUE:def_1;
hence  a divides b by INT_1:def_3; ::_thesis: verum
end;
end;
end;
 ( a < 0 implies a divides b )
proof
assume  a < 0 ; ::_thesis: a divides b
then A5: abs b = (- a) * m by A2, ABSVALUE:def_1;
percases ( b < 0 or b >= 0 ) ;
suppose b < 0 ; ::_thesis: a divides b
then  - b = - (a * m) by A5, ABSVALUE:def_1;
hence  a divides b by INT_1:def_3; ::_thesis: verum
end;
suppose b >= 0 ; ::_thesis: a divides b
then  b = a * (- m) by A5, ABSVALUE:def_1;
hence  a divides b by INT_1:def_3; ::_thesis: verum
end;
end;
end;
hence  a divides b by A3; ::_thesis: verum
end;

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 & 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 & c divides b holds
c divides a gcd b by Def2;

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 & b = (a gcd b) * b1 & a1,b1 are_relative_prime )
proof
let a, b be Integer; ::_thesis: ( ( a <> 0 or b <> 0 ) implies ex a1, b1 being Integer st
( a = (a gcd b) * a1 & b = (a gcd b) * b1 & a1,b1 are_relative_prime ) )
assume  ( a <> 0 or b <> 0 ) ; ::_thesis: ex a1, b1 being Integer st
( a = (a gcd b) * a1 & b = (a gcd b) * b1 & a1,b1 are_relative_prime )
then A1: a gcd b <> 0 by Th5;
 a gcd b divides a by Def2;
then consider a1 being Integer such that
A2: a = (a gcd b) * a1 by INT_1:def_3;
 a gcd b divides b by Def2;
then consider b1 being Integer such that
A3: b = (a gcd b) * b1 by INT_1:def_3;
 a1 gcd b1 divides b1 by Def2;
then consider b2 being Integer such that
A4: b1 = (a1 gcd b1) * b2 by INT_1:def_3;
 b = ((a gcd b) * (a1 gcd b1)) * b2 by A3, A4;
then A5: (a gcd b) * (a1 gcd b1) divides b by INT_1:def_3;
 a1 gcd b1 divides a1 by Def2;
then consider a2 being Integer such that
A6: a1 = (a1 gcd b1) * a2 by INT_1:def_3;
 a = ((a gcd b) * (a1 gcd b1)) * a2 by A2, A6;
then  (a gcd b) * (a1 gcd b1) divides a by INT_1:def_3;
then  (a gcd b) * (a1 gcd b1) divides a gcd b by A5, Def2;
then consider c being Integer such that
A7: a gcd b = ((a gcd b) * (a1 gcd b1)) * c by INT_1:def_3;
 (a gcd b) * 1 = (a gcd b) * ((a1 gcd b1) * c) by A7;
then  1 = (a1 gcd b1) * c by A1, XCMPLX_1:5;
then  ( a1 gcd b1 = 1 or a1 gcd b1 = - 1 ) by INT_1:9;
then  a1,b1 are_relative_prime by Def3;
hence  ex a1, b1 being Integer st
( a = (a gcd b) * a1 & b = (a gcd b) * b1 & a1,b1 are_relative_prime ) by A2, A3; ::_thesis: verum
end;

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 & (c * a) gcd (b * c) = abs c & (a * c) gcd (c * b) = abs c & (a * c) gcd (b * c) = abs c )
proof
let a, b, c be Integer; ::_thesis: ( a,b are_relative_prime implies ( (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 ) )
assume  a,b are_relative_prime ; ::_thesis: ( (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 )
then A1: a gcd b = 1 by Def3;
thus A2: (c * a) gcd (c * b) = abs c ::_thesis: ( (c * a) gcd (b * c) = abs c & (a * c) gcd (c * b) = abs c & (a * c) gcd (b * c) = abs c )
proof
 (c * a) gcd (c * b) divides c * b by Def2;
then consider l being Integer such that
A3: c * b = ((c * a) gcd (c * b)) * l by INT_1:def_3;
 (c * a) gcd (c * b) divides c * a by Def2;
then consider k being Integer such that
A4: c * a = ((c * a) gcd (c * b)) * k by INT_1:def_3;
 ( c divides c * a & c divides c * b ) by Th2;
then  c divides (c * a) gcd (c * b) by Def2;
then consider d being Integer such that
A5: (c * a) gcd (c * b) = c * d by INT_1:def_3;
A6: c * b = c * (d * l) by A5, A3;
A7: c * a = c * (d * k) by A5, A4;
A8: ( c <> 0 implies (c * a) gcd (c * b) = abs c )
proof
assume A9: c <> 0 ; ::_thesis: (c * a) gcd (c * b) = abs c
then  b = d * l by A6, XCMPLX_1:5;
then A10: d divides b by INT_1:def_3;
 a = d * k by A7, A9, XCMPLX_1:5;
then  d divides a by INT_1:def_3;
then  d divides 1 by A1, A10, Def2;
then  ( (c * a) gcd (c * b) = c * 1 or (c * a) gcd (c * b) = c * (- 1) ) by A5, Th13;
then  ( (c * a) gcd (c * b) = c * 1 or (c * a) gcd (c * b) = (- c) * 1 ) ;
then A11: abs ((c * a) gcd (c * b)) = abs c by COMPLEX1:52;
 (c * a) gcd (c * b) >= 0 by NAT_1:2;
hence  (c * a) gcd (c * b) = abs c by A11, ABSVALUE:def_1; ::_thesis: verum
end;
(0 * a) gcd (0 * b) = 0 by Th5
.= abs 0 by ABSVALUE:2 ;
hence  (c * a) gcd (c * b) = abs c by A8; ::_thesis: verum
end;
hence  (c * a) gcd (b * c) = abs c ; ::_thesis: ( (a * c) gcd (c * b) = abs c & (a * c) gcd (b * c) = abs c )
thus  ( (a * c) gcd (c * b) = abs c & (a * c) gcd (b * c) = abs c ) by A2; ::_thesis: verum
end;

theorem Th25: :: INT_2:25
for c, a, b being Integer st c divides a * b & a,c are_relative_prime holds
c divides b
proof
let c, a, b be Integer; ::_thesis: ( c divides a * b & a,c are_relative_prime implies c divides b )
assume that
A1: c divides a * b and
A2: a,c are_relative_prime ; ::_thesis: c divides b
 c divides c * b by Th2;
then A3: c divides (a * b) gcd (c * b) by A1, Def2;
A4: (a * b) gcd (c * b) = abs b by A2, Th24;
 ( b < 0 implies c divides b )
proof
assume  b < 0 ; ::_thesis: c divides b
then  c divides - b by A4, A3, ABSVALUE:def_1;
hence  c divides b by Th10; ::_thesis: verum
end;
hence  c divides b by A4, A3, ABSVALUE:def_1; ::_thesis: verum
end;

theorem :: INT_2:26
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
let a, c, b be Integer; ::_thesis: ( a,c are_relative_prime & b,c are_relative_prime implies a * b,c are_relative_prime )
assume that
A1: a,c are_relative_prime and
A2: b,c are_relative_prime ; ::_thesis: a * b,c are_relative_prime
A3: a gcd c = 1 by A1, Def3;
A4: ((a * b) gcd c) gcd a divides a by Def2;
A5: (a * b) gcd c divides c by Def2;
 ((a * b) gcd c) gcd a divides (a * b) gcd c by Def2;
then  ((a * b) gcd c) gcd a divides c by A5, Lm2;
then  ((a * b) gcd c) gcd a divides 1 by A3, A4, Def2;
then  ( ((a * b) gcd c) gcd a = 1 or ((a * b) gcd c) gcd a = - 1 ) by Th13;
then  a,(a * b) gcd c are_relative_prime by Def3;
then A6: (a * b) gcd c divides b by Th21, Th25;
 b gcd c = 1 by A2, Def3;
then  (a * b) gcd c divides 1 by A5, A6, Def2;
then  ( (a * b) gcd c = 1 or (a * b) gcd c = - 1 ) by Th13;
hence  a * b,c are_relative_prime by Def3; ::_thesis: verum
end;


definition
let p be Nat;
attrp is prime  means :Def4: :: INT_2:def 4
( p > 1 & ( 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 & ( 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 & a divides b holds
a <= b
proof
let b, a be Integer; ::_thesis: ( 0 < b & a divides b implies a <= b )
assume A1: 0 < b ; ::_thesis: ( not a divides b or a <= b )
assume  a divides b ; ::_thesis: a <= b
then consider c being Integer such that
A2: b = a * c by INT_1:def_3;
percases ( a <= 0 or a > 0 ) ;
suppose a <= 0 ; ::_thesis: a <= b
hence  a <= b by A1, XXREAL_0:2; ::_thesis: verum
end;
supposeA3: a > 0 ; ::_thesis: a <= b
then  c > 0 by A1, A2, XREAL_1:131;
then  c >= 0 + 1 by INT_1:7;
hence  a <= b by A2, A3, XREAL_1:151; ::_thesis: verum
end;
end;
end;

theorem Th28: :: INT_2:28
2 is prime
proof
thus  2 > 1 ; :: according to INT_2:def_4 ::_thesis: for n being Nat holds
( not n divides 2 or n = 1 or n = 2 )
let n be Nat; ::_thesis: ( not n divides 2 or n = 1 or n = 2 )
assume A1: n divides 2 ; ::_thesis: ( n = 1 or n = 2 )
then  n <= 2 by Th27;
then  ( n = 0 or n = 1 or n = 2 ) by NAT_1:26;
hence  ( n = 1 or n = 2 ) by A1, Th3; ::_thesis: verum
end;

theorem Th29: :: INT_2:29
not 4 is prime
proof
 ex n being Nat st
( n divides 4 & n <> 1 & n <> 4 )
proof
take  2 ; ::_thesis: ( 2 divides 4 & 2 <> 1 & 2 <> 4 )
 4 = 2 * 2 ;
hence  ( 2 divides 4 & 2 <> 1 & 2 <> 4 ) by INT_1:def_3; ::_thesis: verum
end;
hence  not 4 is prime by Def4; ::_thesis: verum
end;

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 & not b1 is prime ) by Th29;
end;

theorem :: INT_2:30
for p, q being Nat st p is prime & q is prime & not p,q are_relative_prime holds
p = q
proof
let p, q be Nat; ::_thesis: ( p is prime & q is prime & not p,q are_relative_prime implies p = q )
assume that
A1: p is prime and
A2: q is prime ; ::_thesis: ( p,q are_relative_prime or p = q )
A3: p gcd q divides q by Def2;
assume  not p,q are_relative_prime ; ::_thesis: p = q
then A4: p gcd q <> 1 by Def3;
 p gcd q divides p by Def2;
then  p gcd q = p by A1, A4, Def4;
hence  p = q by A2, A4, A3, Def4; ::_thesis: verum
end;

theorem :: INT_2:31
for l being Nat st l >= 2 holds
ex p being Element of NAT st
( p is prime & p divides l )
proof
let l be Nat; ::_thesis: ( l >= 2 implies ex p being Element of NAT st
( p is prime & p divides l ) )
defpred S1[ Nat] means  ex p being Nat st
( p is prime & p divides $1 );
A1: for k being Nat st k >= 2 & ( for n being Nat st n >= 2 & n < k holds
S1[n] ) holds
S1[k]
proof
let k be Nat; ::_thesis: ( k >= 2 & ( for n being Nat st n >= 2 & n < k holds
S1[n] ) implies S1[k] )
assume A2: k >= 2 ; ::_thesis: ( ex n being Nat st
( n >= 2 & n < k & not S1[n] ) or S1[k] )
assume A3: for n being Nat st n >= 2 & n < k holds
ex p being Nat st
( p is prime & p divides n ) ; ::_thesis: S1[k]
A4: (k + 1) - 1 > (1 + 1) - 1 by A2, NAT_1:13;
 ( not k is prime implies ex p being Element of NAT st
( p is prime & p divides k ) )
proof
assume  not k is prime ; ::_thesis: ex p being Element of NAT st
( p is prime & p divides k )
then consider m being Nat such that
A5: m divides k and
A6: m <> 1 and
A7: m <> k by A4, Def4;
 m <> 0 by A5, A7, Th3;
then  m > 0 by NAT_1:3;
then  m >= 0 + 1 by NAT_1:13;
then  m > 1 by A6, XXREAL_0:1;
then A8: m >= 1 + 1 by NAT_1:13;
 k > 0 by A2, XXREAL_0:2;
then  m <= k by A5, Th27;
then  m < k by A7, XXREAL_0:1;
then consider p1 being Nat such that
A9: ( p1 is prime & p1 divides m ) by A3, A8;
reconsider p1 = p1 as Element of NAT by ORDINAL1:def_12;
take  p1 ; ::_thesis: ( p1 is prime & p1 divides k )
thus  ( p1 is prime & p1 divides k ) by A5, A9, Lm2; ::_thesis: verum
end;
hence  S1[k] ; ::_thesis: verum
end;
A10: for k being Nat st k >= 2 holds
S1[k] from NAT_1:sch_9(A1);
assume  l >= 2 ; ::_thesis: ex p being Element of NAT st
( p is prime & p divides l )
then consider p being Nat such that
A11: ( p is prime & p divides l ) by A10;
reconsider p = p as Element of NAT by ORDINAL1:def_12;
take  p ; ::_thesis: ( p is prime & p divides l )
thus  ( p is prime & p divides l ) by A11; ::_thesis: verum
end;

begin

theorem :: INT_2:32
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
let i, j be Integer; ::_thesis: ( i >= 0 & j >= 0 implies ( (abs i) mod (abs j) = i mod j & (abs i) div (abs j) = i div j ) )
assume that
A1: i >= 0 and
A2: j >= 0 ; ::_thesis: ( (abs i) mod (abs j) = i mod j & (abs i) div (abs j) = i div j )
percases ( j > 0 or j = 0 ) by A2, XXREAL_0:1;
supposeA3: j > 0 ; ::_thesis: ( (abs i) mod (abs j) = i mod j & (abs i) div (abs j) = i div j )
 i = abs i by A1, ABSVALUE:def_1;
hence  ( (abs i) mod (abs j) = i mod j & (abs i) div (abs j) = i div j ) by A3, ABSVALUE:def_1; ::_thesis: verum
end;
supposeA4: j = 0 ; ::_thesis: ( (abs i) mod (abs j) = i mod j & (abs i) div (abs j) = i div j )
 abs 0 = 0 by ABSVALUE:def_1;
then  ( (abs i) mod (abs 0) = 0 & (abs i) div (abs 0) = 0 ) by INT_1:48, INT_1:def_10;
hence  ( (abs i) mod (abs j) = i mod j & (abs i) div (abs j) = i div j ) by A4, INT_1:48, INT_1:def_10; ::_thesis: verum
end;
end;
end;

theorem :: INT_2:33
for a, b being Integer holds a lcm b = (abs a) lcm (abs b)
proof
let a, b be Integer; ::_thesis: a lcm b = (abs a) lcm (abs b)
A1: ( abs b = b or abs b = - b ) by ABSVALUE:1;
A2: ( abs a = a or abs a = - a ) by ABSVALUE:1;
A3: now__::_thesis:_for_m_being_Integer_st_abs_a_divides_m_&_abs_b_divides_m_holds_
a_lcm_b_divides_m
let m be Integer; ::_thesis: ( abs a divides m & abs b divides m implies a lcm b divides m )
assume  ( abs a divides m & abs b divides m ) ; ::_thesis: a lcm b divides m
then  ( a divides m & b divides m ) by A2, A1, Th10;
hence  a lcm b divides m by Def1; ::_thesis: verum
end;
 b divides a lcm b by Def1;
then A4: abs b divides a lcm b by A1, Th10;
 a divides a lcm b by Def1;
then  abs a divides a lcm b by A2, Th10;
hence  a lcm b = (abs a) lcm (abs b) by A4, A3, Def1; ::_thesis: verum
end;

theorem :: INT_2:34
for a, b being Integer holds a gcd b = (abs a) gcd (abs b)
proof
let a, b be Integer; ::_thesis: a gcd b = (abs a) gcd (abs b)
A1: ( abs b = b or abs b = - b ) by ABSVALUE:1;
A2: ( abs a = a or abs a = - a ) by ABSVALUE:1;
A3: now__::_thesis:_for_m_being_Integer_st_m_divides_abs_a_&_m_divides_abs_b_holds_
m_divides_a_gcd_b
let m be Integer; ::_thesis: ( m divides abs a & m divides abs b implies m divides a gcd b )
assume  ( m divides abs a & m divides abs b ) ; ::_thesis: m divides a gcd b
then  ( m divides a & m divides b ) by A2, A1, Th10;
hence  m divides a gcd b by Def2; ::_thesis: verum
end;
 a gcd b divides b by Def2;
then A4: a gcd b divides abs b by A1, Th10;
 a gcd b divides a by Def2;
then  a gcd b divides abs a by A2, Th10;
hence  a gcd b = (abs a) gcd (abs b) by A4, A3, Def2; ::_thesis: verum
end;