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

now

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

now

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

suppose a = 0 ; :: thesis: contradiction

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

end;

suppose a = 1 ; :: thesis: contradiction

then (a |^ p) - 1 = 1 - 1 by NEWTON:15;
hence contradiction by INT_2:def 5, A1; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence contradiction by A2, NAT_1:26; :: thesis: verum