let a, m be Nat; :: thesis: ( m is prime implies (a |^ m) mod m = a mod m )
assume A2: m is prime ; :: thesis: (a |^ m) mod m = a mod m

per cases ( a,m are_coprime or not a,m are_coprime ) ;

suppose A3: a,m are_coprime ; :: thesis: (a |^ m) mod m = a mod m

per cases ( a <> 0 or a = 0 ) ;

suppose A1: a <> 0 ; :: thesis: (a |^ m) mod m = a mod m

m - 1 > 1 - 1 by A2, 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, A2, A3, 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; :: thesis: verum

end;

suppose a = 0 ; :: thesis: (a |^ m) mod m = a mod m

hence (a |^ m) mod m = a mod m by A2, NEWTON:11; :: thesis: verum

end;

end;

end;

suppose not a,m are_coprime ; :: thesis: (a |^ m) mod m = a mod m

then consider p being Nat such that
A5: p divides a and
A6: p divides m and
A7: p <> 1 by NOW;
m divides a by A2, A5, A6, A7;
then consider k being Nat such that
A7: a = m * k by NAT_D:def 3;
A8: (m * k) mod m = 0 by NAT_D:13;
((m * k) |^ m) mod m = (((m * k) mod m) |^ m) mod m by Th12P
.= 0 mod m by A2, A8, NEWTON:11
.= 0 by INT_1:73 ;
hence (a |^ m) mod m = a mod m by A7, A8; :: thesis: verum

end;

end;