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