257 -' 1 = 257 - 1 by XREAL_0:def 2
.= 256 + 0 ;
then Fermat 3 divides (3 |^ (((Fermat 3) -' 1) div 2)) - (- 1) by Lm47, Th53;
then 3 |^ (((Fermat 3) -' 1) div 2), - 1 are_congruent_mod Fermat 3 ;
hence 257 is prime by Th53, Th58; :: thesis: verum