let a, n be Nat; :: thesis: ( a > 1 & n > 1 & (a |^ n) + 1 is Prime implies ( a is even & ex k being non zero Nat st n = 2 |^ k ) )
assume A0: ( a > 1 & n > 1 & (a |^ n) + 1 is Prime ) ; :: thesis: ( a is even & ex k being non zero Nat st n = 2 |^ k )
FinalLemma: ( n is even implies ex s being Nat st n = 2 |^ s )

proof

assume n is even ; :: thesis: ex s being Nat st n = 2 |^ s
then consider s, t being Nat such that
C1: ( t is odd & s > 0 & n = (2 |^ s) * t ) by A0, NAT_5:2;
P1: t >= 1

proof

assume t < 1 ; :: thesis: contradiction
hence contradiction by C1, NAT_1:14; :: thesis: verum

end;

VV: ((a |^ (2 |^ s)) |^ t) + 1 is Prime by A0, C1, NEWTON:9;
reconsider aaa = a |^ (2 |^ s) as Nat ;
a to_power (2 |^ s) > a to_power 0 by A0, POWER:39;
then VB: aaa > 1 by NEWTON:4;
v2: t is odd by C1;
t < 1 + 1

proof

assume t >= 1 + 1 ; :: thesis: contradiction
then t > 1 by NAT_1:13;
then t is even by VV, VB, FunnyLemma;
hence contradiction by v2; :: thesis: verum

end;

then t <= 1 by NAT_1:13;
then t = 1 by P1, XXREAL_0:1;
hence ex s being Nat st n = 2 |^ s by C1; :: thesis: verum

end;

V4: a <> 1 by A0;
n is even

proof

assume A2: n is odd ; :: thesis: contradiction
set n1 = n -' 1;
set aa = - a;
set bb = 1;
n >= 1 + 1 by A0, NAT_1:13;
then n - 1 >= 2 - 1 by XREAL_1:9;
then A1: (n -' 1) + 1 = n by NAT_D:43;
B2: (- a) |^ n = - (a |^ n) by A2, POWER:2;
((- a) |^ n) - (1 |^ n) = ((- a) - 1) * (Sum (((- a),1) Subnomial (n -' 1))) by A1, NEWTON04:51;
then - ((a |^ n) + 1) = - ((a + 1) * (Sum (((- a),1) Subnomial (n -' 1)))) by B2;
then V1: a + 1 divides (a |^ n) + 1 ;
V3: a > 0 by A0;
then V2: a + 1 <> 1 ;
a + 1 <> (a |^ n) + 1

proof

assume a + 1 = (a |^ n) + 1 ; :: thesis: contradiction
then a to_power 1 = a to_power n ;
then 1 = n by V3, V4, POWER:50;
hence contradiction by A0; :: thesis: verum

end;

then (a |^ n) + 1 is not Prime by V1, V2, INT_2:def 4;
hence contradiction by A0; :: thesis: verum

end;

then consider s being Nat such that
D1: n = 2 |^ s by FinalLemma;
D2: s <> 0

proof

assume s = 0 ; :: thesis: contradiction
then n = 1 by D1, NEWTON:4;
hence contradiction by A0; :: thesis: verum

end;

a is even

proof

assume a is odd ; :: thesis: contradiction
then (a |^ n) + 1 = 2 by A0, NUMBER06:2;
then a to_power n = a to_power 0 by NEWTON:4;
hence contradiction by A0, POWER:50; :: thesis: verum

end;

hence ( a is even & ex k being non zero Nat st n = 2 |^ k ) by D1, D2; :: thesis: verum