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;
A3: now :: thesis: for m being Integer st m divides |.a.| & m divides |.b.| holds
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;
a gcd b divides b by Def2;
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