let a, p be Nat; :: thesis: ( p > 1 & (a |^ p) - 1 is Prime implies ( a = 2 & p is Prime ) )
assume that
A1: p > 1 and
A2: (a |^ p) - 1 is Prime ; :: thesis: ( a = 2 & p is Prime )
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 ;
then a < a |^ p by ;
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 ;
a - 1 divides (a |^ p) - 1 by A1, A2, Lm6, Th27;
hence contradiction by A2, A5, A7, A8, NAT_4:12; :: thesis: verum
end;
hence a = 2 by ; :: 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 ;
consider q being Nat such that
A12: p = n * q by ;
1 + 1 <= n by ;
then 2 < 2 |^ n by PREPOWER:13;
then A13: 2 + 1 <= 2 |^ n by NAT_1:13;
2 |^ n <= a |^ n by ;
then 2 + 1 <= a |^ n by ;
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 ;
a |^ n < a |^ p by ;
then A16: (a |^ n) - 1 < (a |^ p) - 1 by XREAL_1:9;
(a |^ n) - 1 divides ((a |^ n) |^ q) - 1 by ;
then (a |^ n) - 1 divides (a |^ p) - 1 by ;
hence contradiction by A2, A16, A15, A14, NAT_4:12; :: thesis: verum
end;
hence ( a = 2 & p is Prime ) ; :: thesis: verum