let a, b, m, x be Integer; :: thesis: ( m <> 0 & a,m are_coprime & ((a * x) - b) mod m = 0 implies ex s being Integer st [x,(b * s)] in Cong m )
assume that
A1: m <> 0 and
A2: a,m are_coprime and
A3: ((a * x) - b) mod m = 0 ; :: thesis: ex s being Integer st [x,(b * s)] in Cong m
a gcd m = 1 by A2, INT_2:def 3;
then consider r, t being Integer such that
A4: 1 = (r * a) + (t * m) by NAT_D:68;
((a * x) - b) mod m = 0 mod m by A3, Th12;
then (a * x) - b, 0 are_congruent_mod m by A1, NAT_D:64;
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 A5: (x * (1 - (t * m))) - (b * r), 0 are_congruent_mod m by A4;
take s = r; :: thesis: [x,(b * s)] in Cong m
((x - ((x * t) * m)) - (b * r)) mod m = ((x - (b * r)) + (((- x) * t) * m)) mod m
.= (x - (b * r)) mod m by NAT_D:61 ;
then (x - (b * r)) mod m = 0 mod m by A5, NAT_D:64;
then 0 ,x - (b * r) are_congruent_mod m by A1, NAT_D:64;
then 0 + (b * r),x are_congruent_mod m ;
then x,b * s are_congruent_mod m by INT_1:14;
hence [x,(b * s)] in Cong m by Def1; :: thesis: verum