let n be Nat; :: thesis:
assume FF: n > 8 ; :: thesis:
assume AA: ( card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 ) ; :: thesis:
assume CC: ( n is not mersenne Prime & n + 1 is not fermat Prime ) ; :: thesis:

per cases ;

suppose E1: ( n is odd & n + 1 is even ) ; :: thesis:

then consider m being Nat such that
R1: n + 1 = 2 |^ m by AA, OnlyPrimeDiv;
consider k being Nat, p being Prime such that
R2: n = p |^ k by E1, AA, OnlyPrimeDiv2;
ST: p |^ k = (2 |^ m) - 1 by R1, R2;
RG: ( p > 0 & p <> 1 ) by INT_2:def 4;
HG: m > 1

proof

assume m <= 1 ; :: thesis:
then m < 1 + 1 by NAT_1:13;
then ( m = 0 or m = 1 ) by NAT_1:23;
then ( p |^ k = 1 - 1 or p |^ k = (2 |^ 1) - 1 ) by ST, NEWTON:4;
then p to_power k = p to_power 0 by NEWTON:4;
then k = 0 by RG, POWER:50;
hence contradiction by AA, ZeroDiv1, R2, NEWTON:4; :: thesis:

end;

HH: p |^ k = Mersenne m by ST, GR_CY_3:def 3;
k <= 1 by HH, HG, MersenneTh;
then k < 1 + 1 by NAT_1:13;
then HA: ( k = 0 or k = 1 ) by NAT_1:23;
k <> 0

proof

assume k = 0 ; :: thesis:
then Mersenne m = 1 by HH, NEWTON:4;
hence contradiction by HG, MerLemma; :: thesis:

end;

then S9: n is Prime by R2, HA;
n = (2 |^ m) - 1 by R1;
then n = Mersenne m by GR_CY_3:def 3;
hence contradiction by CC, S9; :: thesis:

end;

suppose E1: ( n + 1 is odd & n is even ) ; :: thesis:

then consider m being Nat such that
R1: n = 2 |^ m by AA, OnlyPrimeDiv;
R3: n + 1 is odd by E1;
then consider k being Nat, p being Prime such that
R2: n + 1 = p |^ k by AA, OnlyPrimeDiv2;
R4: k >= 1

proof

assume k < 1 ; :: thesis:
then k = 0 by NAT_1:14;
then n + 1 = 1 by R2, NEWTON:4;
then n = 0 ;
hence contradiction by FF; :: thesis:

end;

XX: p is odd

proof

assume p is even ; :: thesis:
then p = 2 by LAGRA4SQ:13;
hence contradiction by R2, R3, R4; :: thesis:

end;

not m <= 1

proof

assume m <= 1 ; :: thesis:
then m < 1 + 1 by NAT_1:13;
then ( m = 0 or m = 1 ) by NAT_1:23;
then ( n = 1 or n = 2 |^ 1 ) by R1, NEWTON:4;
hence contradiction by FF; :: thesis:

end;

then UJ: m > 1 ;
SH: p |^ k = (2 |^ m) + 1 by R2, R1;
SY: 2 |^ m = (p |^ k) - 1 by R2, R1;
not k = 1

proof

assume k = 1 ; :: thesis:
then E0: n + 1 = p by R2;
E1: n + 1 is not fermat Prime by CC;
E2: n = 2 |^ m by R1;
then e2: p = (2 |^ m) + 1 by E0;

per cases by UJ;

suppose m < 1 ; :: thesis:

then n = 2 |^ 0 by E2, NAT_1:14
.= 1 by NEWTON:4 ;
hence contradiction by FF; :: thesis:

end;

suppose m = 1 ; :: thesis:

then e3: p = 3 by e2;
3 is fermat Prime by Fermat3;
hence contradiction by CC, e3, E0; :: thesis:

end;

suppose fg: m > 1 ; :: thesis:

ff: p = (2 |^ m) + 1 by e2;
consider k being non zero Nat such that
fz: m = 2 |^ k by ff, fg, Curious;
p = (2 |^ (2 |^ k)) + 1 by fz, ff;
then p = Fermat k by PEPIN:def 3;
hence contradiction by E0, E1; :: thesis:

end;

