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

proof

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

end;

( x <> 0 & y mod x = 0 implies x divides y )

proof

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

end;

hence ( ( x divides y implies y mod x = 0 ) & ( x <> 0 & y mod x = 0 implies x divides y ) ) by A1; :: thesis: verum