let a be Integer; :: thesis: ( 0 divides a iff a = 0 )
( 0 divides a implies a = 0 )

proof

assume 0 divides a ; :: thesis: a = 0
then ex b being Integer st a = 0 * b by INT_1:def 3;
hence a = 0 ; :: thesis: verum

end;

hence ( 0 divides a iff a = 0 ) ; :: thesis: verum