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
reconsider a' = a, b' = b as Integer ;
A2: a',b' are_relative_prime by A1, INT_2:def 4;
let m be Nat; :: thesis: (a * m) gcd (b * m) = m
thus (a * m) gcd (b * m) = abs (abs m) by A2, INT_2:39
.= m by ABSVALUE:def 1 ; :: thesis: verum