let i, n be Nat; :: thesis: ( i <> 0 implies ( i divides n iff n mod i = 0 ) )
assume A1: i <> 0 ; :: thesis: ( i divides n iff n mod i = 0 )
A2: ( n mod i = 0 implies i divides n )

proof

assume n mod i = 0 ; :: thesis: i divides n
then ex t being Nat st
( n = (i * t) + 0 & 0 < i ) by A1, NAT_D:def 2;
hence i divides n ; :: thesis: verum

end;

( i divides n implies n mod i = 0 )

proof

assume i divides n ; :: thesis: n mod i = 0
then ex t being Nat st n = i * t by NAT_D:def 3;
hence n mod i = 0 by NAT_D:13; :: thesis: verum

end;

hence ( i divides n iff n mod i = 0 ) by A2; :: thesis: verum