let i, j be Integer; :: thesis: ( j <> 0 & i mod j = 0 implies i div j = i / j )
assume that
A1: j <> 0 and
A2: i mod j = 0 ; :: thesis: i div j = i / j
i = ((i div j) * j) + (i mod j) by A1, INT_1:59
.= (i div j) * j by A2 ;
hence i div j = i / j by A1, XCMPLX_1:89; :: thesis: verum