let a, m, n be natural Number ; ( a <> 0 & m > 1 & (a * n) mod m = n mod m & m,n are_coprime implies a mod m = 1 )
assume that
A1:
a <> 0
and
A2:
m > 1
and
A3:
(a * n) mod m = n mod m
and
A4:
m,n are_coprime
; a mod m = 1
consider k2 being Nat such that
A5:
n = (m * k2) + (n mod m)
and
n mod m < m
by A2, NAT_D:def 2;
consider k1 being Nat such that
A6:
a * n = (m * k1) + ((a * n) mod m)
and
(a * n) mod m < m
by A2, NAT_D:def 2;
(a - 1) * n = m * (k1 - k2)
by A3, A6, A5;
then A7:
m divides (a - 1) * n
by INT_1:def 3;
reconsider t = a - 1, m = m as Integer ;
m divides t
by A4, A7, INT_2:25;
then consider tt being Integer such that
A8:
a - 1 = m * tt
by INT_1:def 3;
a - 1 >= 0
by A1, Lm2;
then A9:
tt >= 0
by A2, A8;
A10:
a = (m * tt) + 1
by A8;
reconsider tt = tt, m = m as Element of NAT by A9, INT_1:3;
a mod m =
(((m * tt) mod m) + 1) mod m
by A10, NAT_D:22
.=
(0 + 1) mod m
by NAT_D:13
.=
1
by A2, NAT_D:24
;
hence
a mod m = 1
; verum