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

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