let a, m be Nat; :: thesis: ( a <> 0 & m is prime & a,m are_relative_prime implies (a |^ m) mod m = a mod m )
assume A1: ( a <> 0 & m is prime & a,m are_relative_prime ) ; :: thesis: (a |^ m) mod m = a mod m
then A2: m > 1 by 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;
A3: mm + 1 = m ;
Euler m = m - 1 by A1, EULER_1:21;
then ((a |^ mm) mod m) * a = 1 * a by A1, A2, Th33;
then ((a |^ mm) * a) mod m = a mod m by Th9;
hence (a |^ m) mod m = a mod m by A3, NEWTON:11; :: thesis: verum