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