let a, p be Nat; ( 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
; ( a = 2 & p is Prime )
now ( 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;
hence
a = 2
by A4, XXREAL_0:1;
p is Primeassume
p is not
Prime
;
contradictionthen 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;
verum end;
hence
( a = 2 & p is Prime )
; verum