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 ) )

( t gcd z is even implies ( t is even & z is even ) )

proof

hence
( t gcd z is even iff ( t is even & z is even ) )
by INT_2:def 2; :: thesis: verum
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;( 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