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

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

suppose A: i = 0 ; :: thesis: (i * j) gcd (i * k) = (abs i) * (j gcd k)

hence (i * j) gcd (i * k) = 0 * (j gcd k) by INT_2:35
.= (abs i) * (j gcd k) by A, ABSVALUE:def 1 ;
:: thesis: verum

end;

suppose A: i <> 0 ; :: thesis: (i * j) gcd (i * k) = (abs 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 B: j gcd k = 0 ; :: thesis: (i * j) gcd (i * k) = (abs i) * (j gcd k)

then ( j = 0 & k = 0 ) by INT_2:35;
hence (i * j) gcd (i * k) = (abs i) * (j gcd k) by B; :: thesis: verum

end;

suppose B: j gcd k <> 0 ; :: thesis: (i * j) gcd (i * k) = (abs i) * (j gcd k)

then Y3: j gcd k > 0 ;
( i * (j gcd k) divides i * j & i * (j gcd k) divides i * k ) by div0, INT_2:31;
then i * (j gcd k) divides (i * j) gcd (i * k) by INT_2:33;
then consider g being Integer such that
X2: (i * j) gcd (i * k) = (i * (j gcd k)) * g by INT_1:def 9;
Y2: ( (i * j) gcd (i * k) divides i * j & (i * j) gcd (i * k) divides i * k ) by INT_2:31;
( (j gcd k) * g divides j & (j gcd k) * g divides k )

proof

consider h1 being Integer such that
Y: ((i * (j gcd k)) * g) * h1 = i * j by Y2, X2, INT_1:def 9;
i * (((j gcd k) * g) * h1) = i * j by Y;
then ((j gcd k) * g) * h1 = j by A, XCMPLX_1:5;
hence (j gcd k) * g divides j by INT_1:def 9; :: thesis: (j gcd k) * g divides k
consider h2 being Integer such that
Y: ((i * (j gcd k)) * g) * h2 = i * k by Y2, X2, INT_1:def 9;
i * (((j gcd k) * g) * h2) = i * k by Y;
then ((j gcd k) * g) * h2 = k by A, XCMPLX_1:5;
hence (j gcd k) * g divides k by INT_1:def 9; :: thesis: verum

end;

then (j gcd k) * g divides j gcd k by INT_2:33;
then consider h3 being Integer such that
Z: ((j gcd k) * g) * h3 = j gcd k by INT_1:def 9;
(j gcd k) * (g * h3) = (j gcd k) * 1 by Z;
then g * h3 = 1 by B, XCMPLX_1:5;
then X3: g divides 1 by INT_1:def 9;

per cases ( g = 1 or g = - 1 ) by X3, INT_2:17;

suppose X4: g = 1 ; :: thesis: (i * j) gcd (i * k) = (abs i) * (j gcd k)

( i < 0 implies (j gcd k) * i < 0 * i ) by Y3, XREAL_1:71;
hence (i * j) gcd (i * k) = (abs i) * (j gcd k) by X4, X2, ABSVALUE:def 1; :: thesis: verum

end;

suppose g = - 1 ; :: thesis: (i * j) gcd (i * k) = (abs i) * (j gcd k)

then X4: (i * j) gcd (i * k) = (- i) * (j gcd k) by X2;

now

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

end;

hence (i * j) gcd (i * k) = (abs i) * (j gcd k) by X4, A, ABSVALUE:def 1; :: thesis: verum

end;

end;

end;

end;

end;

end;