let m be Integer; :: thesis: ( 0 gcd m = abs m & 1 gcd m = 1 )
A1: m gcd 1 = (abs m) gcd (abs 1) by INT_2:34
.= (abs m) gcd 1 by ABSVALUE:def 1
.= 1 by NEWTON:51 ;
m gcd 0 = (abs m) gcd (abs 0) by INT_2:34
.= (abs m) gcd 0 by ABSVALUE:2
.= abs m by NEWTON:52 ;
hence ( 0 gcd m = abs m & 1 gcd m = 1 ) by A1; :: thesis: verum