let a, b, m, x be Integer; :: thesis: ( m <> 0 & a,m are_relative_prime & ((a * x) - b) mod m = 0 implies ex s being Integer st [x,(b * s)] in Cong m )
assume A1: ( m <> 0 & a,m are_relative_prime & ((a * x) - b) mod m = 0 ) ; :: thesis: ex s being Integer st [x,(b * s)] in Cong m
then a gcd m = 1 by INT_2:def 4;
then consider r, t being Integer such that
A2: 1 = (r * a) + (t * m) by INT_3:16;
((a * x) - b) mod m = 0 mod m by A1, Th12;
then (a * x) - b, 0 are_congruent_mod m by A1, INT_3:12;
then ((a * x) - b) * r,0 * r are_congruent_mod m by Th11;
then (x * (a * r)) - (b * r), 0 are_congruent_mod m ;
then A3: (x * (1 - (t * m))) - (b * r), 0 are_congruent_mod m by A2;
((x - ((x * t) * m)) - (b * r)) mod m = ((x - (b * r)) + (((- x) * t) * m)) mod m
.= (x - (b * r)) mod m by INT_3:8 ;
then (x - (b * r)) mod m = 0 mod m by A3, INT_3:12;
then 0 ,x - (b * r) are_congruent_mod m by A1, INT_3:12;
then A4: 0 + (b * r),x are_congruent_mod m by INT_1:40;
take s = r; :: thesis: [x,(b * s)] in Cong m
x,b * s are_congruent_mod m by A4, INT_1:35;
hence [x,(b * s)] in Cong m by Def1; :: thesis: verum