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 ;
:: 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 ;
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 ;
i * (j gcd k) divides i * j by ;
then i * (j gcd k) divides (i * j) gcd (i * k) by ;
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 ;
i * (((j gcd k) * g) * h1) = i * j by A10;
then ((j gcd k) * g) * h1 = j by ;
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 ;
i * (((j gcd k) * g) * h2) = i * k by A11;
then ((j gcd k) * g) * h2 = k by ;
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 ;
then A13: g divides 1 by INT_1:def 3;
per cases ( g = 1 or g = - 1 ) by ;
suppose A14: g = 1 ; :: thesis: (i * j) gcd (i * k) = |.i.| * (j gcd k)
( i < 0 implies (j gcd k) * i < 0 * i ) by ;
hence (i * j) gcd (i * k) = |.i.| * (j gcd k) by ; :: 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 ; :: thesis: verum
end;
(i * j) gcd (i * k) = (- i) * (j gcd k) by ;
hence (i * j) gcd (i * k) = |.i.| * (j gcd k) by ; :: thesis: verum
end;
end;
end;
end;
end;
end;