let a, c, b be Nat; :: thesis: ( a <> 0 & c <> 0 & (a * c) gcd (b * c) = c implies a,b are_relative_prime )
assume that
A1: a <> 0 and
A2: c <> 0 and
A3: (a * c) gcd (b * c) = c ; :: thesis: a,b are_relative_prime
a * c <> 0 * c by A1, A2, XCMPLX_1:5;
then consider a1, b1 being Integer such that
A4: a * c = ((a * c) gcd (b * c)) * a1 and
A5: ( b * c = ((a * c) gcd (b * c)) * b1 & a1,b1 are_relative_prime ) by INT_2:38;
a = a1 by A2, A3, A4, XCMPLX_1:5;
hence a,b are_relative_prime by A2, A3, A5, XCMPLX_1:5; :: thesis: verum