let t, z be Integer; :: thesis: t gcd z = (- t) gcd z
t gcd z = |.t.| gcd |.z.| by INT_2:34
.= |.(- t).| gcd |.z.| by COMPLEX1:52
.= (- t) gcd z by INT_2:34 ;
hence t gcd z = (- t) gcd z ; :: thesis: verum