let x, y be Integer; :: thesis: ( ( x <> 0 or y <> 0 ) implies x div (x gcd y),y div (x gcd y) are_coprime )

assume A1: ( x <> 0 or y <> 0 ) ; :: thesis: x div (x gcd y),y div (x gcd y) are_coprime

then A2: x gcd y <> 0 by INT_2:5;

A3: y = (y div (x gcd y)) * (x gcd y) by Lm11, INT_2:21;

consider a, b being Integer such that

A4: x = (x gcd y) * a and

A5: ( y = (x gcd y) * b & a,b are_coprime ) by A1, INT_2:23;

x = (x div (x gcd y)) * (x gcd y) by Lm11, INT_2:21;

then a = x div (x gcd y) by A2, A4, XCMPLX_1:5;

hence x div (x gcd y),y div (x gcd y) are_coprime by A2, A3, A5, XCMPLX_1:5; :: thesis: verum

assume A1: ( x <> 0 or y <> 0 ) ; :: thesis: x div (x gcd y),y div (x gcd y) are_coprime

then A2: x gcd y <> 0 by INT_2:5;

A3: y = (y div (x gcd y)) * (x gcd y) by Lm11, INT_2:21;

consider a, b being Integer such that

A4: x = (x gcd y) * a and

A5: ( y = (x gcd y) * b & a,b are_coprime ) by A1, INT_2:23;

x = (x div (x gcd y)) * (x gcd y) by Lm11, INT_2:21;

then a = x div (x gcd y) by A2, A4, XCMPLX_1:5;

hence x div (x gcd y),y div (x gcd y) are_coprime by A2, A3, A5, XCMPLX_1:5; :: thesis: verum