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

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

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

(i gcd |.j.|) * (x * y) = j
by A1, A2;
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;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

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