let a, b, c be Nat; :: thesis: ( c <> 0 & c < b implies not ((a * b) + c) / b is integer )
assume that
A1: c <> 0 and
A2: c < b ; :: thesis: not ((a * b) + c) / b is integer
A3: ((a * b) + c) mod b = c mod b by NAT_D:21;
c mod b = c by A2, NAT_D:24;
then not b divides (a * b) + c by A1, A2, A3, INT_1:62;
hence not ((a * b) + c) / b is integer by A2, WSIERP_1:17; :: thesis: verum