then hc: k > 1 by R4, XXREAL_0:1;
then k >= 1 + 1 by NAT_1:13;
then k - 1 >= 2 - 1 by XREAL_1:9;
then X4: (k -' 1) + 1 = k by NAT_D:43;
then (p |^ k) - (1 |^ k) = (p - 1) * (Sum ((p,1) Subnomial (k -' 1))) by NEWTON04:51;
then KK: (p |^ k) - 1 = (p - 1) * (Sum ((p,1) Subnomial (k -' 1))) ;
then X9: Sum ((p,1) Subnomial (k -' 1)) divides 2 |^ m by SY;
set SS = (p,1) Subnomial (k -' 1);
O1: ( p > 0 & p <> 1 ) by INT_2:def 4;
k is even

proof

assume X1: k is odd ; :: thesis:
X8: len ((p,1) Subnomial (k -' 1)) = k by X4, NEWTON04:def 2;
then X2: len ((p,1) Subnomial (k -' 1)) is odd by X1;
for i being Nat st i in dom ((p,1) Subnomial (k -' 1)) holds
((p,1) Subnomial (k -' 1)) . i is odd

proof

let i be Nat; :: thesis:
assume X6: i in dom ((p,1) Subnomial (k -' 1)) ; :: thesis:
then X0: ( 1 <= i & i <= len ((p,1) Subnomial (k -' 1)) ) by FINSEQ_3:25;
then reconsider m = i - 1 as Nat ;
k - 1 >= 1 - 1 by hc, XREAL_1:9;
then S1: k -' 1 = k - 1 by XREAL_0:def 2;
i - 1 <= k - 1 by X0, X8, XREAL_1:9;
then (k -' 1) - m in NAT by S1, INT_1:5;
then reconsider l = (k -' 1) - m as Nat ;
((p,1) Subnomial (k -' 1)) . i = (p |^ l) * (1 |^ m) by X6, NEWTON04:def 2
.= p |^ l ;
hence ((p,1) Subnomial (k -' 1)) . i is odd by XX; :: thesis:

end;

then Sum ((p,1) Subnomial (k -' 1)) is odd by X2, OddSum;
then Sum ((p,1) Subnomial (k -' 1)) = 1 by X9, DivEqualOne;
then p to_power k = p to_power 1 by KK;
hence contradiction by hc, O1, POWER:50; :: thesis:

end;

then consider l being Nat such that
h1: k = 2 * l by ABIAN:def 2;
((p |^ l) - 1) * ((p |^ l) + 1) = ((p |^ l) ^2) - (1 ^2)
.= ((p |^ l) |^ 2) - 1 by NEWTON:81
.= (p |^ k) - 1 by h1, NEWTON:9 ;
then h3: 2 |^ m = ((p |^ l) - 1) * ((p |^ l) + 1) by SH;
hh: 2 is Prime by INT_2:28;
hb: ( p > 1 & p > 0 ) by INT_2:def 4;
p |^ l <> 2

proof

assume UK: p |^ l = 2 ; :: thesis:
UL: p <> 2

proof

assume p = 2 ; :: thesis:
hence contradiction by UJ, hc, SH; :: thesis:

end;

UH: 2 divides p |^ l by UK;
not 2 is trivial by NAT_2:28;
then p divides 2 by UH, NEWTON03:47;
then ( p = 1 or p = 2 ) by hh, INT_2:def 4;
hence contradiction by UL, INT_2:def 4; :: thesis:

end;

then tt: (p |^ l) - 1 <> 1 ;
ts: l >= 1

proof

assume l < 1 ; :: thesis:
then l = 0 by NAT_1:14;
hence contradiction by h1, R4; :: thesis:

end;

proof

assume m1 < 1 ; :: thesis:
then m1 = 0 by NAT_1:14;
then (p |^ l) - 1 = 1 by SY, NEWTON:4;
hence contradiction by tt; :: thesis:

end;

cc: ( p > 0 & p <> 1 ) by INT_2:def 4;
y1: m2 >= 2

proof

assume m2 < 2 ; :: thesis:

per cases by NAT_1:23;

suppose m2 = 0 ; :: thesis:

then (p |^ l) + 1 = 1 by SZ, NEWTON:4;
then p |^ l = 0 ;
hence contradiction ; :: thesis:

end;

suppose m2 = 1 ; :: thesis:

then (p |^ l) + 1 = 2 by SZ;
then p to_power l = p to_power 0 by NEWTON:4;
hence contradiction by ts, cc, POWER:50; :: thesis:

end;

(2 |^ m2) - (2 |^ m1) = 2 by SY, SZ;
then ( m2 = 2 & m1 = 1 ) by y1, y4, Diff2A;
then ( (p |^ l) - 1 = 2 |^ 1 & (p |^ l) + 1 = 2 |^ 2 ) by SY, SZ;
then h4: ( (p |^ l) - 1 = 2 & (p |^ l) + 1 = 4 ) ;
then h5: p = 3 by Lemma3Prime;
2 |^ m = 2 |^ 3 by h3, h4, POWER:61;
then jj: 3 |^ k = (2 |^ 3) + 1 by SH, h5;
n + 1 = 3 |^ k by R2, h5;
then n = 8 by jj, POWER:61;
hence contradiction by FF; :: thesis:

end;