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