let x, y be Integer; :: thesis: ( ( x divides y implies y mod x = 0 ) & ( x <> 0 & y mod x = 0 implies x divides y ) )
thus ( x divides y implies y mod x = 0 ) :: thesis: ( x <> 0 & y mod x = 0 implies x divides y )

proof

assume x divides y ; :: thesis: y mod x = 0
then consider i being Integer such that
A1: y = x * i ;
y mod x = ((x * i) + 0) mod x by A1
.= 0 mod x by NAT_D:61
.= 0 by INT_1:73 ;
hence y mod x = 0 ; :: thesis: verum

end;

assume that
A2: x <> 0 and
A3: y mod x = 0 ; :: thesis: x divides y
y = ((y div x) * x) + (y mod x) by A2, INT_1:59
.= (y div x) * x by A3 ;
hence x divides y ; :: thesis: verum