let i, j be natural Number ; :: thesis: ( j divides i iff i = j * (i div j) )
thus ( j divides i implies i = j * (i div j) ) :: thesis: ( i = j * (i div j) implies j divides i )

proof

assume j divides i ; :: thesis: i = j * (i div j)
then consider k being Nat such that
A1: i = j * k ;
A2: i = (j * k) + 0 by A1;

now :: thesis: ( j <> 0 implies i = j * (i div j) )

assume A3: j <> 0 ; :: thesis: i = j * (i div j)
then A4: i = (j * (i div j)) + (i mod j) by INT_1:59;
i mod j < j by A3, Th1;
hence i = j * (i div j) by A2, A4, NAT_1:18; :: thesis: verum

end;

hence i = j * (i div j) by A1; :: thesis: verum

end;

thus ( i = j * (i div j) implies j divides i ) ; :: thesis: verum