let a, b, m be Integer; :: thesis: ( m <> 0 & a gcd m divides b implies ex x being Integer st ((a * x) - b) mod m = 0 )
assume that
A1: m <> 0 and
A2: a gcd m divides b ; :: thesis: ex x being Integer st ((a * x) - b) mod m = 0
consider a1, m1 being Integer such that
A3: a = (a gcd m) * a1 and
A4: m = (a gcd m) * m1 and
A5: a1,m1 are_coprime by A1, INT_2:23;
consider b1 being Integer such that
A6: b = (a gcd m) * b1 by A2;
A7: m1 <> 0 by A1, A4;
consider y being Integer such that
A8: ((a1 * y) - b1) mod m1 = 0 by A5, Th15;
take y ; :: thesis: ((a * y) - b) mod m = 0
((a1 * y) - b1) mod m1 = 0 mod m1 by A8, Th12;
then (a1 * y) - b1, 0 are_congruent_mod m1 by A7, NAT_D:64;
then ((a1 * y) - b1) * (a gcd m),(a gcd m) * 0 are_congruent_mod m1 * (a gcd m) by Th10;
then ((a * y) - b) mod m = 0 mod m by A3, A4, A6, NAT_D:64;
hence ((a * y) - b) mod m = 0 by Th12; :: thesis: verum