let a, b be Integer; :: thesis: for n being Nat st n > 0 holds
(a * b) mod n = (a * (b mod n)) mod n
let n be Nat; :: thesis: ( n > 0 implies (a * b) mod n = (a * (b mod n)) mod n )
assume n > 0 ; :: thesis: (a * b) mod n = (a * (b mod n)) mod n
then (b mod n) + ((b div n) * n) = (b - ((b div n) * n)) + ((b div n) * n) by INT_1:def 8
.= b + 0 ;
then (a * b) - (a * (b mod n)) = (a * (b div n)) * n ;
then n divides (a * b) - (a * (b mod n)) by INT_1:def 9;
then a * b,a * (b mod n) are_congruent_mod n by INT_2:19;
hence (a * b) mod n = (a * (b mod n)) mod n by INT_3:12; :: thesis: verum