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

hence contradiction by A3, NAT_1:25; :: thesis: verum

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
a <= 1
; :: thesis: contradictionassume A4:
( a = 0 or a = 1 )
; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;hence contradiction ; :: thesis: verum

hence contradiction by A3, NAT_1:25; :: thesis: verum