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

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