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

proof

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

end;

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