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.|

then |.i.| divides i * j by INT_2:2;

hence (i * j) gcd i = |.i.| by A5, A1, INT_2:def 2; :: thesis: verum

A1: for m being Integer st m divides i * j & m divides i holds

m divides |.i.|

proof

A5:
|.i.| divides i
by Th13;
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;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

then |.i.| divides i * j by INT_2:2;

hence (i * j) gcd i = |.i.| by A5, A1, INT_2:def 2; :: thesis: verum