let m, n, k be Nat; :: thesis: ( 1 < m & (n * k) mod m = k mod m & k,m are_relative_prime implies n mod m = 1 )
assume A1: ( 1 < m & (n * k) mod m = k mod m & k,m are_relative_prime ) ; :: thesis: n mod m = 1
then consider t1 being Nat such that
A2: ( n * k = (m * t1) + ((n * k) mod m) & (n * k) mod m < m ) by NAT_D:def 2;
consider t2 being Nat such that
A3: ( k = (m * t2) + (k mod m) & k mod m < m ) by A1, NAT_D:def 2;
(n * k) - (1 * k) = m * (t1 - t2) by A1, A2, A3;
then A4: m divides k * (n - 1) by INT_1:def 9;
reconsider n = n, m = m as Integer ;
m divides n - 1 by A1, A4, INT_2:40;
then consider tt being Integer such that
A5: n - 1 = m * tt by INT_1:def 9;
n = (m * tt) + 1 by A5;
then n mod m = 1 mod m by EULER_1:13
.= 1 by A1, NAT_D:14 ;
hence n mod m = 1 ; :: thesis: verum