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