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 a9 = a, b9 = b as Integer ;
a9,b9 are_coprime by A1, INT_2:def 3;
hence (a * m) gcd (b * m) = |.|.m.|.| by INT_2:24
.= m by ABSVALUE:def 1 ;
:: thesis: verum