3 |^ (((Fermat 1) -' 1) div 2), - 1 are_congruent_mod Fermat 1 by Lm22;
hence 5 is prime by Th56, Th63; :: thesis: verum