let c, a, b be Nat; :: 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
A3: c divides c * b by NAT_D:9;
a gcd c = 1 by A2, INT_2:def 3;
then (a * b) gcd (c * b) = b by Th6;
hence c divides b by A1, A3, NEWTON:50; :: thesis: verum