let i1, i2, i3 be Integer; :: thesis: ( i3 <> 0 implies ( i1 divides i2 iff i1 * i3 divides i2 * i3 ) )
assume A1: i3 <> 0 ; :: thesis: ( i1 divides i2 iff i1 * i3 divides i2 * i3 )
thus ( i1 divides i2 implies i1 * i3 divides i2 * i3 ) :: thesis: ( i1 * i3 divides i2 * i3 implies i1 divides i2 )

proof

assume i1 divides i2 ; :: thesis: i1 * i3 divides i2 * i3
then consider i4 being Integer such that
A2: i2 = i1 * i4 ;
i2 * i3 = (i1 * i3) * i4 by A2;
hence i1 * i3 divides i2 * i3 ; :: thesis: verum

end;

assume i1 * i3 divides i2 * i3 ; :: thesis: i1 divides i2
then consider i5 being Integer such that
A3: i2 * i3 = (i1 * i3) * i5 ;
i2 * i3 = (i1 * i5) * i3 by A3;
then i2 = i1 * i5 by A1, XCMPLX_1:5;
hence i1 divides i2 ; :: thesis: verum