let a, m be Nat; ( a <> 0 & m is prime & a,m are_relative_prime implies (a |^ m) mod m = a mod m )
assume that
A1:
a <> 0
and
A2:
m is prime
and
A3:
a,m are_relative_prime
; (a |^ m) mod m = a mod m
A4:
m > 1
by A2, INT_2:def 5;
then
m - 1 > 1 - 1
by XREAL_1:11;
then reconsider mm = m - 1 as Element of NAT by INT_1:16;
Euler m = m - 1
by A2, EULER_1:21;
then
((a |^ mm) mod m) * a = 1 * a
by A1, A3, A4, Th33;
then
( mm + 1 = m & ((a |^ mm) * a) mod m = a mod m )
by Th9;
hence
(a |^ m) mod m = a mod m
by NEWTON:11; verum