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