let m, b, n, a be Nat; :: thesis: ( m > 1 & b <> 0 & m,n are_relative_prime & a,m are_relative_prime & n = (a * b) mod m implies m,b are_relative_prime )
assume A1: ( m > 1 & b <> 0 & m,n are_relative_prime & a,m are_relative_prime & n = (a * b) mod m ) ; :: thesis: m,b are_relative_prime
assume not m,b are_relative_prime ; :: thesis: contradiction
then A2: m gcd b <> 1 by INT_2:def 4;
set k = m gcd b;
A3: ( m gcd b divides m & m gcd b divides b ) 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;
consider kb being Nat such that
A6: b = (m gcd b) * kb by A3, 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)) & (a * ((m gcd b) * kb)) mod ((m gcd b) * km) < (m gcd b) * km ) by A1, A4, NAT_D:def 2;
A8: (a * ((m gcd b) * kb)) mod ((m gcd b) * km) = (m gcd b) * ((a * kb) - (km * p)) by A7;
set tm = (a * kb) - (km * p);
A9: ( (a * kb) - (km * p) = 0 implies m gcd n <> 1 ) by A1, A4, A6, A8, NEWTON:65;
A10: m gcd b <> - 1 by NAT_1:2;
( (a * kb) - (km * p) <> 0 implies m gcd n <> 1 )

proof

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

end;

hence contradiction by A1, A9, INT_2:def 4; :: thesis: verum