let t, z be Integer; :: thesis: ( t gcd z is even iff ( t is even & z is even ) )
( t gcd z is even implies ( t is even & z is even ) )

proof

assume A1: t gcd z is even ; :: thesis: ( t is even & z is even )
( t gcd z divides t & t gcd z divides z ) by INT_2:21;
hence ( t is even & z is even ) by A1; :: thesis: verum

end;

hence ( t gcd z is even iff ( t is even & z is even ) ) by INT_2:def 2; :: thesis: verum