let x, y, i be Integer; :: thesis: ( x <> 0 & y <> 0 & i > 0 implies (i * x) gcd (i * y) = i * (x gcd y) )
assume A1: ( x <> 0 & y <> 0 & i > 0 ) ; :: thesis: (i * x) gcd (i * y) = i * (x gcd y)
then consider a2, b2 being Integer such that
A2: x = (x gcd y) * a2 and
A3: y = (x gcd y) * b2 and
A4: a2,b2 are_relative_prime by INT_2:38;
A5: i * x = (i * (x gcd y)) * a2 by A2;
i * y = (i * (x gcd y)) * b2 by A3;
then A6: (i * x) gcd (i * y) = abs (i * (x gcd y)) by A4, A5, INT_2:39
.= (abs i) * (abs (x gcd y)) by COMPLEX1:151 ;
i = abs i by A1, ABSVALUE:def 1;
hence (i * x) gcd (i * y) = i * (x gcd y) by A6, ABSVALUE:def 1; :: thesis: verum