let a, p be Nat; :: thesis: ( p > 1 & (a |^ p) - 1 is Prime implies ( a = 2 & p is Prime ) )
assume A1:
( p > 1 & (a |^ p) - 1 is Prime )
; :: thesis: ( a = 2 & p is Prime )
now A2:
a > 1
by A1, LmST2;
then A3:
a >= 1
+ 1
by NAT_1:13;
p >= 1
+ 1
by NAT_1:13, A1;
then
a < a |^ p
by A2, PREPOWER:21;
then A4:
a - 1
< (a |^ p) - 1
by XREAL_1:11;
hence
a = 2
by XXREAL_0:1, A3;
:: thesis: p is Primeassume A8:
p is not
Prime
;
:: thesis: contradictionconsider n being
Element of
NAT such that A9:
(
n divides p & 1
< n &
n < p )
by NAT_4:12, A1, A8;
consider q being
Nat such that A10:
p = n * q
by A9, NAT_D:def 3;
(a |^ n) - 1
divides ((a |^ n) |^ q) - 1
by LmST1, PEPIN:26, A2, A9;
then A11:
(a |^ n) - 1
divides (a |^ p) - 1
by NEWTON:14, A10;
a |^ n < a |^ p
by A2, A9, PEPIN:71;
then A12:
(a |^ n) - 1
< (a |^ p) - 1
by XREAL_1:11;
a >= 0 + 1
by A1, LmST2;
then A13:
(a |^ n) - 1 is
Element of
NAT
by PREPOWER:19, NAT_1:21;
1
+ 1
<= n
by NAT_1:13, A9;
then
2
< 2
|^ n
by PREPOWER:21;
then A14:
2
+ 1
<= 2
|^ n
by NAT_1:13;
2
|^ n <= a |^ n
by A3, PREPOWER:17;
then
2
+ 1
<= a |^ n
by A14, XXREAL_0:2;
then
2
< a |^ n
by NAT_1:13;
then
2
- 1
< (a |^ n) - 1
by XREAL_1:11;
hence
contradiction
by NAT_4:12, A1, A11, A12, A13;
:: thesis: verum end;
hence
( a = 2 & p is Prime )
; :: thesis: verum