let m, n, a, b be Nat; :: thesis: ( m > 1 & m,n are_relative_prime & n = (a * b) mod m implies m,b are_relative_prime )
assume that
A1: m > 1 and
A2: m,n are_relative_prime and
A3: n = (a * b) mod m ; :: thesis: m,b are_relative_prime
set k = m gcd b;
m gcd b divides m by NAT_D:def 5;
then consider km being Nat such that
A4: m = (m gcd b) * km by NAT_D:def 3;
A5: ( m gcd b <> 0 & km <> 0 ) by A1, A4;
reconsider km = km as Element of NAT by ORDINAL1:def 13;
m gcd b divides b by NAT_D:def 5;
then consider kb being Nat such that
A6: b = (m gcd b) * kb by NAT_D:def 3;
consider p being Nat such that
A7: a * ((m gcd b) * kb) = (((m gcd b) * km) * p) + ((a * ((m gcd b) * kb)) mod ((m gcd b) * km)) and
(a * ((m gcd b) * kb)) mod ((m gcd b) * km) < (m gcd b) * km by A1, A4, NAT_D:def 2;
set tm = (a * kb) - (km * p);
A8: (a * ((m gcd b) * kb)) mod ((m gcd b) * km) = (m gcd b) * ((a * kb) - (km * p)) by A7;
assume not m,b are_relative_prime ; :: thesis: contradiction
then A9: m gcd b <> 1 by INT_2:def 4;
A10: m gcd b <> - 1 by NAT_1:2;
A11: ( (a * kb) - (km * p) <> 0 implies m gcd n <> 1 )

proof

assume (a * kb) - (km * p) <> 0 ; :: thesis: m gcd n <> 1
m gcd n = (m gcd b) * (km gcd ((a * kb) - (km * p))) by A3, A4, A5, A6, A8, EULER_1:16;
hence m gcd n <> 1 by A9, A10, INT_1:22; :: thesis: verum

end;

( (a * kb) - (km * p) = 0 implies m gcd n <> 1 ) by A1, A3, A4, A6, A8, NEWTON:65;
hence contradiction by A2, A11, INT_2:def 4; :: thesis: verum