let a, b, m, x be Integer; ( m <> 0 & ((a * x) - b) mod m = 0 implies for y being Integer holds
( ( a,m are_coprime & ((a * y) - b) mod m = 0 implies y in Class ((Cong m),x) ) & ( y in Class ((Cong m),x) implies ((a * y) - b) mod m = 0 ) ) )
assume that
A1:
m <> 0
and
A2:
((a * x) - b) mod m = 0
; for y being Integer holds
( ( a,m are_coprime & ((a * y) - b) mod m = 0 implies y in Class ((Cong m),x) ) & ( y in Class ((Cong m),x) implies ((a * y) - b) mod m = 0 ) )
let y be Integer; ( ( a,m are_coprime & ((a * y) - b) mod m = 0 implies y in Class ((Cong m),x) ) & ( y in Class ((Cong m),x) implies ((a * y) - b) mod m = 0 ) )
hereby ( y in Class ((Cong m),x) implies ((a * y) - b) mod m = 0 )
assume that A3:
a,
m are_coprime
and A4:
((a * y) - b) mod m = 0
;
y in Class ((Cong m),x)
(a * x) - b,
(a * y) - b are_congruent_mod m
by A1, A2, A4, NAT_D:64;
then
((a * x) - b) + b,
a * y are_congruent_mod m
;
then
x,
y are_congruent_mod m
by A3, Th9;
then
[x,y] in Cong m
by Def1;
hence
y in Class (
(Cong m),
x)
by EQREL_1:18;
verum
end;
assume
y in Class ((Cong m),x)
; ((a * y) - b) mod m = 0
then
[x,y] in Cong m
by EQREL_1:18;
then
x,y are_congruent_mod m
by Def1;
then A5:
x * a,y * a are_congruent_mod m
by Th11;
((a * x) - b) mod m = 0 mod m
by A2, Th12;
then
0 ,(a * x) - b are_congruent_mod m
by A1, NAT_D:64;
then
0 + b,a * x are_congruent_mod m
;
then
0 + b,a * y are_congruent_mod m
by A5, INT_1:15;
then
0 ,(a * y) - b are_congruent_mod m
;
then
((a * y) - b) mod m = 0 mod m
by NAT_D:64;
hence
((a * y) - b) mod m = 0
by Th12; verum