let n be Element of NAT ; ( n > 1 & n <> 4 & Fib n is prime implies n is prime )
assume that
A1:
n > 1
and
A2:
n <> 4
; ( not Fib n is prime or n is prime )
assume A3:
Fib n is prime
; n is prime
assume
not n is prime
; contradiction
then consider k being non zero Element of NAT such that
A4:
k <> 1
and
A5:
k <> 2
and
A6:
k <> n
and
A7:
k divides n
by A1, A2, Th49;
A8:
Fib k <> Fib n
by A1, A4, A6, Th48;
( Fib k <> 1 & Fib k divides Fib n )
by A4, A5, A7, Th42, Th47;
hence
contradiction
by A3, A8, INT_2:def 4; verum