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