let k, l be Integer; :: thesis: ( k <> 0 implies ( k divides l iff l / k is Integer ) )
assume A1: k <> 0 ; :: thesis: ( k divides l iff l / k is Integer )
hence ( k divides l implies l / k is Integer ) by XCMPLX_1:89; :: thesis: ( l / k is Integer implies k divides l )
assume l / k is Integer ; :: thesis: k divides l
then reconsider m = l / k as Integer ;
l = k * m by A1, XCMPLX_1:87;
hence k divides l ; :: thesis: verum