let a, b be Integer; :: thesis: a gcd b = |.a.| gcd |.b.|

A1: ( |.b.| = b or |.b.| = - b ) by ABSVALUE:1;

A2: ( |.a.| = a or |.a.| = - a ) by ABSVALUE:1;

then A4: a gcd b divides |.b.| by A1, Th10;

a gcd b divides a by Def2;

then a gcd b divides |.a.| by A2, Th10;

hence a gcd b = |.a.| gcd |.b.| by A4, A3, Def2; :: thesis: verum

A1: ( |.b.| = b or |.b.| = - b ) by ABSVALUE:1;

A2: ( |.a.| = a or |.a.| = - a ) by ABSVALUE:1;

A3: now :: thesis: for m being Integer st m divides |.a.| & m divides |.b.| holds

m divides a gcd b

a gcd b divides b
by Def2;m divides a gcd b

let m be Integer; :: thesis: ( m divides |.a.| & m divides |.b.| implies m divides a gcd b )

assume ( m divides |.a.| & m divides |.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;assume ( m divides |.a.| & m divides |.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

then A4: a gcd b divides |.b.| by A1, Th10;

a gcd b divides a by Def2;

then a gcd b divides |.a.| by A2, Th10;

hence a gcd b = |.a.| gcd |.b.| by A4, A3, Def2; :: thesis: verum