let i, j, k be Integer; :: thesis: (i * j) gcd (i * k) = |.i.| * (j gcd k)

per cases ( i = 0 or i <> 0 ) ;

suppose A1: i = 0 ; :: thesis: (i * j) gcd (i * k) = |.i.| * (j gcd k)

hence (i * j) gcd (i * k) = 0 * (j gcd k) by INT_2:5
.= |.i.| * (j gcd k) by A1, ABSVALUE:def 1 ;
:: thesis: verum

end;

suppose A2: i <> 0 ; :: thesis: (i * j) gcd (i * k) = |.i.| * (j gcd k)

set d = j gcd k;
set e = (i * j) gcd (i * k);

per cases ( j gcd k = 0 or j gcd k <> 0 ) ;

suppose A3: j gcd k = 0 ; :: thesis: (i * j) gcd (i * k) = |.i.| * (j gcd k)

then A4: k = 0 by INT_2:5;
j = 0 by A3, INT_2:5;
hence (i * j) gcd (i * k) = |.i.| * (j gcd k) by A3, A4; :: thesis: verum

end;

suppose A5: j gcd k <> 0 ; :: thesis: (i * j) gcd (i * k) = |.i.| * (j gcd k)

A6: (i * j) gcd (i * k) divides i * k by INT_2:21;
A7: i * (j gcd k) divides i * k by Th8, INT_2:21;
i * (j gcd k) divides i * j by Th8, INT_2:21;
then i * (j gcd k) divides (i * j) gcd (i * k) by A7, INT_2:22;
then consider g being Integer such that
A8: (i * j) gcd (i * k) = (i * (j gcd k)) * g by INT_1:def 3;
A9: (i * j) gcd (i * k) divides i * j by INT_2:21;
( (j gcd k) * g divides j & (j gcd k) * g divides k )

proof

consider h1 being Integer such that
A10: ((i * (j gcd k)) * g) * h1 = i * j by A8, A9, INT_1:def 3;
i * (((j gcd k) * g) * h1) = i * j by A10;
then ((j gcd k) * g) * h1 = j by A2, XCMPLX_1:5;
hence (j gcd k) * g divides j by INT_1:def 3; :: thesis: (j gcd k) * g divides k
consider h2 being Integer such that
A11: ((i * (j gcd k)) * g) * h2 = i * k by A8, A6, INT_1:def 3;
i * (((j gcd k) * g) * h2) = i * k by A11;
then ((j gcd k) * g) * h2 = k by A2, XCMPLX_1:5;
hence (j gcd k) * g divides k by INT_1:def 3; :: thesis: verum

end;

then (j gcd k) * g divides j gcd k by INT_2:22;
then consider h3 being Integer such that
A12: ((j gcd k) * g) * h3 = j gcd k by INT_1:def 3;
(j gcd k) * (g * h3) = (j gcd k) * 1 by A12;
then g * h3 = 1 by A5, XCMPLX_1:5;
then A13: g divides 1 by INT_1:def 3;

per cases ( g = 1 or g = - 1 ) by A13, INT_2:13;

suppose A14: g = 1 ; :: thesis: (i * j) gcd (i * k) = |.i.| * (j gcd k)

( i < 0 implies (j gcd k) * i < 0 * i ) by A5, XREAL_1:69;
hence (i * j) gcd (i * k) = |.i.| * (j gcd k) by A8, A14, ABSVALUE:def 1; :: thesis: verum

end;

suppose A15: g = - 1 ; :: thesis: (i * j) gcd (i * k) = |.i.| * (j gcd k)

A16: now :: thesis: ( i > 0 implies (j gcd k) * (- i) < 0 * (- i) )

assume i > 0 ; :: thesis: (j gcd k) * (- i) < 0 * (- i)
then - (- i) > 0 ;
then - i < 0 ;
hence (j gcd k) * (- i) < 0 * (- i) by A5, XREAL_1:69; :: thesis: verum

end;

(i * j) gcd (i * k) = (- i) * (j gcd k) by A8, A15;
hence (i * j) gcd (i * k) = |.i.| * (j gcd k) by A2, A16, ABSVALUE:def 1; :: thesis: verum

end;

end;

end;

end;

end;

end;