1 = |.a.| gcd 2 by Def3
.= |.(- a).| gcd 2 by COMPLEX1:52 ;
hence - a is odd by INT_6:14; :: thesis: verum