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