let a, p be Nat; :: thesis: ( p > 1 & (a |^ p) - 1 is Prime implies a > 1 )
assume that
A1: p > 1 and
A2: (a |^ p) - 1 is Prime ; :: thesis: a > 1

A3: now :: thesis: ( not a = 0 & not a = 1 )

assume A4: ( a = 0 or a = 1 ) ; :: thesis: contradiction

now :: thesis: contradiction

per cases ( a = 0 or a = 1 ) by A4;

suppose a = 0 ; :: thesis: contradiction

then (a |^ p) - 1 = 0 - 1 by A1, NEWTON:84;
hence contradiction by A2; :: thesis: verum

end;

suppose a = 1 ; :: thesis: contradiction

then (a |^ p) - 1 = 1 - 1 ;
hence contradiction by A2, INT_2:def 4; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

assume a <= 1 ; :: thesis: contradiction
hence contradiction by A3, NAT_1:25; :: thesis: verum