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

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