let a, p be Nat; :: thesis: ( p <> 1 & (a |^ p) - 1 is Prime implies ( a = 2 & p is Prime ) )
assume that
A0: p <> 1 and
A2: (a |^ p) - 1 is Prime ; :: thesis: ( a = 2 & p is Prime )

A1: now :: thesis: not p <= 1

assume p <= 1 ; :: thesis: contradiction
then p = 0 by A0, NAT_1:25;
then (a |^ p) - 1 = 1 - 1 by NEWTON:4;
hence contradiction by A2, INT_2:def 4; :: thesis: verum

end;

now :: thesis: ( a = 2 & p is Prime )

A3: a > 1 by A1, A2, Lm6;
then A4: a >= 1 + 1 by NAT_1:13;
p >= 1 + 1 by A1, NAT_1:13;
then a < a |^ p by A3, PREPOWER:13;
then A5: a - 1 < (a |^ p) - 1 by XREAL_1:9;

now :: thesis: not a > 2

assume A6: a > 2 ; :: thesis: contradiction
then A7: a - 1 > 2 - 1 by XREAL_1:9;
A8: a - 1 is Element of NAT by A6, NAT_1:20;
a - 1 divides (a |^ p) - 1 by Th27;
hence contradiction by A2, A5, A7, A8, NAT_4:12; :: thesis: verum

end;

hence a = 2 by A4, XXREAL_0:1; :: thesis: p is Prime
assume p is not Prime ; :: thesis: contradiction
then consider n being Element of NAT such that
A9: n divides p and
A10: 1 < n and
A11: n < p by A1, NAT_4:12;
consider q being Nat such that
A12: p = n * q by A9, NAT_D:def 3;
1 + 1 <= n by A10, NAT_1:13;
then 2 < 2 |^ n by PREPOWER:13;
then A13: 2 + 1 <= 2 |^ n by NAT_1:13;
2 |^ n <= a |^ n by A4, PREPOWER:9;
then 2 + 1 <= a |^ n by A13, XXREAL_0:2;
then 2 < a |^ n by NAT_1:13;
then A14: 2 - 1 < (a |^ n) - 1 by XREAL_1:9;
a >= 0 + 1 by A1, A2, Lm6;
then A15: (a |^ n) - 1 is Element of NAT by NAT_1:21, PREPOWER:11;
a |^ n < a |^ p by A3, A11, PEPIN:66;
then A16: (a |^ n) - 1 < (a |^ p) - 1 by XREAL_1:9;
(a |^ n) - 1 divides ((a |^ n) |^ q) - 1 by Th27;
then (a |^ n) - 1 divides (a |^ p) - 1 by A12, NEWTON:9;
hence contradiction by A2, A16, A15, A14, NAT_4:12; :: thesis: verum

end;

hence ( a = 2 & p is Prime ) ; :: thesis: verum