let a, n be Nat; :: thesis: ( a > 1 & n > 1 & (a |^ n) + 1 is Prime implies n is even )
assume A0: ( a > 1 & n > 1 & (a |^ n) + 1 is Prime ) ; :: thesis: n is even
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 = (n -' 1) + 1 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 ;
V4: a <> 1 by A0;
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