let j, k, l be Nat; :: thesis: ( 0 < l & l < j implies not j divides (j * k) + l )
set i = (j * k) + l;
assume that
A3: 0 < l and
A2: l < j ; :: thesis: not j divides (j * k) + l
assume j divides (j * k) + l ; :: thesis: contradiction
then (j * k) + l = j * (((j * k) + l) div j) by NAT_D:3;
then j * (((j * k) + l) div j) = (j * (((j * k) + l) div j)) + l by A2, NAT_D:def 1;
hence contradiction by A3; :: thesis: verum