3 |^ (((Fermat 1) -' 1) div 2), - 1 are_congruent_mod Fermat 1 by Lm23;
hence 5 is prime by Th51, Th58; :: thesis: verum