let a, b be Nat; :: thesis: ( a gcd b = 1 implies for c being Nat holds (a * c) gcd (b * c) = c )
assume A1: a gcd b = 1 ; :: thesis: for c being Nat holds (a * c) gcd (b * c) = c
let m be Nat; :: thesis: (a * m) gcd (b * m) = m
reconsider a' = a, b' = b as Integer ;
a',b' are_relative_prime by A1, INT_2:def 4;
hence (a * m) gcd (b * m) = abs (abs m) by INT_2:39
.= m by ABSVALUE:def 1 ;
:: thesis: verum