let k, m, n be Integer; :: thesis: ( m divides n * k & m gcd n = 1 implies m divides k )
assume that
A1: m divides n * k and
A2: m gcd n = 1 ; :: thesis: m divides k
consider m1, n1 being Integer such that
A3: (m * m1) + (n * n1) = 1 by A2, Th28;
k = ((m * m1) + (n * n1)) * k by A3
.= (m * (m1 * k)) + ((n * k) * n1) ;
hence m divides k by A1, Th5; :: thesis: verum