let z be Integer; :: thesis: 1 gcd z = 1
thus 1 gcd z = (abs 1) gcd (abs z) by INT_2:34
.= 1 gcd (abs z) by ABSVALUE:def 1
.= 1 by NEWTON:51 ; :: thesis: verum