let a, b be Nat; :: thesis: for c being non zero Nat st (a mod c) * (b mod c) >= c holds
a mod c > 1
let c be non zero Nat; :: thesis: ( (a mod c) * (b mod c) >= c implies a mod c > 1 )
assume A1: (a mod c) * (b mod c) >= c ; :: thesis: a mod c > 1
( a mod c > 1 or (a mod c) * (b mod c) <= 1 * (b mod c) ) by XREAL_1:64;
then ( a mod c > 1 or b mod c >= c ) by A1, XXREAL_0:2;
hence a mod c > 1 by INT_1:58; :: thesis: verum