let i, j be Integer; :: thesis: (i * j) gcd i = abs i
A1: for m being Integer st m divides i * j & m divides i holds
m divides abs i

proof

let m be Integer; :: thesis: ( m divides i * j & m divides i implies m divides abs i )
assume that
m divides i * j and
A2: m divides i ; :: thesis: m divides abs i
consider k being Integer such that
A3: m * k = i by A2, INT_1:def 3;
i divides abs i by Th13;
then consider l being Integer such that
A4: i * l = abs i by INT_1:def 3;
m * (k * l) = abs i by A3, A4;
hence m divides abs i by INT_1:def 3; :: thesis: verum

end;

A5: abs i divides i by Th13;
then abs i divides i * j by INT_2:2;
hence (i * j) gcd i = abs i by A5, A1, INT_2:def 2; :: thesis: verum