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 by INT_1:def 9;
y mod x = ((x * i) + 0 ) mod x by A2
.= 0 mod x by EULER_1:13
.= 0 by Th12 ;
hence y mod x = 0 ; :: thesis: verum

end;

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

proof

assume A3: ( x <> 0 & y mod x = 0 ) ; :: thesis: x divides y
then y = ((y div x) * x) + (y mod x) by INT_1:86
.= (y div x) * x by A3 ;
hence x divides y by INT_1:def 9; :: 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