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

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;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

now :: thesis: ( c = 0 implies a divides b mod c )

hence
a divides b mod c
by A3; :: thesis: verumassume
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;then b mod c = 0 by INT_1:def 10;

hence a divides b mod c by Lm5; :: thesis: verum