let a, b, c be Integer; :: thesis: ( c divides a * b & a,c are_coprime implies c divides b )
assume that
A1: c divides a * b and
A2: a,c are_coprime ; :: thesis: c divides b
c divides c * b ;
then A3: c divides (a * b) gcd (c * b) by A1, Def2;
A4: (a * b) gcd (c * b) = |.b.| by A2, Th24;
( 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 Th10; :: thesis: verum
end;
hence c divides b by A4, A3, ABSVALUE:def 1; :: thesis: verum