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 )

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 )

hence
( a = 2 & p is Prime )
; :: thesis: verumA3:
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;

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 A3, A10, Th27, PEPIN:25;

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;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

hence
a = 2
by A4, XXREAL_0:1; :: thesis: p is Primeassume 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 A1, A2, Lm6, Th27;

hence contradiction by A2, A5, A7, A8, NAT_4:12; :: thesis: verum

end;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 A1, A2, Lm6, Th27;

hence contradiction by A2, A5, A7, A8, NAT_4:12; :: thesis: verum

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 A3, A10, Th27, PEPIN:25;

then (a |^ n) - 1 divides (a |^ p) - 1 by A12, NEWTON:9;

hence contradiction by A2, A16, A15, A14, NAT_4:12; :: thesis: verum