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

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