let a, b be Integer; :: thesis: a gcd b = (abs a) gcd (abs b)
A1: ( abs a = a or abs a = - a ) by ABSVALUE:1;
a gcd b divides a by Def3;
then A2: a gcd b divides abs a by A1, Th14;
A3: ( abs b = b or abs b = - b ) by ABSVALUE:1;
a gcd b divides b by Def3;
then A4: a gcd b divides abs b by A3, Th14;

now

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 A1, A3, Th14;
hence m divides a gcd b by Def3; :: thesis: verum

end;

hence a gcd b = (abs a) gcd (abs b) by A2, A4, Def3; :: thesis: verum