let a, n, k be Nat; :: thesis: ( a divides k * ((a * n) + 1) iff a divides k )
( a divides k * ((a * n) + 1) implies a divides k )

proof

assume a divides k * ((a * n) + 1) ; :: thesis: a divides k
then A1: a divides ((k * a) * n) + (k * 1) ;
a divides a * (k * n) ;
hence a divides k by A1, INT_2:1; :: thesis: verum

end;

hence ( a divides k * ((a * n) + 1) iff a divides k ) by INT_2:2; :: thesis: verum