let a, b, c be Nat; :: thesis: ( 0 < a & 0 < b & a < c & b < c & c is prime implies (a * b) mod c <> 0 )
assume that
A1: ( 0 < a & 0 < b ) and
A2: a < c and
A3: b < c and
A4: 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 A2, NAT_D:2;
then c divides a * b by NAT_D:def 3;
then ( c divides a or c divides b ) by A4, NEWTON:80;
hence contradiction by A1, A2, A3, NAT_D:7; :: thesis: verum