let a, b, c be Integer; :: thesis: ( a divides b & a divides c implies a divides b mod c )
assume that
A1: a divides b and
A2: a divides c ; :: thesis: a divides b mod c
A3: now :: thesis: ( c <> 0 implies a divides b mod c )
assume c <> 0 ; :: thesis: a divides b mod c
then A4: b = (c * (b div c)) + (b mod c) by INT_1:59;
a divides c * (b div c) by A2, Th2;
hence a divides b mod c by A1, A4, Th1; :: thesis: verum
end;
now :: thesis: ( c = 0 implies a divides b mod c )
assume c = 0 ; :: thesis: a divides b mod c
then b mod c = 0 by INT_1:def 10;
hence a divides b mod c by Lm5; :: thesis: verum
end;
hence a divides b mod c by A3; :: thesis: verum