let a, p, k be Nat; :: thesis: ( (a |^ k) mod p = 1 & k >= 1 & p is prime implies a,p are_relative_prime )
assume A1: ( (a |^ k) mod p = 1 & k >= 1 ) ; :: thesis: ( not p is prime or a,p are_relative_prime )
assume A2: p is prime ; :: thesis: a,p are_relative_prime
assume A3: not a,p are_relative_prime ; :: thesis: contradiction
reconsider a = a, p = p, k = k as Element of NAT by ORDINAL1:def 13;
a gcd p = p by A2, A3, PEPIN:2;
then p divides a by NAT_D:def 5;
then consider i being Nat such that
A4: a = p * i by NAT_D:def 3;
(((p * i) mod p) |^ k) mod p = 1 by A1, A4, PEPIN:12;
then (0 |^ k) mod p = 1 by NAT_D:13;
then (p * 0 ) mod p = 1 by A1, NEWTON:16;
hence contradiction by NAT_D:13; :: thesis: verum