let a, k be Nat; ( k + 1 is prime & not k + 1 divides a implies k + 1 divides (a |^ k) - 1 )
assume that
A1:
k + 1 is prime
and
A2:
not k + 1 divides a
; k + 1 divides (a |^ k) - 1
k + 1 divides (a |^ (k + 1)) - a
by A1, Th58;
then
k + 1 divides ((a |^ k) * a) - a
by NEWTON:6;
then
k + 1 divides a * ((a |^ k) - 1)
;
hence
k + 1 divides (a |^ k) - 1
by A1, A2, INT_5:7; verum