let a, b, m be Integer; :: thesis: ( a,m are_coprime implies ex x being Integer st ((a * x) - b) mod m = 0 )
assume a,m are_coprime ; :: thesis: ex x being Integer st ((a * x) - b) mod m = 0
then a gcd m = 1 by INT_2:def 3;
then consider s, t being Integer such that
A1: 1 = (s * a) + (t * m) by NAT_D:68;
take b * s ; :: thesis: ((a * (b * s)) - b) mod m = 0
(((a * b) * s) - b) mod m = (((a * s) - 1) * b) mod m
.= ((- (m * t)) * b) mod m by A1
.= (0 + (m * ((- t) * b))) mod m
.= 0 mod m by NAT_D:61
.= 0 by Th12 ;
hence ((a * (b * s)) - b) mod m = 0 ; :: thesis: verum