let a, m, n be Nat; :: thesis: ( a <> 0 & m > 1 & n <> 0 & (a * n) mod m = n mod m & m,n are_relative_prime implies a mod m = 1 )
assume A1: ( a <> 0 & m > 1 & n <> 0 & (a * n) mod m = n mod m & m,n are_relative_prime ) ; :: thesis: a mod m = 1
then consider k1 being Nat such that
A2: a * n = (m * k1) + ((a * n) mod m) and
(a * n) mod m < m by NAT_D:def 2;
consider k2 being Nat such that
A3: n = (m * k2) + (n mod m) and
n mod m < m by A1, NAT_D:def 2;
(a - 1) * n = m * (k1 - k2) by A1, A2, A3;
then A4: m divides (a - 1) * n by INT_1:def 9;
reconsider t = a - 1, m = m as Integer ;
m divides t by A1, A4, INT_2:40;
then consider tt being Integer such that
A5: a - 1 = m * tt by INT_1:def 9;
A6: a = (m * tt) + 1 by A5;
a - 1 >= 0 by A1, Lm2;
then tt >= 0 by A1, A5, XREAL_1:160;
then reconsider tt = tt, m = m as Element of NAT by INT_1:16;
a mod m = (((m * tt) mod m) + 1) mod m by A6, NAT_D:22
.= (0 + 1) mod m by NAT_D:13
.= 1 by A1, NAT_D:24 ;
hence a mod m = 1 ; :: thesis: verum