let i, j be Integer; :: thesis: (i * j) gcd i = |.i.|
A1: for m being Integer st m divides i * j & m divides i holds
m divides |.i.|
proof
let m be Integer; :: thesis: ( m divides i * j & m divides i implies m divides |.i.| )
assume that
m divides i * j and
A2: m divides i ; :: thesis: m divides |.i.|
consider k being Integer such that
A3: m * k = i by A2, INT_1:def 3;
i divides |.i.| by Th13;
then consider l being Integer such that
A4: i * l = |.i.| by INT_1:def 3;
m * (k * l) = |.i.| by A3, A4;
hence m divides |.i.| by INT_1:def 3; :: thesis: verum
end;
A5: |.i.| divides i by Th13;
then |.i.| divides i * j by INT_2:2;
hence (i * j) gcd i = |.i.| by A5, A1, INT_2:def 2; :: thesis: verum