let a, b, c be Nat; :: thesis: ( a <> 0 & c <> 0 & (a * c) gcd (b * c) = c implies a,b are_coprime )
assume that
A1: a <> 0 and
A2: c <> 0 and
A3: (a * c) gcd (b * c) = c ; :: thesis: a,b are_coprime
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_coprime ) by INT_2:23;
a = a1 by A2, A3, A4, XCMPLX_1:5;
hence a,b are_coprime by A2, A3, A5, XCMPLX_1:5; :: thesis: verum