let i, x, y be Integer; :: thesis: ( x <> 0 & i >= 0 implies (i * x) gcd (i * y) = i * (x gcd y) )
assume that
A1: x <> 0 and
A2: i >= 0 ; :: thesis: (i * x) gcd (i * y) = i * (x gcd y)
consider a2, b2 being Integer such that
A3: ( x = (x gcd y) * a2 & y = (x gcd y) * b2 ) and
A4: a2,b2 are_coprime by A1, INT_2:23;
( i * x = (i * (x gcd y)) * a2 & i * y = (i * (x gcd y)) * b2 ) by A3;
then A5: (i * x) gcd (i * y) = |.(i * (x gcd y)).| by A4, INT_2:24
.= |.i.| * |.(x gcd y).| by COMPLEX1:65 ;
i = |.i.| by A2, ABSVALUE:def 1;
hence (i * x) gcd (i * y) = i * (x gcd y) by A5, ABSVALUE:def 1; :: thesis: verum