let c, a, b be Integer; :: thesis: ( c divides a * b & a,c are_relative_prime implies c divides b )
assume that
A1: c divides a * b and
A2: a,c are_relative_prime ; :: thesis: c divides b
c divides c * b by Th12;
then A3: c divides (a * b) gcd (c * b) by A1, Def3;
A4: (a * b) gcd (c * b) = abs b by A2, Th39;
( b < 0 implies c divides b )

proof

assume b < 0 ; :: thesis: c divides b
then c divides - b by A4, A3, ABSVALUE:def 1;
hence c divides b by Th14; :: thesis: verum

end;

hence c divides b by A4, A3, ABSVALUE:def 1; :: thesis: verum