let i, j be Integer; :: thesis: i gcd j = i gcd (abs j)
set k = i gcd (abs j);
A: i gcd (abs j) divides i by INT_2:def 3;
i gcd (abs j) divides abs j by INT_2:def 3;
then consider x being Integer such that
H: (i gcd (abs j)) * x = abs j by INT_1:def 9;
abs j divides j by thabs0;
then consider y being Integer such that
K: (abs j) * y = j by INT_1:def 9;
(i gcd (abs j)) * (x * y) = j by H, K;
then B: i gcd (abs j) divides j by INT_1:def 9;
for m being Integer st m divides i & m divides j holds
m divides i gcd (abs j)

proof

let m be Integer; :: thesis: ( m divides i & m divides j implies m divides i gcd (abs j) )
assume AS: ( m divides i & m divides j ) ; :: thesis: m divides i gcd (abs j)
then consider x being Integer such that
H: m * x = j by INT_1:def 9;
j divides abs j by thabs0;
then consider y being Integer such that
H1: j * y = abs j by INT_1:def 9;
m * (x * y) = abs j by H, H1;
then m divides abs j by INT_1:def 9;
hence m divides i gcd (abs j) by AS, INT_2:def 3; :: thesis: verum

end;

hence i gcd j = i gcd (abs j) by A, B, INT_2:def 3; :: thesis: verum