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

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