let a, b, m be Integer; :: thesis: ( m > 0 & a,m are_coprime implies ex n being Nat st ((a * n) - b) mod m = 0 )

assume that

A1: m > 0 and

A2: a,m are_coprime ; :: thesis: ex n being Nat st ((a * n) - b) mod m = 0

consider x being Integer such that

A3: ((a * x) - b) mod m = 0 by A2, Th15;

consider q, n being Integer such that

A4: x = (m * q) + n and

A5: n >= 0 and

n < m by A1, Th13;

A6: ((a * x) - b) mod m = (((a * q) * m) + ((a * n) - b)) mod m by A4

.= ((a * n) - b) mod m by EULER_1:12 ;

n in NAT by A5, INT_1:3;

then reconsider n = n as Nat ;

take n ; :: thesis: ((a * n) - b) mod m = 0

thus ((a * n) - b) mod m = 0 by A3, A6; :: thesis: verum

assume that

A1: m > 0 and

A2: a,m are_coprime ; :: thesis: ex n being Nat st ((a * n) - b) mod m = 0

consider x being Integer such that

A3: ((a * x) - b) mod m = 0 by A2, Th15;

consider q, n being Integer such that

A4: x = (m * q) + n and

A5: n >= 0 and

n < m by A1, Th13;

A6: ((a * x) - b) mod m = (((a * q) * m) + ((a * n) - b)) mod m by A4

.= ((a * n) - b) mod m by EULER_1:12 ;

n in NAT by A5, INT_1:3;

then reconsider n = n as Nat ;

take n ; :: thesis: ((a * n) - b) mod m = 0

thus ((a * n) - b) mod m = 0 by A3, A6; :: thesis: verum