let t be Integer; :: thesis: ( t is odd iff t gcd 2 = 1 )
thus ( t is odd implies t gcd 2 = 1 ) :: thesis: ( t gcd 2 = 1 implies t is odd )
proof
assume t is odd ; :: thesis: t gcd 2 = 1
then consider z being Integer such that
A1: t = (2 * z) + 1 by ABIAN:1;
t gcd 2 = 1 gcd (1 + (1 * 1)) by A1, NEWTON02:5
.= 1 ;
hence t gcd 2 = 1 ; :: thesis: verum
end;
( t gcd 2 <> |.2.| implies not 2 divides t ) by NEWTON02:3;
hence ( t gcd 2 = 1 implies t is odd ) ; :: thesis: verum