let h, i, j be natural Number ; :: thesis: ( i divides j & i divides h implies i divides j mod h )
assume that
A1: i divides j and
A2: i divides h ; :: thesis: i divides j mod h
A3: now :: thesis: ( h = 0 implies i divides j mod h )
assume h = 0 ; :: thesis: i divides j mod h
then j mod h = 0 by Def2;
hence i divides j mod h by Th6; :: thesis: verum
end;
now :: thesis: ( h <> 0 implies i divides j mod h )
assume h <> 0 ; :: thesis: i divides j mod h
then A4: j = (h * (j div h)) + (j mod h) by INT_1:59;
i divides h * (j div h) by A2, Th9;
hence i divides j mod h by A1, A4, Th10; :: thesis: verum
end;
hence i divides j mod h by A3; :: thesis: verum