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