theorem :: NAT_6:43

for n being non zero Nat holds
( Fermat n is prime iff 3 |^ (((Fermat n) - 1) / 2), - 1 are_congruent_mod Fermat n )