let x, y be Integer; ( ( 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 )
; 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; verum