let a, b, m, n be Nat; ( m > 1 & m,n are_coprime & n = (a * b) mod m implies m,b are_coprime )
assume that
A1:
m > 1
and
A2:
m,n are_coprime
and
A3:
n = (a * b) mod m
; m,b are_coprime
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 12;
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_coprime
; contradiction
then A9:
m gcd b <> 1
by INT_2:def 3;
A10:
m gcd b <> - 1
by NAT_1:2;
A11:
( (a * kb) - (km * p) <> 0 implies m gcd n <> 1 )
( (a * kb) - (km * p) = 0 implies m gcd n <> 1 )
by A1, A3, A4, A6, A8, NEWTON:52;
hence
contradiction
by A2, A11, INT_2:def 3; verum