let n be Integer; :: thesis: ( n is even iff n mod 2 = 0 )
thus ( n is even implies n mod 2 = 0 ) :: thesis: ( n mod 2 = 0 implies n is even )

proof

assume n is even ; :: thesis: n mod 2 = 0
then ex k being Integer st n = 2 * k by ABIAN:11;
hence n mod 2 = 0 by NAT_D:71; :: thesis: verum

end;

assume A2: n mod 2 = 0 ; :: thesis: n is even
assume n is odd ; :: thesis: contradiction
then consider k being Integer such that
A3: n = (2 * k) + 1 by ABIAN:1;
A4: (2 * k) mod 2 = 0 by NAT_D:71;
((2 * k) + 1) mod 2 = (((2 * k) mod 2) + (1 mod 2)) mod 2 by NAT_D:66
.= 1 by A4, A5 ;
hence contradiction by A2, A3; :: thesis: verum