let n be Nat; :: thesis: ( n is even iff n mod 2 = 0 )
A1: n in NAT by ORDINAL1:def 13;
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 consider k being Element of NAT such that
A2: n = 2 * k by A1, ABIAN:def 2;
n = (2 * k) + 0 by A2;
hence n mod 2 = 0 by NAT_D:def 2; :: thesis: verum

end;

assume n mod 2 = 0 ; :: thesis: n is even
then ex k being Nat st
( n = (2 * k) + 0 & 0 < 2 ) by NAT_D:def 2;
hence n is even ; :: thesis: verum