let a, b, m be Integer; :: thesis: ( m <> 0 & not a gcd m divides b implies for x being Integer holds not ((a * x) - b) mod m = 0 )

assume that

A1: m <> 0 and

A2: not a gcd m divides b ; :: thesis: for x being Integer holds not ((a * x) - b) mod m = 0

given y being Integer such that A3: ((a * y) - b) mod m = 0 ; :: thesis: contradiction

a gcd m divides m by INT_2:21;

then A4: ex i being Integer st m = (a gcd m) * i ;

((a * y) - b) mod m = 0 mod m by A3, Th12;

then (a * y) - b, 0 are_congruent_mod m by A1, NAT_D:64;

then (a * y) - b, 0 are_congruent_mod a gcd m by A4, INT_1:20;

then A5: a gcd m divides ((a * y) - b) - 0 ;

a gcd m divides a * y by INT_2:2, INT_2:21;

hence contradiction by A2, A5, Lm5; :: thesis: verum

assume that

A1: m <> 0 and

A2: not a gcd m divides b ; :: thesis: for x being Integer holds not ((a * x) - b) mod m = 0

given y being Integer such that A3: ((a * y) - b) mod m = 0 ; :: thesis: contradiction

a gcd m divides m by INT_2:21;

then A4: ex i being Integer st m = (a gcd m) * i ;

((a * y) - b) mod m = 0 mod m by A3, Th12;

then (a * y) - b, 0 are_congruent_mod m by A1, NAT_D:64;

then (a * y) - b, 0 are_congruent_mod a gcd m by A4, INT_1:20;

then A5: a gcd m divides ((a * y) - b) - 0 ;

a gcd m divides a * y by INT_2:2, INT_2:21;

hence contradiction by A2, A5, Lm5; :: thesis: verum