let a, b, m, x be Integer; ( 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
; 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; [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; verum