let n, p be Nat; :: thesis: ( p is prime & n,p are_relative_prime implies (n |^ (p -' 1)) mod p = 1 )
assume that
A1: p is prime and
A2: n,p are_relative_prime ; :: thesis: (n |^ (p -' 1)) mod p = 1
A3: p <> 0 by A1, INT_2:def 4;
A4: n <> 0

proof

assume n = 0 ; :: thesis: contradiction
then n gcd p = p by NEWTON:52;
then n gcd p > 1 by A1, INT_2:def 4;
hence contradiction by A2, INT_2:def 3; :: thesis: verum

end;

then A5: n |^ (p -' 1) <> 0 by PREPOWER:5;
(n |^ p) mod p = n mod p by A1, A2, A4, EULER_2:19;
then A6: ((n |^ (p -' 1)) * n) mod p = n mod p by A3, A4, Th27;
p > 1 by A1, INT_2:def 4;
hence (n |^ (p -' 1)) mod p = 1 by A2, A6, A5, EULER_2:12; :: thesis: verum