let i, j, k be Integer; :: thesis: ( i,j are_relative_prime implies i gcd (j * k) = i gcd k )
assume A1: i gcd j = 1 ; :: according to INT_2:def 4 :: thesis: i gcd (j * k) = i gcd k
(i * k) gcd (j * k) = (abs k) * (i gcd j) by Th16;
then i gcd (abs k) = (i gcd (i * k)) gcd (j * k) by A1, Th18
.= (abs i) gcd (j * k) by Th17
.= (j * k) gcd i by Th14 ;
hence i gcd (j * k) = i gcd k by Th14; :: thesis: verum