let a, b, c be Element of NAT ; :: thesis: ( 0 < a & 0 < b & a < c & b < c & c is prime implies (a * b) mod c <> 0 )
assume A1: ( 0 < a & 0 < b & a < c & b < c & c is prime ) ; :: thesis: (a * b) mod c <> 0
assume (a * b) mod c = 0 ; :: thesis: contradiction
then a * b = (c * ((a * b) div c)) + 0 by A1, NAT_D:2;
then c divides a * b by NAT_D:def 3;
then ( c divides a or c divides b ) by A1, NEWTON:98;
hence contradiction by A1, NAT_D:7; :: thesis: verum