let a, m be Nat; ( a <> 0 & m is prime & a,m are_coprime implies (a |^ m) mod m = a mod m )
assume that
A1:
a <> 0
and
A2:
m is prime
and
A3:
a,m are_coprime
; (a |^ m) mod m = a mod m
A4:
m > 1
by A2, INT_2:def 4;
then
m - 1 > 1 - 1
by XREAL_1:9;
then reconsider mm = m - 1 as Element of NAT by INT_1:3;
Euler m = m - 1
by A2, EULER_1:20;
then
((a |^ mm) mod m) * a = 1 * a
by A1, A3, A4, Th18;
then
( mm + 1 = m & ((a |^ mm) * a) mod m = a mod m )
by Th7;
hence
(a |^ m) mod m = a mod m
by NEWTON:6; verum