let a, b be Integer; :: thesis: for n being Nat holds (a * b) mod n = (a * (b mod n)) mod n

let n be Nat; :: thesis: (a * b) mod n = (a * (b mod n)) mod n

let n be Nat; :: thesis: (a * b) mod n = (a * (b mod n)) mod n

per cases
( n > 0 or n = 0 )
;

end;

suppose
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 10

.= 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 3;

then a * b,a * (b mod n) are_congruent_mod n by INT_2:15;

hence (a * b) mod n = (a * (b mod n)) mod n by NAT_D:64; :: thesis: verum

end;.= 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 3;

then a * b,a * (b mod n) are_congruent_mod n by INT_2:15;

hence (a * b) mod n = (a * (b mod n)) mod n by NAT_D:64; :: thesis: verum