let a, b, c be Integer; :: thesis: (a * b) mod (a * c) = a * (b mod c)

per cases ( a = 0 or a <> 0 ) ;

suppose a = 0 ; :: thesis: (a * b) mod (a * c) = a * (b mod c)

hence (a * b) mod (a * c) = a * (b mod c) ; :: thesis: verum

end;

suppose a <> 0 ; :: thesis: (a * b) mod (a * c) = a * (b mod c)

then reconsider a = a as non zero Integer ;

per cases ( c = 0 or c <> 0 ) ;

suppose c = 0 ; :: thesis: (a * b) mod (a * c) = a * (b mod c)

then ( (a * b) mod (a * c) = 0 & b mod c = 0 ) ;
hence (a * b) mod (a * c) = a * (b mod c) ; :: thesis: verum

end;

suppose c <> 0 ; :: thesis: (a * b) mod (a * c) = a * (b mod c)

then reconsider c = c as non zero Integer ;
(a * b) mod (a * c) = (a * b) - (((a * b) div (a * c)) * (a * c)) by INT_1:def 10
.= (a * b) - ([\((a * b) / (a * c))/] * (a * c)) by INT_1:def 9
.= a * (b - ([\((a * b) / (a * c))/] * c))
.= a * (b - ([\(b / c)/] * c)) by XCMPLX_1:91
.= a * (b - ((b div c) * c)) by INT_1:def 9 ;
hence (a * b) mod (a * c) = a * (b mod c) by INT_1:def 10; :: thesis: verum

end;

end;

end;

end;