let a be Integer; :: thesis: for b being non zero Integer
for c being non zero Nat holds a mod (b * c) = (a mod b) + (b * ((a div b) mod c))
let b be non zero Integer; :: thesis: for c being non zero Nat holds a mod (b * c) = (a mod b) + (b * ((a div b) mod c))
let c be non zero Nat; :: thesis: a mod (b * c) = (a mod b) + (b * ((a div b) mod c))
A1: ( a div b = ((a div b) mod c) + (c * ((a div b) div c)) & (a mod (b * c)) + ((b * c) * (a div (b * c))) = a & a = (a mod b) + (b * (a div b)) ) by INT_1:59;
then a mod (b * c) = (a mod b) + (b * ((a div b) - (c * (a div (b * c)))))
.= (a mod b) + (b * ((a div b) - (c * ((a div b) div c)))) by NAT227
.= (a mod b) + (b * ((a div b) mod c)) by A1 ;
hence a mod (b * c) = (a mod b) + (b * ((a div b) mod c)) ; :: thesis: verum