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