let a, p be Nat; :: thesis:
assume that
A1: p > 1 and
A2: (a |^ p) - 1 is Prime ; :: thesis:

A3: now :: thesis:

assume A4: ( a = 0 or a = 1 ) ; :: thesis:

per cases by A4;

suppose a = 0 ; :: thesis:

then (a |^ p) - 1 = 0 - 1 by A1, NEWTON:84;
hence contradiction by A2; :: thesis:

end;

suppose a = 1 ; :: thesis:

then (a |^ p) - 1 = 1 - 1 ;
hence contradiction by A2, INT_2:def 4; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

assume a <= 1 ; :: thesis:
hence contradiction by A3, NAT_1:25; :: thesis: