let a, b be Nat; :: thesis: for c being non zero Nat holds
( (a mod c) * (b mod c) < c iff (a * b) mod c = (a mod c) * (b mod c) )
let c be non zero Nat; :: thesis: ( (a mod c) * (b mod c) < c iff (a * b) mod c = (a mod c) * (b mod c) )
( (a mod c) * (b mod c) < c implies (a * b) mod c = (a mod c) * (b mod c) )

proof

assume (a mod c) * (b mod c) < c ; :: thesis: (a * b) mod c = (a mod c) * (b mod c)
then ((a mod c) * (b mod c)) mod c = (a mod c) * (b mod c) by NAT_D:24;
hence (a * b) mod c = (a mod c) * (b mod c) by NAT_D:67; :: thesis: verum

end;

hence ( (a mod c) * (b mod c) < c iff (a * b) mod c = (a mod c) * (b mod c) ) by INT_1:58; :: thesis: verum